#pragma CIVL ACSL
int * a;

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