1 typedef struct _node *node;
2 
3 struct _node {
4   int val;
5   /*@dependent@*/ /*@null@*/ node next;
6 }
7 
node_free1(node n)8 void node_free1 (/*@only@*/ node n)
9 {
10   free (n); /* error: must free n->next */
11 }
12 
node_free2(node n)13 void node_free2 (/*@only@*/ node n)
14 {
15   node nn = n->next;
16   free (n); /* okay */
17 } /* okay - no need to free nn since it is dependent */
18 
node_free3(node n)19 void node_free3 (/*@only@*/ node n)
20 {
21   node nn = n->next;
22   free (n); /* okay */
23   node_free1 (nn); /* error: dependent at only */
24 } /* okay */
25 
26