]>
Commit | Line | Data |
---|---|---|
77970e15 | 1 | typedef struct { |
2 | int id; | |
3 | /*@only@*/ char *name; | |
4 | } *record; | |
5 | ||
6 | static /*@special@*/ record record_new (void) | |
7 | /*@defines result->id@*/ | |
8 | { | |
9 | record r = (record) malloc (sizeof (*r)); | |
10 | assert (r != NULL); | |
11 | r->id = 3; | |
12 | return r; | |
13 | } | |
14 | ||
15 | static void record_setName (/*@special@*/ record r, /*@only@*/ char *name) | |
16 | /*@defines r->name@*/ | |
17 | { | |
18 | r->name = name; | |
19 | } | |
20 | ||
21 | record record_create (/*@only@*/ char *name) | |
22 | { | |
23 | record r = record_new (); | |
24 | record_setName (r, name); | |
25 | return r; | |
26 | } | |
27 | ||
28 | void record_clearName (/*@special@*/ record r) | |
29 | /*@releases r->name@*/ | |
30 | /*@ensures isnull r->name@*/ | |
31 | { | |
32 | free (r->name); | |
33 | r->name = NULL; | |
34 | } | |
35 | ||
36 | void record_free (/*@only@*/ record r) | |
37 | { | |
38 | record_clearName (r); | |
39 | free (r); | |
40 | } |