--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on November 2010 ---
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.