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

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.