--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] \at in ACSL assertions



Le lundi 15 novembre 2010 ? 16:56 +0100, Anne Pacalet a ?crit :
> Le 15/11/2010 16:51, Guillaume Melquiond a ?crit :
> > So I will state my point again and refrain from giving an example. It is
> > not obvious to me that \at(v,l) is the value of variable v the last time
> > the program reached label l. It could also be any value of v any time
> > the program reached l.
> 
> Your interpretation looks strange if you consider the annotation :
>    //@ assert x > \at (y, Here);
> Would it means that x is greater than every values y can take
> in any execution ?

As a matter of fact, that's exactly the current ACSL interpretation. The
annotation above is syntactic sugar for

Here42:
//@ assert \at(x,Here42) > \at(y,Here42);

and it precisely states that for any program state at label Here42, the
value of variable x in that state is greater than the value of variable
y in that state.

That said, I see how my interpretation fails when it involves several
labels in a loop, so Virgile's one seems like the only sensible one, if
any.

Best regards,

Guillaume