]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | typedef struct |
2 | { | |
3 | int id; | |
4 | char *name; | |
5 | } *record; | |
6 | ||
7 | int *badResult (void) | |
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@*/ | |
11 | { | |
12 | return NULL; /* 3. Null storage returned as non-null: NULL */ | |
13 | } | |
14 | ||
15 | /*@special@*/ record createName (/*@only@*/ char *name) | |
16 | /*@defines result->name@*/ | |
17 | { | |
18 | record res = (record) malloc (sizeof (*res)); | |
19 | ||
20 | assert (res != NULL); | |
21 | res->name = name; | |
22 | return res; | |
23 | } | |
24 | ||
25 | /*@special@*/ record createName2 (void) | |
26 | /*@defines result->name@*/ | |
27 | { | |
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 */ | |
31 | } | |
32 | ||
33 | /*@special@*/ record createName3 (void) | |
34 | /*@defines result->id@*/ | |
35 | /*@allocates result->name@*/ | |
36 | { | |
37 | record res = (record) malloc (sizeof (*res)); | |
38 | ||
39 | assert (res != NULL); | |
40 | ||
41 | res->name = (char *) malloc (sizeof (char) * 23); | |
42 | res->id = 21; | |
43 | return res; | |
44 | } | |
45 | ||
46 | /*@special@*/ record createName4 (void) | |
47 | /*@defines result->id@*/ | |
48 | /*@allocates result->name@*/ | |
49 | { | |
50 | record res = (record) malloc (sizeof (*res)); | |
51 | ||
52 | assert (res != NULL); | |
53 | ||
54 | res->id = 21; | |
55 | return res; /* 6. Unallocated storage res->name corresponds to storage ... */ | |
56 | } | |
57 | ||
58 | ||
59 | ||
60 | ||
61 |