8 extern void setName (/*@special@*/ record *r, /*@only@*/ char *name)
9 /*@defines r->name@*/ ;
11 extern /*@observer@*/ char *getName (/*@special@*/ record r)
14 extern void freeName (/*@special@*/ record r)
15 /*@releases r.name@*/ ;
17 extern /*@observer@*/ char *f (/*@only@*/ char *name, char *id)
24 return (getName (r)); /* r.name not released */
28 return (getName (r)); /* r.name not defined */
32 r.name = malloc (sizeof (char) * 12);
33 setName (&r, name); /* r.name allocated, memory leak */
34 return id; /* r.name not released */
40 printf ("%s\n", r.name); /* dead! */