#pragma CIVL ACSL
int * a;

/*@ assigns (a + (0 .. 9))[0 .. 9][0];
  @*/
int f() {
  return 0;
}