source: CIVL/examples/loop_invariants/arrayZeroes2d.cvl@ b0ff124

#include<assert.h>

#pragma CIVL ACSL

$input int N;
$assume(N > 0);

void arrayZeroes(int (*a)[], int n) {
  int i, j;
  
  /*@ loop invariant 0 <= i && i <= n;
    @ loop invariant \forall int t; 0<=t && t<i ==> (\forall int k;  0<=k && k<n ==>
    @                               a[t][k] == 0);
    @ loop assigns i, j, a[0 .. n-1][0 .. n-1];
    @*/
  for (i = 0; i < n; i++) {
    /*@ loop invariant 0 <= j && j <= n;
      @ loop invariant \forall int k; 0<=k && k<j 
      @                               ==> a[i][k] == 0;
      @ loop assigns j, a[i][0 .. n-1];
      @*/
    for (j = 0; j < n; j++)
      a[i][j] = 0;
  }
}

int main() {
  int a[N][N];

  $havoc(&a);
  arrayZeroes(a, N);
  $assert($forall (int i : 0 .. N-1) ($forall (int j : 0 .. N-1) a[i][j] == 0));
}