8 /* 1. Function result is used in defines clause of badResult but ...
9 2. Special clause accesses field of non-struct or union result */
10 /*@defines result->name@*/
12 return NULL; /* 3. Null storage returned as non-null: NULL */
15 /*@special@*/ record createName (/*@only@*/ char *name)
16 /*@defines result->name@*/
18 record res = (record) malloc (sizeof (*res));
25 /*@special@*/ record createName2 (void)
26 /*@defines result->name@*/
28 record res = (record) malloc (sizeof (*res));
29 return res; /* 4. Undefined storage res->name corresponds to storage listed ...
30 5. Possibly null storage res returned as non-null: res */
33 /*@special@*/ record createName3 (void)
34 /*@defines result->id@*/
35 /*@allocates result->name@*/
37 record res = (record) malloc (sizeof (*res));
41 res->name = (char *) malloc (sizeof (char) * 23);
46 /*@special@*/ record createName4 (void)
47 /*@defines result->id@*/
48 /*@allocates result->name@*/
50 record res = (record) malloc (sizeof (*res));
55 return res; /* 6. Unallocated storage res->name corresponds to storage ... */