source: CIVL/examples/abstraction/isAllZero.cvl@ 1aaefd4

int allZero(int * A, int len) {
  /* Note in theory one must assert here that A + (0..len-1) are valid pointers.
     There is no good way in CIVL-C to express it currently.
  */
  $assert($true);
  
  int ret;
  $havoc(&ret); // assigning ret a fresh symbolic constant
  $assume(ret == 0 || ret == 1);
  $assume(ret == 1 => $forall (int i: 0 .. (len-1)) A[i] == 0);
  $assume(ret == 0 => $exists (int i: 0 .. (len-1)) A[i] != 0);
  return ret;
}


int allZeroImpl(int * A, int len) {
  int ret = 1;
  
  for (int i = 0; i < len; i++) {
    if (A[i] != 0) {
      ret = 0;
      // return ret // I comment out this early return to enlarge the state space of this function 
                    // for a model checker
    }
  }
  return ret;
}

#define N 10
$input int A[N];

int main() {
  int ret;
  
  /* These two calls deliver the same functionality for the assertion
     below.  The first call is much faster when N is large. But one
     has to prove that allZero is an abstraction of allZeroImpl.

     A separate proof can be done with smaller scopes or using loop
     invariants.  In either case, it can overcome the state explosion
     problem brought by nondeterminism when N is very large.
  */
  ret = allZero(A, N);             
  //ret = allZeroImpl(A, N); 
  
  $assert(ret == 1 => $forall (int i: 0 .. N-1) A[i] == 0);  
}