Frama-C warning: Missing assigns clause (assigns 'everything' instead)

I'm testing this small program with frama-c and I keep getting the same error. I'm not sure what it means. I'm particularly confused on what assigns everything means.

Here is the code in question with ACSL annotations:

// assuming n is nonnegative and even, f returns n

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  while (i<n) {
    i+=2;
  }
  //@ assert i==n;
  return i;
}

Here is what the terminal says when I try to test the code:

[wp] warning: Missing RTE guards
p3.c:9:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Unknown (Qed:8ms) (54ms)
[wp] Proved goals:    0 / 1
    Alt-Ergo:        0  (unknown: 1)

Solution

First of all, your property is not true as is since you don't require n to be even in the function's precondition. I will therefore show you how to prove a variant of your program with i += 1 in the loop body.

The assigns clause is something that WP requires you to specify for every loop and every external function call. It must contain a list of all the memory locations (i.e., variables) that may be modified by the loop (or function). It needs this in order to know that everything else is not modified by the loop. In particular, in this program WP needs to know that while the value of i may change in the loop, the value of n does not change. But if you don't tell it that this is the case, it assumes that the loop may assign "everything", including n.

To specify this, you can insert the following annotation just above the loop:

/*@ loop assigns i; */

If you try proving this (in the GUI), you will see that WP can verify this assigns clause.

However, your assertion after the loop can still not be proved with this. That is because in addition to an assigns clause, every loop must also have a loop invariant: Something that is always true before and after every iteration of the loop. Choosing correct and sufficiently powerful loop invariants is a dark art, but in general the invariant must be something that, once the loop condition is false and the loop has terminated, allows us to conclude the assertion after the loop.

That is, we want as invariant a formula I that has the property that:

I && !(i < n)  ==>  i == n

A good choice is therefore the loop invariant i <= n since if i <= n but we know that i < n is not true (because the loop has stopped iterating), then i must be equal to n.

Putting everything together, here is an annotated variant of your program:

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  /*@ loop assigns i;
    @ loop invariant i <= n;
   */
  while (i<n) {
    i += 1;
  }
  //@ assert i==n;
  return i;
}

And this is verified automatically:

[wp] warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals:    4 / 4
    Qed:             4