9 /*@special@*/ record newrecord (void)
11 /*@post:isnull result->name@*/
13 record r = (record) malloc (sizeof (*r));
21 record createrecord (/*@only@*/ char *name)
23 record r = newrecord ();
28 record createrecord2 (void)
30 record r = newrecord ();
31 return r; /* 1. Null storage r->name derivable from return value: r */
34 /*@special@*/ record newrecord2 (void)
36 /*@post:observer result->name@*/
38 record r = (record) malloc (sizeof (*r));
43 return r; /* 2. Non-observer storage r->name corresponds to storage ... */
46 record createrecordx (void)
48 record r = newrecord2 ();
49 return r; /* 3. Observer storage r->name reachable from observer return */