]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | extern /*@out@*/ /*@only@*/ void *smalloc (unsigned int size); |
2 | ||
3 | typedef int mint; | |
4 | ||
5 | typedef struct _st | |
6 | { | |
7 | int a; | |
8 | /*@only@*/ int *b; | |
9 | /*@shared@*/ mint *c; | |
10 | int d; | |
11 | } *st; | |
12 | ||
13 | /*@only@*/ st st_create1 () | |
14 | { | |
15 | st res = (st) smalloc (sizeof(struct _st)); | |
16 | int *z; | |
17 | ||
18 | res->a = 3; | |
19 | z = res->b; /* res->b not defined */ | |
20 | z = (*res).c; /* (*res).c not defined */ | |
21 | ||
22 | return res; /* res->d not defined */ | |
23 | } | |
24 | ||
25 | void f1(/*@only@*/ st x) | |
26 | { | |
27 | free (x->b); | |
28 | free (x); | |
29 | } /* correct */ | |
30 | ||
31 | void f2(/*@only@*/ st x) | |
32 | { | |
33 | free (x); | |
34 | } /* bad --- didn't release x->b */ | |
35 | ||
36 | void f3(/*@only@*/ st x) | |
37 | { | |
38 | free (x->c); /* bad --- x->c is shared */ | |
39 | } /* bad --- didn't release x */ | |
40 | ||
41 | /*@only@*/ st st_create () | |
42 | { | |
43 | st res = (st) smalloc(sizeof(struct _st)); | |
44 | res->a = 3; | |
45 | return res; /* 6, 7, 8. res->b, res->c, res->d not defined */ | |
46 | } | |
47 | ||
48 |