]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | typedef struct |
885824d3 | 2 | { |
3 | /*@only@*/ char *name; | |
4 | int val; | |
5 | } *stx; | |
6 | ||
7 | /*@only@*/ char *stx_name (stx x) | |
8 | { | |
9 | return (x->name); /* 1. Function returns reference to parameter x: (x->name) | |
10 | ** [2]. Return value exposes rep of stx: (x->name) | |
11 | ** 3. Released storage x->name reachable from parameter | |
12 | */ | |
13 | } | |
14 | ||
15 | /*@observer@*/ char *stx_observeName (stx x) | |
16 | { | |
17 | return (x->name); | |
18 | } | |
19 | ||
20 | /*@exposed@*/ char *stx_exposeName (stx x) | |
21 | { | |
22 | return (x->name); /* okay */ | |
23 | } | |
24 | ||
25 | char *f (stx x) | |
26 | { | |
27 | char *s; | |
28 | ||
29 | s = stx_name (x); | |
30 | free (s); /* okay */ | |
31 | ||
32 | s = stx_observeName (x); | |
33 | *s = 'x'; /* 4. Modification of observer */ | |
34 | free (s); /* 5. Pass observer as only */ | |
35 | ||
36 | s = stx_exposeName (x); | |
37 | *s = 'x'; /* okay */ | |
38 | free (s); /* 6. Pass exposed as only */ | |
39 | ||
40 | s = stx_observeName (x); | |
41 | return s; /* 7. Observer storage s returned without qualification: s | |
42 | ** 8. Dependent storage s returned as unqualified: s | |
43 | */ | |
44 | } | |
45 | ||
46 | ||
47 | ||
48 | ||
49 | ||
50 | ||
51 |