source: CIVL/examples/loop_invariants/loop_assigns_given/arrayEquals.cvl@ e2570cd

#include<assert.h>

#pragma CIVL ACSL

$input int N;
$assume(N > 0);
$input double a[N];
$input double b[N];

_Bool arrayEquals(double * a, double * b, int n) {
  int i;
  
  /*@ loop invariant 0 <= i && i <= n;
    @ loop invariant \forall int j; 0<=j && j<i ==> a[j] == b[j];  
    @ loop assigns i;
    @*/
  for (i = 0; i < n; i++) 
    if (a[i] != b[i])
      return $false;
  return $true;
}

int main() {
  _Bool ret = arrayEquals(a, b, N);
  
  if (ret)
    assert($forall (int i: 0 .. N-1) a[i] == b[i]);
  //  if (ret < N)
  //  assert(a[ret] != b[ret]);
}