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



Le mer. 16 f?vr. 2011 17:49:10 CET,
"Boris Hollas" <hollas at informatik.htw-dresden.de> a ?crit :

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

No, this is not possible. \at and \old cannot be expressed as normal
ACSL functions.

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

However, you can define a predicate cond, and use it in the assumes
clauses of the behaviors and everywhere else.

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

You're right. The global requires clause makes regular contract quite
specific.

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