source: CIVL/examples/loop_invariants/loop_assigns_gen/arrayEquals2.cvl@ 367a390

#include<assert.h>

#pragma CIVL ACSL

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

int arrayEquals(double * a, double * b, int n) {
  int i = 0;
  
  /*@ loop invariant 0 <= i && i <= n;
    @ loop invariant \forall int j; 0<=j && j<i ==> a[j] == b[j];  
    @*/
  while (0<=i && i < n && a[i] == b[i]) 
    i++;
  return i;
}

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