--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on November 2010 ---
Le 15/11/2010 15:31, Virgile Prevosto a ?crit : > Yes. To be frank, I've never been really convinced by the syntactic > restriction above. As shown by the 'g' function, this does not solve > all uninitialization issues. It seemed to me that a label can be used in an annotation only if the label program point L "dominates" the program point P of the annotation, meaning that every path that reach P must go through L, but I might be wrong... Moreover, I think that when I worked on the 'scope' plug-in, we said that \at(x,L) means the value of (x) the last time L was reached. So, I am not sure that I would even accept : //@ assert \at(c,Pre) != 0 ==> \at(i-d, then) == 0; on f... because of the dominators reason. -- Anne.