--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on February 2011 ---
On Thu, 2011-02-17 at 16:16 +0100, BAUDIN Patrick wrote: > 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(); Thanks, I'll try it. > 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 I see. However, I'd name that section "Labelled predicates and functions", as "hybrid" is a rather vague term. There's room for improvement wrt to the description of labelled predicates in section 2.6.9. There should be an example that doesn't use axioms because labels are also useful for predicates w/o axioms. -- Regards, Boris