[splint-discuss] Ensures clause question

[Gaurav Mathur]

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