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

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>