1 typedef struct _node *node;
8 /*@dependent@*/ item val;
12 void node_free1 (/*@only@*/ node n)
14 free (n); /* errors: must free n->next */
17 void node_free2 (/*@only@*/ node n)
21 } /* error - nn not released */
23 void node_free3 (/*@only@*/ node n)
26 free (n->val); /* error: free dependent */
29 node_free1 (nn); /* okay (error for null) */