1 int f(/*@only@*/ int *x
, /*@only@*/ int *y
, /*@only@*/ int *z
, /*@only@*/ int *z2
)
6 } /* 1. Variable x is released in true branch, but live in continuation. */
11 } /* 2. Variable y is released in while body, but live if loop is not taken. */
20 } /* 3. Variable z2 is released in false branch, but live in true branch. */
21 /* 4. Variable z is released in true branch, but live in false branch. */