--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with predicate and location labels



Hello Virgile,

so, if ACSL predicates are evaluated by-value, is there a way to define a
predicate that has the same behavior as

#define unchanged(k) (k <==> \old(k))

that can be used in other contracts?

Alternatively, I may use assigns L instead and make sure that k is not in
L. But there's a problem if the function contains an if-statement and
assigns k in one branch, but not in the other. Since assigns is a keyword
like requires or ensures, I can't specify a postcondition such as

ensures (cond ==> assigns k) && (!cond ==> assigns \empty);

It is possible using behaviors but these can't be specified as predicates
to be reused in other contracts.

BTW, I believe the ACSL manual, sections 2.3.3, 2.3.4 is wrong on the
equivalence of named and regular contract as stated on p. 30.

Regards,
Boris