// weirdness with labels
int main(void) {
	int a = 10, *p;

	goto lbl_1;

  lbl_2:
	/*@ assert \valid(p); */
	return 0;


	// the problem is here: the call to __full_init(... p ...) is inserted
	// before the label lbl_1, instead of before the assignment.
  lbl_1:
	p = &a;
	goto lbl_2;
}