CODEWITHSUNDEEP
verificationframa-c
Mikael Åsberg
Mikael Åsberg

Reputation: 51

Verification issue using the Jessie plug-in and Frama-C

I'm new to Frama-C and I want to learn the ACSL syntax properly. I have this dummy example and the Jessie plug-in cannot verify line nr 9 and 12. Am I missing something? The function to be verified (equal) will check if the two arrays (a and b) have the same values or not at each index:

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

Upvotes: 3

Views: 323

Answers (1)

Cristiano Sousa
Cristiano Sousa

Reputation: 932

There are a couple of incorrect things here:

behavior all_equal:
     assumes i == n;
     ensures \result == 1;
 behavior some_not_equal:
    assumes i != n;
    ensures \result == 0;

In the assumes clause, all variables are evaluated in the pre-state of the function. Meaning if you have two equal arrays of size n, and assuming i is 0 (which it could not be, see next explanation), i == n will always fail except when the array is of size 0

Another thing: you seem to be using i as a variable for loop control, setting it to 0 at the start of the loop, however in your annotations you say that i, in the pre-state of the program, is between 0 and n. This in conjunction with what I said previously are one of the reasons why jessie isn't able to prove this.

Finally, the main reason you cannot prove this is because you are missing an essential loop invariant, one that guarantees that both arrays, for all array indexes previous to the current iteration, are equal:

loop invariant loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];

With this invariant you can now specify your behaviors better. A correct solution for your problem would be:

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

Upvotes: 2

Related Questions