--- layout: fc_discuss_archives title: Message 78 from Frama-C-discuss on May 2010 ---
Alos, you should require that p is valid. > /*@ ensures (\old(*p) < *p); > */ > void fun(int* p) { > *p++; > }