--- layout: fc_discuss_archives title: Message 119 from Frama-C-discuss on December 2009 ---
Sorry, I made a confusion since "p" is a formal parameter. Of course, these two clauses (assigns and ensures) hold. /*@ requires \valid(p); @ assigns *p; @ ensures *p == 1; */ void f(int *p) { *p = 1; } That specification is equivalent to : /*@ requires \valid(p); @ assigns *\old(p); @ ensures *\old(p) == 1; */ void f(int *p) { *p = 1; } Now let consider "q" a global variable : int * q ; This specification holds : /*@ requires \valid(q); @ assigns *\old(q); @ ensures *\old(q) == 1; */ void g(void) { *g = 1; } But without the use \old construction, something is required about separation to satisfy the ensures clauses. /*@ requires \valid(q) && something about separation @ assigns *q; @ ensures *q == 1; */ void g(void) { *g = 1; } Patrick Baudin. > > Hello, > Just from an ACSL point of view, the proof of the "assigns" > and "ensures" clauses of your spec requires locations "p" > and "*p" to be \separated. > Patrick Baudin. > > Consider the following spec, > > > > /*@ requries \valid(p); > > @ assigns *p; > > @ ensures *p == 1; > > */ > > void f(int *p) > > { > > *p = 1; > > }