Cannot prove assignment condition - Frama-C

Question

I am new to Frama-c and I would like to understand what the problem is 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) will not prove the assignment clause in the contract of a function, and I cannot understand why. Any help would be appreciated =)

Answer 1

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

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

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

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