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



On Thu, 2011-02-17 at 16:16 +0100, BAUDIN Patrick wrote:
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();
>
With

/*@	predicate unchanged{P,H}(bool* p) =
		\at(*p, P) <==> \at(*p, H);
*/

and

ensures unchanged{P,H}(&this->active)

I get "user error: no label in the context".

-- 
Regards,
Boris