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