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 =)

why? Isn't it ok? I just want to fill an array of int (declared statically) with zeros... Isn't int * array[] an array of int pointers?? Anyway it doesn't do the trick :/ — roo
I don't see what you mean. Even with this signature fill(int * array, int length), the problem is still here... — roo
@EliasVanOotegem In C, arrays are passed by reference. The function is fine, and the specifications are fine. The Value plug-in does not prove the “assigns” because it does not aim to do this (it only uses “assigns” clauses as a source of information, and only for library functions without source code). I thought WP would prove it. Roo, what automatic provers do you have installed? — Pascal Cuoq
Since length is passed as int I would add the precondition that length is ≥0 or >0 though (whichever you prefer). — Pascal Cuoq
@PascalCuoq: My bad, I've googled Frama-C, and now I know what this question is about. That's why I commented, and not set about writing a lengthy answer. I got the impression there was more to this than I initially thought... — Elias Van Ootegem

byako byako · Accepted Answer · 2013-05-24T09:24:08

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.

Unable to prove assign clause - Frama-C

1 Answers