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