test/linked2.c

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