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