5

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.

kruk
  • 137
  • 5

1 Answers1

3

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.

François Bobot
  • 316
  • 1
  • 4
  • thanks for the answer. When using wp plugin, it breaks. Now I'm installing Jessie plugin to see if it works. Which one did you use? – kruk Nov 04 '14 at 12:50
  • Tried with Jessie. I had to put declaration of R into axiomatic block. Afterwards, I got typing error: unbound identifier R. @François, you don't have similar problem? Which version of Jessie do you use? – kruk Nov 04 '14 at 14:01
  • sorry for confusion, there was some other technical problem. The idea with introducing logical R works with wp. – kruk Nov 07 '14 at 09:14