--- layout: fc_discuss_archives title: Message 76 from Frama-C-discuss on May 2010 ---
Hello, two remarks: 1.) ++ has a higher precedence than * (dereference): http://www.difranco.net/cop2220/op-prec.htm Therefore, I think your implementation must be written as void fun(int* p) { (*p)++; } 2.) Even then you must take into account that an overflow can occur when calling ++, e.g. calling fun with p pointing to INT_MAX. Regards Jens On 20.05.2010, at 12:12, Michael Schausten wrote: > 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++; > } > > I try to prove it with Alt-Ergo via the GWhy-Tool with > frama-c -jessie-analysis -jessie-gui fun.c > > It seems to me, that the prover does not make the right usage of \old. In the right part of the gWhy-Tool, it says it tries to prove: > integer_of_int32(select(int_P_int_M_p_0_22, p_0)) < integer_of_int32(select(int_P_int_M_p_0_22, p_0)) > So apparently, it doesn't try to prove \old(*p) < *p, but rather *p < *p (which is not provable, of course). > > I just can't find out what I'm doing wrong, and I hope you can give me a hint what's the problem with my code. > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100520/d090e614/attachment.htm>