source: CIVL/mods/dev.civl.abc/examples/contract/memLocation1.c

#pragma CIVL ACSL
/*@ requires \valid(t + (0 .. n-1));
  @ assigns t[0 .. n-1];
  @ assigns *(t + (0 .. n-1));
  @*/
void reset_array(int* t, int n) {
  int i;
  for (i=0;i<n;i++)
    t[i]=0;
}