--- layout: fc_discuss_archives title: Message 40 from Frama-C-discuss on February 2011 ---
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