--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on February 2011 ---
Hello, > 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? > Predicates with labels can be usefull. Perhaps you needs to defines predicates having pointers as arguments. For example, contract //@ensures x==\old(x) ; bar(); can be defined as follow: //@predicate bar_spec{L1,L2}(int * p) = \at(*p, L1) == at(*p, L1); //@ensures bar_spec{Here,Old}(&x) ; bar(); The defined predicate can be reused for the specification of foo function. > 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. > They are described in section 2.6.9 "Hybrid functions and predicates". You can have a look at exemples 2.43, 2.44 and 2.45 Patrick Baudin.