source: CIVL/examples/loop_invariants/loop_assigns_given/arrayZeroes1d-bad.cvl@ afc300c

#include<assert.h>

#pragma CIVL ACSL

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

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

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