1 typedef struct _node *node; 2 3 struct _node { 4 int val; 5 /*@dependent@*/ /*@null@*/ node next; 6 } 7 node_free1(node n)8void node_free1 (/*@only@*/ node n) 9 { 10 free (n); /* error: must free n->next */ 11 } 12 node_free2(node n)13void 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)19void 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