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

On Wed, 2011-02-16 at 18:43 +0100, Virgile Prevosto wrote:
> > 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.

Assume I have a function foo that calls another function bar. I want to
write a contract for foo such as

ensures bar_spec(this->a);

where bar_spec also specifies variables that remain unchanged and
bar_spec may contain specifications of functions called by bar. Thus,
the specification of function foo contains the union of all functions
transitively called by foo. 
So far, I use the preprocessor to accomplish this. Is there a more
elegant way to do this?

Also, what is the semantics of predicate p{L1,...,Ln}(...) and how does
it relate to predicate p(...)? I haven't found a description of
predicate labels in the ACSL manual.
-- 
Regards,
Boris