1 typedef struct { /*@null@*/ /*@only@*/ int *x; } *st;
3 void f(/*@only@*/ st x)
13 void f2 (/*@only@*/ st x)
27 void g (/*@only@*/ st x)
40 void h(/*@only@*/ st x)
48 } /* 1. Storage x->x is released in one path, but live in another. */
53 void m(/*@only@*/ st x)
60 free (x->x); /* 2. Possibly null storage passed as non-null param: x->x */
61 } /* 3. Storage x->x is released in one path, but live in another. */