test/clauses.c

   1 int f(/*@only@*/ int *x, /*@only@*/ int *y, /*@only@*/ int *z, /*@only@*/ int *z2)
   2 {
   3   if (3 > 4)
   4     {
   5       free (x);
   6     } /* 1. Variable x is released in true branch, but live in continuation. */
   7
   8   while (3 < 4)
   9     {
  10       free (y);
  11     } /* 2. Variable y is released in while body, but live if loop is not taken. */
  12
  13   if (3 > 4)
  14     {
  15       free (z);
  16     }
  17   else
  18     {
  19       free (z2);
  20     } /* 3. Variable z2 is released in false branch, but live in true branch. */
  21       /* 4. Variable z is released in true branch, but live in false branch. */
  22   return 3;
  23 }
  24