struct S1 {
  int t;
};

int foo(struct S1 s) {
  /*@assert \initialized(&s.t); */
  if (s.t > 0)
    return 0;
  return 1;
}

int main(int argc, const char **argv) {
  struct S1 s;
  s.t = 1;
  /*@assert \initialized(&s.t); */
  foo(s);
  return 0;
}