7 /*@only@*/ char *stx_name (stx x)
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
15 /*@observer@*/ char *stx_observeName (stx x)
20 /*@exposed@*/ char *stx_exposeName (stx x)
22 return (x->name); /* okay */
32 s = stx_observeName (x);
33 *s = 'x'; /* 4. Modification of observer */
34 free (s); /* 5. Pass observer as only */
36 s = stx_exposeName (x);
38 free (s); /* 6. Pass exposed as only */
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