5 /*@dependent@*/ int *z;
8 extern /*@only@*/ /*@out@*/ void *smalloc (size_t);
10 /*@only@*/ pair pair_create (void)
12 pair p = (pair) smalloc (sizeof (*p));
14 p->x = smalloc (sizeof (int));
15 p->y = smalloc (sizeof (int));
24 /*@only@*/ pair pair_create1 (void)
26 pair p = (pair) smalloc (sizeof (*p));
28 p->x = smalloc (sizeof (int));
29 p->y = smalloc (sizeof (int));
34 p->y = smalloc (sizeof (int));
37 return p; /* 1. Returned storage p->z is only (should be dependant): p */
40 void mangle (/*@temp@*/ pair p)
43 } /* 2. Released storage p->x reachable from parameter */
45 void mangle2 (/*@temp@*/ pair p)
49 } /* 3. Storage p->y reachable from parameter is dependant */
51 /*@only@*/ pair mangle3 (/*@only@*/ pair p)
55 return p; /* 4. Storage p->y reachable from return value is dependant (should be */
60 p->x = NULL; /* 5. Only storage p->x not released before assignment: p->x = NULL */
73 void mangleok (/*@temp@*/ pair p)