--- layout: fc_discuss_archives title: Message 20 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 lun. 15 nov. 2010 15:07:03 CET,
Yannick Moy <yannick.moy at adacore.com> a ?crit :

> >> a- should the commented functions main and f be parsable by the
> >> front-end? Currently, they can't be parsed with either Boron or the
> >> development version. The error message is similar to "u.c:14:[kernel]
> >> user error: logic label `cond' not found in annotation"
> 
> Interesting possibility, to designate the last value at some label, including at
> a more deeply nested level.
> 

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.

-- 
Virgile Prevosto
Ing?nieur-Chercheur, CEA, LIST
Laboratoire de S?ret? des Logiciels
+33/0 1 69 08 82 98