]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | typedef struct _node *node; |
2 | ||
3 | typedef struct { | |
4 | char *val; | |
5 | } *item; | |
6 | ||
7 | struct _node { | |
8 | /*@only@*/ item val; | |
9 | /*@null@*/ node next; | |
10 | } | |
11 | ||
12 | extern void keeper (/*@keep@*/ item iv); | |
13 | ||
14 | void node_free1 (/*@only@*/ node n) | |
15 | { | |
16 | free (n); /* 2 errors: must free n->next, n->val */ | |
17 | } | |
18 | ||
19 | void node_free2 (/*@only@*/ node n) | |
20 | { | |
21 | node nn = n->next; | |
22 | keeper (n->val); | |
23 | free (n); /* okay */ | |
24 | } /* error - nn not released */ | |
25 | ||
26 | void node_free3 (/*@only@*/ node n) | |
27 | { | |
28 | node nn = n->next; | |
29 | keeper (n->val); | |
30 | free (n); /* okay */ | |
31 | if (nn != NULL) { | |
32 | node_free1 (nn); /* okay (error for null) */ | |
33 | } | |
34 | } /* okay */ | |
35 |