--- layout: fc_discuss_archives title: Message 26 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 lundi 15 novembre 2010 ? 16:38 +0100, Virgile Prevosto a ?crit :

> > That said, characterizing a label in an inner loop does not seem that
> > obvious to me. Virgile explained it should be the last one encountered,
> > but why couldn't it be all the labels at once? In other words, the
> > logical property would become an invariant of the loop.
> > 
> 
> But at the point where \at is written, we don't know that the label is
> inside a loop or not: in the 'g' example, there is no loop at all, and
> as already said, the fact that it is in an inner block is irrelevant as
> soon as you have gotos. In addition, \at(i,b) is a term that can be
> part of an arbitrary complicated statement (containing others \at as
> subterm). What kind of invariant would you infer from that?

The invariant part was just an example for clarifying what I meant by
"all the labels at once" in the case of the original "assert
\at(i,b)==2" inside a loop. I completely agree that whether the label is
in a loop is irrelevant.

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.

Best regards,

Guillaume