]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | # include "repexpose.h" |
2 | ||
3 | abst abst_create (/*@dependent@*/ abst p, /*@only@*/ char *x, int i) | |
4 | { | |
5 | abst a = (abst) malloc (sizeof (struct _abst)); | |
6 | abst b = p; | |
7 | ||
8 | a->name = x; /* 1. Arrow access from possibly null pointer a */ | |
9 | a->val = i; | |
10 | a->parent = p; /* [3. exposes rep] */ | |
11 | a->parent = b; /* [4. exposes rep through alias] */ | |
12 | a->parent = p->parent; /* [5, 6. exposes rep] */ | |
13 | a->parent = b->parent; /* 2. Suspect modification of p->parent through alias a->parent */ | |
14 | /* [7, 8. exposes rep through alias] 3. modifies p */ | |
15 | b = a; | |
16 | a->name = *globstring; /* [9, 10.] exposes rep through global */ | |
17 | b->name = *globstring; /* ??? NO? 3. Suspect modification of *globstring through alias a->name */ | |
18 | /* [11, 12.] exposes rep through global and alias */ | |
19 | return a; /* 4. Storage a->name reachable from return value is kept */ | |
20 | /* 5. Returned storage *a contains 1 undefined field: im */ | |
21 | /* 6. Storage *globstring reachable from global is kept */ | |
22 | } | |
23 | ||
24 | /*@only@*/ char *abst_name (abst a) | |
25 | { | |
26 | return a->name; /* 7. Released storage a->name reachable from parameter */ | |
27 | /* [15, 16.] reference to parameter, exposes rep */ | |
28 | } | |
29 | ||
30 | int abst_val (abst a) | |
31 | { | |
32 | return a->val; | |
33 | } | |
34 | ||
35 | int *abst_aval(abst a) | |
36 | { | |
37 | return (&(a->val)); /* 9. [17, 18] reference to parameter, exposes rep */ | |
38 | } | |
39 | ||
40 | abst abst_parent (abst a) | |
41 | { | |
42 | abst b = a; | |
43 | ||
44 | if (TRUE) return b; /* [19] reference to parameter a */ | |
45 | else return b->parent; /* 8. Dependent storage b->parent returned as only */ | |
46 | /* 9. Only storage a not released before return */ | |
47 | } | |
48 | ||
49 | /*@dependent@*/ char *immut_name (immut im) | |
50 | { | |
51 | return (im->name); /* 10. Only storage im->name returned as dependent: (im->name) */ | |
52 | /* [23, 24] exposes rep, reference to parameter */ | |
53 | } | |
54 | ||
55 | void abst_setIm (abst a, immut im) | |
56 | { | |
57 | a->im = im; /* 11. Suspect modification of a->im: a->im = im */ | |
58 | /* 13. [25] modifies a, NO rep exposure since it is immutable! */ | |
59 | } | |
60 | ||
61 | immut abst_getIm (abst a) | |
62 | { | |
63 | return (a->im); /* NO rep exposure since it is immutable */ | |
64 | } | |
65 | ||
66 |