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