]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | typedef struct |
2 | { | |
3 | /*@owned@*/ int *x; | |
4 | /*@owned@*/ int *y; | |
5 | /*@dependent@*/ int *z; | |
6 | } *pair; | |
7 | ||
8 | extern /*@only@*/ /*@out@*/ void *smalloc (size_t); | |
9 | ||
10 | /*@only@*/ pair pair_create (void) | |
11 | { | |
12 | pair p = (pair) smalloc (sizeof (*p)); | |
13 | ||
14 | p->x = smalloc (sizeof (int)); | |
15 | p->y = smalloc (sizeof (int)); | |
16 | p->z = p->y; | |
17 | ||
18 | *(p->x) = 3; | |
19 | *(p->y) = 12; | |
20 | ||
21 | return p; | |
22 | } | |
23 | ||
24 | /*@only@*/ pair pair_create1 (void) | |
25 | { | |
26 | pair p = (pair) smalloc (sizeof (*p)); | |
27 | ||
28 | p->x = smalloc (sizeof (int)); | |
29 | p->y = smalloc (sizeof (int)); | |
30 | p->z = p->y; | |
31 | *(p->y) = 12; | |
32 | ||
33 | *(p->x) = 3; | |
34 | p->y = smalloc (sizeof (int)); | |
35 | *(p->y) = 12; | |
36 | ||
37 | return p; /* 1. Returned storage p->z is only (should be dependant): p */ | |
38 | } | |
39 | ||
40 | void mangle (/*@temp@*/ pair p) | |
41 | { | |
42 | free (p->x); | |
43 | } /* 2. Released storage p->x reachable from parameter */ | |
44 | ||
45 | void mangle2 (/*@temp@*/ pair p) | |
46 | { | |
47 | free (p->x); | |
48 | p->x = p->y; | |
49 | } /* 3. Storage p->y reachable from parameter is dependant */ | |
50 | ||
51 | /*@only@*/ pair mangle3 (/*@only@*/ pair p) | |
52 | { | |
53 | free (p->x); | |
54 | p->x = p->y; | |
55 | return p; /* 4. Storage p->y reachable from return value is dependant (should be */ | |
56 | } | |
57 | ||
58 | int f (pair p) | |
59 | { | |
60 | p->x = NULL; /* 5. Only storage p->x not released before assignment: p->x = NULL */ | |
61 | ||
62 | return *(p->y); | |
63 | } | |
64 | ||
65 | void swap (pair p) | |
66 | { | |
67 | int *tmp = p->x; | |
68 | ||
69 | p->x = p->y; | |
70 | p->y = tmp; | |
71 | } | |
72 | ||
73 | void mangleok (/*@temp@*/ pair p) | |
74 | { | |
75 | int *loc = p->x; | |
76 | *loc = 8; | |
77 | } |