--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on November 2010 ---
Le lun. 15 nov. 2010 15:54:32 CET, Guillaume Melquiond <guillaume.melquiond at inria.fr> a ?crit : > Le lundi 15 novembre 2010 ? 15:33 +0100, Pascal Cuoq a ?crit : > > 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; */ > > Unless I'm mistaken, this is equivalent to > > /*@ assert \at(i, b) == 2; */ > > since all the other \at operators apply to constant values and are > therefore ignored. This tends to be my interpretation too, but my guess is that Pascal has another semantics in mind: each \at goes back in time (to the last time the label has been encountered, starting from the current point), so that the whole expression denotes the value of i the third-to-last time b has been reached. I'm not sure I agree with using \at as the (backward) description of an execution path, though. I tend to find that quite confusing. > > 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? -- Virgile Prevosto Ing?nieur-Chercheur, CEA, LIST Laboratoire de S?ret? des Logiciels +33/0 1 69 08 82 98