[splint-discuss] Ensures clause question

[Gaurav Mathur]

Thanks for the response Chuck..

Here's what I am really curious about.. Let's say that 
x and y are indeed references, and let's assume that 
the value of *y *has* to be either 1 or 0 after the 
function returns and it's not just dependent on the 
if condition of my example. What would be the splint 
annotation to capture that information.

I am a splin newbie so maybe I am missing something out
here. What I actually wanted was to achieve some of the
power of the *ensures* clause of the LSL (Larch) stlye
of specifications. 

Another example would be... Suppose I want to state 
that two char * pointers would have the same value when
the function exits. In LSL I would do something like...

char a[10];
char b[10];
.
.
ensures sameStr (a, b)
.
.

where sameStr was defined in some LSL trait.
How would I do this in splint...

Thanks and Regards,
-Gaurav

> 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!
> 
> 
> _______________________________________________
> splint-discuss mailing list
> splint-discuss at cs.virginia.edu
> http://www.splint.org/mailman/listinfo/splint-discuss