[splint-discuss] Ensures clause question

[CBFalconer]

Gaurav Mathur wrote:
> 
> 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.

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!