]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /*@-paramuse@*/ |
2 | ||
3 | typedef struct | |
4 | { | |
5 | int id; | |
6 | char *name; | |
7 | } *record; | |
8 | ||
9 | /*@special@*/ record newrecord (void) | |
10 | /*@defines result@*/ | |
11 | /*@post:isnull result->name@*/ | |
12 | { | |
13 | record r = (record) malloc (sizeof (*r)); | |
14 | ||
15 | assert (r != NULL); | |
16 | r->id = 3; | |
17 | r->name = NULL; | |
18 | return r; | |
19 | } | |
20 | ||
21 | record createrecord (/*@only@*/ char *name) | |
22 | { | |
23 | record r = newrecord (); | |
24 | r->name = name; | |
25 | return r; | |
26 | } | |
27 | ||
28 | record createrecord2 (void) | |
29 | { | |
30 | record r = newrecord (); | |
31 | return r; /* 1. Null storage r->name derivable from return value: r */ | |
32 | } | |
33 | ||
34 | /*@special@*/ record newrecord2 (void) | |
35 | /*@defines *result@*/ | |
36 | /*@post:observer result->name@*/ | |
37 | { | |
38 | record r = (record) malloc (sizeof (*r)); | |
39 | ||
40 | assert (r != NULL); | |
41 | r->id = 3; | |
42 | r->name = NULL; | |
43 | return r; /* 2. Non-observer storage r->name corresponds to storage ... */ | |
44 | } | |
45 | ||
46 | record createrecordx (void) | |
47 | { | |
48 | record r = newrecord2 (); | |
49 | return r; /* 3. Observer storage r->name reachable from observer return */ | |
50 | } | |
51 | ||
52 |