1 # include "repexpose.h"
3 abst abst_create (/*@dependent@*/ abst p, /*@only@*/ char *x, int i)
5 abst a = (abst) malloc (sizeof (struct _abst));
8 a->name = x; /* 1. Arrow access from possibly null pointer a */
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 */
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 */
24 /*@only@*/ char *abst_name (abst a)
26 return a->name; /* 7. Released storage a->name reachable from parameter */
27 /* [15, 16.] reference to parameter, exposes rep */
35 int *abst_aval(abst a)
37 return (&(a->val)); /* 9. [17, 18] reference to parameter, exposes rep */
40 abst abst_parent (abst a)
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 */
49 /*@dependent@*/ char *immut_name (immut im)
51 return (im->name); /* 10. Only storage im->name returned as dependent: (im->name) */
52 /* [23, 24] exposes rep, reference to parameter */
55 void abst_setIm (abst a, immut im)
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! */
61 immut abst_getIm (abst a)
63 return (a->im); /* NO rep exposure since it is immutable */