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



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