[splint-discuss] Ensures clause question
cbfalconer at yahoo.com
Sun Nov 30 10:33:39 EST 2003
Gaurav Mathur wrote:
> 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.
y is passed by value, and thus any alterations by the function are
lost. But, within the function, how about:
y = (x < 0);
Chuck F (cbfalconer at yahoo.com) (cbfalconer at worldnet.att.net)
Available for consulting/temporary embedded and systems.
<http://cbfalconer.home.att.net> USE worldnet address!
More information about the splint-discuss