Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.