test/clauses3.c

   1 typedef struct { /*@null@*/ /*@only@*/ int *x; } *st;
   2
   3 void f(/*@only@*/ st x)
   4 {
   5   if (x->x != NULL)
   6     {
   7       free (x->x);
   8     } ;
   9
  10   free (x);
  11 }
  12
  13 void f2 (/*@only@*/ st x)
  14 {
  15   if (x->x != NULL)
  16     {
  17       free (x->x);
  18     }
  19   else
  20     {
  21       ;
  22     }
  23
  24   free (x);
  25 }
  26
  27 void g (/*@only@*/ st x)
  28 {
  29   if (x->x == NULL)
  30     {
  31     }
  32   else
  33     {
  34       free (x->x);
  35     }
  36
  37   free (x);
  38 }
  39
  40 void h(/*@only@*/ st x)
  41 {
  42   if (7 > 3)
  43     {
  44       if (x->x != NULL)
  45         {
  46           free (x->x);
  47         }
  48     } /* 1. Storage x->x is released in one path, but live in another. */
  49
  50   free (x);
  51 }
  52
  53 void m(/*@only@*/ st x)
  54 {
  55   if (7 > 3)
  56     {
  57     }
  58   else
  59     {
  60       free (x->x); /* 2. Possibly null storage passed as non-null param: x->x */
  61     } /* 3. Storage x->x is released in one path, but live in another. */
  62
  63   free (x);
  64 }
  65
  66
  67
  68
  69