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
|
extern /*@out@*/ /*@only@*/ void *smalloc (unsigned int size);
typedef int mint;
typedef struct _st
{
int a;
/*@only@*/ int *b;
/*@shared@*/ mint *c;
int d;
} *st;
/*@only@*/ st st_create1 ()
{
st res = (st) smalloc (sizeof(struct _st));
int *z;
res->a = 3;
z = res->b; /* res->b not defined */
z = (*res).c; /* (*res).c not defined */
return res; /* res->d not defined */
}
void f1(/*@only@*/ st x)
{
free (x->b);
free (x);
} /* correct */
void f2(/*@only@*/ st x)
{
free (x);
} /* bad --- didn't release x->b */
void f3(/*@only@*/ st x)
{
free (x->c); /* bad --- x->c is shared */
} /* bad --- didn't release x */
/*@only@*/ st st_create ()
{
st res = (st) smalloc(sizeof(struct _st));
res->a = 3;
return res; /* 6, 7, 8. res->b, res->c, res->d not defined */
}
|
