frama-c - assign句を証明できません - Frama-C

Question

私は Frama-c を初めて使用するので、この簡単な例の問題点を理解したいと思います。

/*@ 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;
    }
}

この例では、Frama-c (WP + 値) は関数コントラクトの assign 句を証明せず、その理由がわかりません。どんな助けでも大歓迎です=）