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 ... */