--- layout: fc_discuss_archives title: Message 19 from Frama-C-discuss on November 2010 ---
>> 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. >> b- if they were parsable, should the assertion in each function be provable? > > yes for main: the value of j the last time we reach odd before > evaluating the assert is indeed 3. \at(...,cond) does not play any > role here, it is subsumed by the inner \at, > > no for f: then is not reached when c==0, \at(i-d,then) has no defined > value. Basically, we can't say much more than \at(i-d,then) == > \at(i-d,then). > > //@ assert \at(c,Pre) != 0 ==> \at(i-d, then) == 0; > would be true, though. I agree with this semantics. You should not be able to prove much if the value is semantically 'not always initialized'. -- Yannick