--- layout: fc_discuss_archives title: Message 29 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 15/11/2010 17:10, Guillaume Melquiond a ?crit :
> 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.

Yes : but what I tried to say is that x and y values are considered
both to be in the same state.

When you said :
 > 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.

it seemed to me that you proposed to merge several states...

-- 
Anne.