source: CIVL/examples/focus/simpleFor.cvl@ f7b746f

#include<assert.h>
#include<mem.cvh>

#pragma CIVL ACSL
$input int N;
$assume(0 < N);
int a[N];

int main() {

  int x = 0;
  /*@ loop invariant x == i;
    @ loop assigns a[0..N-1],x;
    @ focus F+{0..2} | a[F..F+2];
    @*/
  for (int i = 0; i < N; i++) {
    a[i] = i + x;
    x = x+1;
  }

  //@ focus ordered(<=, F : 0..N-1 | a[F]);
  int y = 0;
  
  // focus F;
  //$assert($forall(int i:0..N-1) a[i] == i+i);
}