Невозможно доказать оговорку о назначении - Frama-C

Я новичок в 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 + Value) не подтвердит пункт assign в функциональном контракте, и я не могу понять, почему. Любая помощь будет оценена =)