Hi, Suppose I have the following code fragment....
void func (int x, int y)
{
if (x<0)
y = 1;
else
y = 0;
}
How do I capture the semantics that y is either
0 or 1 after this function returns. Could I use
ensures (assume y is a reference in that case)
or some other annotation.
Thanks in advance,
Regards,
-Gaurav
_______________________________________________
splint-discuss mailing list
[EMAIL PROTECTED]
http://www.splint.org/mailman/listinfo/splint-discuss
