#pragma CIVL ACSL
int * a;
double x[10];
/*@ 
  @ assigns *((a + (0 .. 9)) + x[0 .. 9]);
  @*/
int f() {
  return 0;
}