--- layout: fc_discuss_archives title: Message 77 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problem with \old



Le jeu. 20 mai 2010 12:12:25 CEST,
Michael Schausten <michaelschausten at googlemail.com> a ?crit :

> Hello,
> 
> I'm getting started using Frama-c, but now I'm stuck with a (probably 
> simple) problem.
> My code:
> 
> /*@ ensures (\old(*p) < *p);
> */
> void fun(int* p) {
>    *p++;
> }
> 

++ binds more tightly than *, so your code reads *(p++) and not (*p)++.

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