]>
Commit | Line | Data |
---|---|---|
885824d3 | 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 | ||
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 | ||
22 | /*@tempref@*/ rp rp_temp (void) | |
23 | { | |
24 | return rp_create2 (); /* 2. New reference returned as temp reference: rp_create2() */ | |
25 | } | |
26 | ||
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 | ||
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 | ||
46 | rp rp_ref (rp x) | |
47 | { | |
48 | return x; /* 4. Reference counted storage returned without modifying ... */ | |
49 | } | |
50 | ||
51 | rp rp_refok (rp x) | |
52 | { | |
53 | x->refs++; | |
54 | return x; | |
55 | } | |
56 | ||
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 | ||
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 |