test/stack.c

   1 int *glob;
   2
   3 void stack1 (int **x)
   4 {
   5   int sa[3] = { 0, 1, 2 } ;
   6   int loc = 3;
   7
   8   glob = &loc;
   9   *x = &sa[0];
  10 } /* 1. Stack-allocated storage *x reachable from parameter x,
  11      2. Stack-allocated storage glob reachable from global glob
  12   */
  13
  14 /*@dependent@*/ int *f (int c)
  15 {
  16   int x = 3;
  17
  18   if (c == 0)
  19     {
  20       return &x; /* 3. Stack-allocated storage &x reachable from return value */
  21     }
  22   else
  23     {
  24       int sa[10];
  25
  26       sa[0] = 35;
  27       sa[2] = 37;
  28
  29       if (c == 1)
  30         {
  31           return sa; /* 4. Stack-allocated storage sa reachable ... */
  32         }
  33       else
  34         {
  35           return &sa[0]; /* 5. Stack-allocated storage sa reachable ... */
  36         }
  37     }
  38 }
  39
  40