4 void f1 (/*@keep@*/ int *x)
10 void f2 (/*@keep@*/ int *x)
12 free (x); /* 1. Keep storage passed as only param: x */
15 int f3 (/*@keep@*/ int *x)
17 int *y = malloc (sizeof (int));
19 if (y == NULL) return 3; /* 2. Keep storage not transferred before return: x */
29 int f4 (/*@only@*/ int *x)
34 void f5 (/*@unused@*/ /*@keep@*/ int *x)
36 return; /* 3. Keep storage not transferred before return: x */
39 void f6 (/*@keep@*/ int *x)
44 } /* 4. Variable x is kept in true branch, but live in continuation. */
46 f2 (x); /* 5. Kept storage passed as keep: f2 (x) */
49 /*@null@*/ int *f7 (/*@null@*/ /*@keep@*/ int *x)
60 return x; /* 6. Kept storage x returned as implicitly only: x */