--- layout: fc_discuss_archives title: Message 27 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 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 ?

Best regards,
-- 
Anne.