]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | typedef union _ut |
2 | { | |
3 | int x; | |
4 | int y; | |
5 | int *ox; | |
6 | /*@dependent@*/ int *dx; | |
7 | struct { int a; int b; int *ip; } st; | |
8 | } *ut; | |
9 | ||
10 | extern /*@only@*/ /*@out@*/ void *smalloc (size_t); | |
11 | ||
12 | ut ut_create1 (/*@unused@*/ int a) | |
13 | { | |
14 | ut u = (ut) smalloc (sizeof (*u)); | |
15 | ||
16 | return u; /* 1. Returned union u contains no defined field */ | |
17 | } | |
18 | ||
19 | ut ut_create2 (int a) | |
20 | { | |
21 | ut u = (ut) smalloc (sizeof (*u)); | |
22 | ||
23 | u->x = a; | |
24 | return u; | |
25 | } | |
26 | ||
27 | ut ut_create3 (int a) | |
28 | { | |
29 | ut u = (ut) smalloc (sizeof (*u)); | |
30 | ||
31 | u->x = a; | |
32 | u->y = a; | |
33 | return u; /* [Not anymore. Returned union u has 2 defined fields: x, y */ | |
34 | } | |
35 | ||
36 | ut ut_create4 (int *t) | |
37 | { | |
38 | ut u = (ut) smalloc (sizeof (*u)); | |
39 | ||
40 | u->ox = t; /* 2. Implicitly temp storage t assigned to implicitly only */ | |
41 | return u; | |
42 | } | |
43 | ||
44 | ut ut_create5 (int *t) | |
45 | { | |
46 | ut u = (ut) smalloc (sizeof (*u)); | |
47 | ||
48 | u->dx = t; /* 3. Implicitly temp storage t assigned to dependent: u->dx = t */ | |
49 | return u; | |
50 | } | |
51 | ||
52 | ut ut_create6 (void) | |
53 | { | |
54 | ut u = (ut) smalloc (sizeof (*u)); | |
55 | ||
56 | u->st.a = 3; | |
57 | return u; /* 4. Returned storage u->st contains 2 undefined fields: b, ip */ | |
58 | } | |
59 | ||
60 | ut ut_create7 (int *p) | |
61 | { | |
62 | ut u = (ut) smalloc (sizeof (*u)); | |
63 | ||
64 | u->st.a = 3; | |
65 | u->st.b = 4; | |
66 | u->st.ip = p; /* 5. Implicitly temp storage p assigned to implicitly only */ | |
67 | return u; | |
68 | } | |
69 | ||
70 | void ut_mangle1 (ut u) | |
71 | { | |
72 | free (u->ox); | |
73 | } /* 6. Released storage u->ox reachable from parameter */ | |
74 | ||
75 | void ut_mangle2 (ut u) | |
76 | { | |
77 | free (u->st.ip); | |
78 | } /* 7. Released storage u->st.ip reachable from parameter */ | |
79 | ||
80 | void ut_mangle3 (ut u) | |
81 | { | |
82 | free (u->st.ip); | |
83 | u->x = 3; /* This one's a toughy... */ | |
84 | } /* 8. Released storage u->st.ip reachable from parameter */ |