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



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