#pragma CIVL ACSL

struct T {
  int x;
} a;

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