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