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



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.