--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on May 2010 ---
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.