--- layout: fc_discuss_archives title: Message 119 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Proof conditions with simple pointer assignment



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;
> > }