1 extern /*@out@*/ /*@only@*/ void *smalloc (size_t);
3 typedef /*@refcounted@*/ struct _rp
9 extern rp rp_create2 (void);
11 void rp_release (/*@killref@*/ rp x)
18 free (x); /* 1. Reference counted storage passed as only param: free (x) */
22 /*@tempref@*/ rp rp_temp (void)
24 return rp_create2 (); /* 2. New reference returned as temp reference: rp_create2() */
27 void rp_f (/*@killref@*/ rp r1, /*@killref@*/ rp r2)
32 r2 = rp_temp (); /* 3. Kill reference parameter r2 not released before assignment */
36 rp rp_create (/*@only@*/ int *p)
38 rp r = (rp) smalloc (sizeof(rp));
48 return x; /* 4. Reference counted storage returned without modifying ... */
57 rp rp_waste (/*@only@*/ int *p)
59 rp z1 = rp_create (p);
63 return z1; /* 5. New reference z2 not released before return */
66 rp rp_waste2 (/*@only@*/ int *p)
68 rp z1 = rp_create (p);
71 z2 = rp_ref (z1); /* 6. New reference z2 not released before assignment */
72 return z1; /* 7. New reference z2 not released ... */