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



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.