#pragma CIVL ACSL

struct T {
  int x;
} * a;

/*@ assigns a->x;
  @*/
int f() {
  return 0;
}