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