]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | typedef struct _node *node; |
2 | ||
3 | struct _node { | |
4 | int val; | |
5 | /*@null@*/ node next; | |
6 | } | |
7 | ||
8 | void node_free1 (/*@only@*/ node n) | |
9 | { | |
10 | free (n); /* error: must free n->next */ | |
11 | } | |
12 | ||
13 | void node_free2 (/*@only@*/ node n) | |
14 | { | |
15 | node nn = n->next; | |
16 | free (n); /* okay */ | |
17 | } /* error: must free nn */ | |
18 | ||
19 | void node_free3 (/*@only@*/ node n) | |
20 | { | |
21 | node nn = n->next; | |
22 | free (n); /* okay */ | |
23 | node_free1 (nn); /* possibly null error */ | |
24 | } /* okay */ | |
25 |