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



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

If you enforce parentheses: (*p)++
then you will get the expected answer.

If you really meant *p++, that is *(p++), then your ensures clause is 
wrong: *p is not modified.


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |