1 extern /*@out@*/ /*@only@*/ void *smalloc (size_t);
2 
3 typedef /*@refcounted@*/ struct _rp
4 {
5   /*@refs@*/ int refs;
6   /*@only@*/ int *p;
7 } *rp;
8 
9 extern rp rp_create2 (void);
10 
rp_release(rp x)11 void rp_release (/*@killref@*/ rp x)
12 {
13   x->refs--;
14 
15   if (x->refs == 0)
16     {
17       free (x->p);
18       free (x); /* 1. Reference counted storage passed as only param: free (x) */
19     }
20 }
21 
rp_temp(void)22 /*@tempref@*/ rp rp_temp (void)
23 {
24   return rp_create2 (); /* 2. New reference returned as temp reference: rp_create2() */
25 }
26 
rp_f(rp r1,rp r2)27 void rp_f (/*@killref@*/ rp r1, /*@killref@*/ rp r2)
28 {
29   rp rt = rp_temp ();
30 
31   rp_release (r1);
32   r2 = rp_temp (); /* 3. Kill reference parameter r2 not released before assignment */
33   rp_release (rt);
34 }
35 
rp_create(int * p)36 rp rp_create (/*@only@*/ int *p)
37 {
38   rp r = (rp) smalloc (sizeof(rp));
39 
40   r->refs = 1;
41   r->p = p;
42 
43   return r;
44 }
45 
rp_ref(rp x)46 rp rp_ref (rp x)
47 {
48   return x; /* 4. Reference counted storage returned without modifying ... */
49 }
50 
rp_refok(rp x)51 rp rp_refok (rp x)
52 {
53   x->refs++;
54   return x;
55 }
56 
rp_waste(int * p)57 rp rp_waste (/*@only@*/ int *p)
58 {
59   rp z1 = rp_create (p);
60   rp z2 = rp_ref (z1);
61 
62   z2->p++;
63   return z1; /* 5. New reference z2 not released before return */
64 }
65 
rp_waste2(int * p)66 rp rp_waste2 (/*@only@*/ int *p)
67 {
68   rp z1 = rp_create (p);
69   rp z2 = rp_ref (z1);
70 
71   z2 = rp_ref (z1); /* 6. New reference z2 not released before assignment */
72   return z1; /* 7. New reference z2 not released ... */
73 }
74 
75 
76