1 typedef struct _node *node;
5 /*@dependent@*/ /*@null@*/ node next;
8 void node_free1 (/*@only@*/ node n)
10 free (n); /* error: must free n->next */
13 void node_free2 (/*@only@*/ node n)
17 } /* okay - no need to free nn since it is dependent */
19 void node_free3 (/*@only@*/ node n)
23 node_free1 (nn); /* error: dependent at only */