1 extern /*@out@*/ /*@only@*/ void *smalloc (unsigned int size);
13 /*@only@*/ st st_create1 ()
15 st res = (st) smalloc (sizeof(struct _st));
19 z = res->b; /* res->b not defined */
20 z = (*res).c; /* (*res).c not defined */
22 return res; /* res->d not defined */
25 void f1(/*@only@*/ st x)
31 void f2(/*@only@*/ st x)
34 } /* bad --- didn't release x->b */
36 void f3(/*@only@*/ st x)
38 free (x->c); /* bad --- x->c is shared */
39 } /* bad --- didn't release x */
41 /*@only@*/ st st_create ()
43 st res = (st) smalloc(sizeof(struct _st));
45 return res; /* 6, 7, 8. res->b, res->c, res->d not defined */