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



Le jeu. 17 f?vr. 2011 16:45:11 CET,
Boris Hollas <hollas at informatik.htw-dresden.de> a ?crit :

> 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.
> 

I think that there's a small typo in Patrick's mail: one of the L1
should be an L2, otherwise the predicate is not very useful ;-)

-- 
E tutto per oggi, a la prossima volta.
Virgile