Unable to verify assign clause - Frama-C

Question

In my example below, frama-c isn't able to prove my assign clause in the function contract and I am not sure why. I would really appreciate any help.

/*@
  @ requires n>0;
  @ requires \valid(a+(0..n-1));
  @ ensures \forall int i; (n>i>=0 ==> a[i]==0);
  @*/

 void f(int n, float *a) {
     /*@ 
       @ loop invariant n>=0;
       @ loop invariant test: \forall int j; (n>j>i ==> a[j]==0);
       @ loop assigns i, a[0..n-1];
       @*/
     for (int i=n-1; i>=0; i--) {
         a[i] = 0;
     }

 }

Here is my ouput:

[wp] 8 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_loop_assign_part3 : Unknown (Qed:24ms) (406ms)
[wp] Proved goals:    7 / 8
    Qed:             5  (4ms-13ms-24ms)
    Alt-Ergo:        2  (20ms-32ms) (28) (unknown: 1)

I'm just zeroing out an array in reverse order in this program.

Answer 1

You are missing a loop invariant on i. As a result, WP has no idea of the range of values it can take, and cannot prove that the indexes of a that are being written are 0 .. n-1. Just add

   @ loop invariant -1 <= i <= n-1;

(Notice that at the end of the last iteration, i is -1, not 0.)