verification - Jessie プラグインと Frama-C を使用した検証の問題

Question

私は Frama-C を初めて使用し、ACSL 構文を適切に学習したいと考えています。このダミーの例がありますが、Jessie プラグインは行番号 9 と 12 を検証できません。検証される関数 (等しい) は、2 つの配列 (a と b) が各インデックスで同じ値を持っているかどうかをチェックします。

/*@
     requires \valid_range(a,0,n-1);
     requires \valid_range(b,0,n-1);
     requires n >= 0;
     requires i >= 0 && i <= n;
     assigns i;
     behavior all_equal:
         assumes i == n;
         ensures \result == 1;
     behavior some_not_equal:
        assumes i != n;
        ensures \result == 0;
*/
int equal(int a[], int n, int b[], int i) {
  /*@ 
    loop invariant 0 <= i <= n;
    loop assigns i;
    loop variant n-i;
  */  
  for (i = 0; i < n; i++) {
    if (a[i] != b[i])
      return 0;
  }
  return 1;
}