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



Alos, you should require that p is valid.

> /*@ ensures (\old(*p) < *p);
> */
> void fun(int* p) {
>    *p++;
> }