--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on November 2010 ---
On Mon, Nov 15, 2010 at 3:07 PM, Yannick Moy <yannick.moy at adacore.com> wrote: > Interesting possibility, to designate the last value at some label I initially thought this would allow to talk imprecisely about execution paths in ACSL, but now that I think about it, I am not sure it is limited to imprecise characterizations of execution paths. Viz: for (i=0; i<=5; i++) { a: j=i; b: j=i; } /*@ assert \at( \at( \at( \at( \at( \at(i, b), a), b), a), b), a) == 2; */ Pascal