test/linked5.c

   1 typedef struct _node *node;
   2
   3 typedef struct {
   4   char *val;
   5 } *item;
   6
   7 struct _node {
   8   /*@dependent@*/ item val;
   9   /*@null@*/ node next;
  10 }
  11
  12 void node_free1 (/*@only@*/ node n)
  13 {
  14   free (n); /* errors: must free n->next */
  15 }
  16
  17 void node_free2 (/*@only@*/ node n)
  18 {
  19   node nn = n->next;
  20   free (n); /* okay */
  21 } /* error - nn not released */
  22
  23 void node_free3 (/*@only@*/ node n)
  24 {
  25   node nn = n->next;
  26   free (n->val); /* error: free dependent */
  27   free (n); /* okay */
  28   if (nn != NULL) {
  29     node_free1 (nn); /* okay (error for null) */
  30   }
  31 } /* okay */
  32