CODEWITHSUNDEEP
frama-c
ratt
ratt

Reputation: 125

How to prove this assigns clause, part 2?

I can't think of any idea to get foo's assigns clause to be proved. I tried assigns var; since foo() indirectly modifies the global var variable, but it doesn't work. Is there a way to get an assigns clause for the local p variable or the location return from a()? Here is the code: 

int var;
//@ assigns \nothing;
int *a(){
    return &var;
}
//@ assigns *p;
void b(int* p){
  *p = 1;
}
//@ assigns \nothing;
void foo(){
   int *p = a();
   b(p);
}
//@ assigns var;
void main(){
    var = 0;
    foo();
    return;
}

frama-c command:

frama-c -wp test.c

[kernel] Parsing test.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assign_normal_part3 : Unknown (103ms)
[wp] [Alt-Ergo] Goal typed_foo_assign_exit_part3 : Unknown (Qed:4ms) (102ms)
[wp] Proved goals:    8 / 10
  Qed:             8 
  Alt-Ergo:        0  (unknown: 2)

Upvotes: 1

Views: 130

Answers (1)

byako
byako

Reputation: 3422

As you guessed, foo does assign something, and assigns \nothing is an invalid clause for this function. The proper clause is indeed assigns var. Within an assigns clause, you must list all global variables that are modified, plus all the variables that are local to a caller and that can be reference through a formal.

Now, why does the proof of the variants with assigns var not go through? Well, as written, in foo, WP cannot guess where p points to, as it has no way of knowing that it is actually equal to &a. You must add this information to the specification of function a. With this modification, the proof is immediate.

Full code:

int var;

/*@ assigns \nothing;
    ensures \result == &var; */
int *a(){
    return &var;
}

//@ assigns *p;
void b(int* p){
  *p = 1;
}

//@ assigns var;
void foo(){
   int *p = a();
   b(p);
}

//@ assigns var;
void main(){
    var = 0;
    foo();
    return;
}

Upvotes: 1

Related Questions