[splint-discuss] Ensures clause question

Gaurav Mathur Gaurav at Colorado.EDU
Sun Nov 30 02:51:34 EST 2003


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




More information about the splint-discuss mailing list