]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | typedef struct |
2 | { | |
3 | int *x; | |
4 | int *y; | |
5 | /*@dependent@*/ int *z; | |
6 | } *pair; | |
7 | ||
8 | extern void pair_keep (/*@keep@*/ pair p); | |
9 | ||
10 | extern /*@only@*/ /*@out@*/ void *smalloc (size_t); | |
11 | extern /*@partial@*/ pair pair_part (void); | |
12 | ||
13 | /*@only@*/ pair pair_copy (pair p) | |
14 | { | |
15 | pair ret = (pair) smalloc (sizeof (*ret)); | |
16 | ||
17 | ret->x = p->x; | |
18 | ret->y = p->y; | |
19 | ret->z = p->z; | |
20 | ||
21 | return (ret); /* 1. Storage p->x reachable from parameter is kept (should be only) */ | |
22 | } /* 2. Storage p->y reachable from parameter is kept (should be only) */ | |
23 | ||
24 | /*@only@*/ pair pair_create (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; /* 3. Only storage p->y assigned to dependent: p->z = p-y */ | |
31 | ||
32 | *(p->x) = 3; | |
33 | *(p->y) = 12; | |
34 | ||
35 | return p; /* 4. Storage p->y reachable from return value is unqualified */ | |
36 | } | |
37 | ||
38 | pair pair_swankle (/*@keep@*/ pair p) | |
39 | { | |
40 | pair ret = pair_part (); | |
41 | ||
42 | ret->x = p->x; | |
43 | pair_keep (p); /* 5. Storage p->x reachable from passed parameter is kept */ | |
44 | p->x = smalloc (sizeof (int)); | |
45 | *p->x = 3; | |
46 | return ret; | |
47 | } |