Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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