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