test/cases2.c

   1 extern /*@only@*/ int *g(/*@only@*/ int *y);
   2
   3 /*@null@*/ /*@only@*/ int *f(/*@only@*/ int *x)
   4 {
   5   switch (*x)
   6     {
   7     case 1:
   8       return g(x);
   9     case 2:
  10       return g(x);
  11     case 3:
  12       return g(x);
  13     default:
  14       return g(x);
  15     }
  16 }
  17
  18 /*@null@*/ /*@only@*/ int *f2(/*@only@*/ int *x)
  19 {
  20   switch (*x)
  21     {
  22     case 1:
  23       return g(x);
  24     case 2:
  25       return g(x);
  26     } /* 1. Variable x is released in one possible execution, but live ... */
  27
  28   return g(x);
  29 }
  30
  31 /*@null@*/ /*@only@*/ int *f3(/*@only@*/ int *x)
  32 {
  33   switch (*x)
  34     {
  35     case 1:
  36       return g(x);
  37     }
  38
  39   return g(x);
  40 }