Unable to prove assign clause - Frama-C

Question

I'm new to Frama-c and I'd like to understand what is the problem with this simple example :

/*@ requires \valid(array+(0..length-1))
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0;
@ assigns array[0..length-1];
*/
void fill(int array[], int length){
    /*@ loop invariant 0 <= i <= length;
    @ loop invariant \forall integer k; 0 <= k < i ==> array[k] == 0;
    @ loop assigns i, array[0..i-1];
    @ loop variant length - i;
    */
    for(int i = 0; i < length; i++){
        array[i] = 0;
    }
}

In this example, Frama-c (WP + Value) won't prove the assign clause in the function contract and I can't understand why. Any help will be appreciated =)

Answer 1

This can be proven (with alt-ergo 0.95.1) if you weaken your loop assigns.

@ loop assigns i, array[0..length-1];

The precondition i >= 0 is also needed, because it is not implied by \valid(array+(0..length-1). array+(0..length-1) is a valid set of locations with length <= 0, although an empty one.

The fact that your original loop assigns does not imply your precondition is a limitation of the current version of the WP plugin.