[splint-discuss] Ensures clause question

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


Suppose I have the following code fragment....

void func (int x, int y)
	if (x<0)
		y = 1;
		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,


More information about the splint-discuss mailing list