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