Assigns clause for local variables in Frama-C

Question

I am trying to verify the following piece of code using frama-c

/*@ ensures \result != \null; 
  @ assigns \nothing;
  @*/
extern int *new_value();

//@ assigns *p;
void f(int* p){
  *p = 8;
}
//@ assigns \nothing;
int main(void){
 int *p = new_value(); 
 f(p);
}

The prover is unable to prove that main assigns \nothing, which makes sense, as main assigns to *p through function f. However, how should I state that in \assigns clause, since p is local variable and can not be accessed within annotation.

Answer 1

The assigns nothing is indeed false. The variable p is local but the effect is done on *p which is an arbitrary pointer.

Counterexample

If new_value is defined as the following:

int g;

int *new_value(){
  return &g;
}

It satisfies the specification and the value of g is 8 at the end of the main.

To go further

If the problem is to be able to give an assign to the function main without any knowledge of the behavior of the function new_value, you can make the result of new_value accessible from the logic space:

For instance :

//@ logic int * R ;
//@ ensures \result == R && \valid(R) ; assigns \nothing ;
extern int *new_value();

//@ assigns *p;
void f(int * p) { … }

//@ assigns *R ;
int main(void) { … }

A more general solution would be to have a set of pointer for R, instead of a unique one.