Assigns a sentence for local variables in Frama-C

Question

I am trying to check the following code snippet 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 explorer cannot prove that main assigns \ anything that makes sense, since main assigns * p via function f. However, how should I indicate that the \ assigns the sentence, since p is a local variable and cannot be accessed in the annotation.

Answer 1

assigns nothing really false. The variable p is local, but the effect is performed 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 g is 8 at the end of the main one.

Go further

If the problem is to enable you to assign the main function without any knowledge of the behavior of the new_value function, you can make the new_value result accessible from the logical 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 pointers for R, and not the only one.