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 ([EMAIL PROTECTED]) ([EMAIL PROTECTED])
> Available for consulting/temporary embedded and systems.
> <http://cbfalconer.home.att.net> USE worldnet address!
>
>
> _______________________________________________
> splint-discuss mailing list
> [EMAIL PROTECTED]
> http://www.splint.org/mailman/listinfo/splint-discuss
_______________________________________________
splint-discuss mailing list
[EMAIL PROTECTED]
http://www.splint.org/mailman/listinfo/splint-discuss
