int *glob;

void stack1 (int **x)
{
  int sa[3] = { 0, 1, 2 } ;
  int loc = 3;

  glob = &loc;
  *x = &sa[0];
} /* 1. Stack-allocated storage *x reachable from parameter x,
     2. Stack-allocated storage glob reachable from global glob
  */

/*@dependent@*/ int *f (int c)
{
  int x = 3;
  
  if (c == 0)
    {
      return &x; /* 3. Stack-allocated storage &x reachable from return value */ 
    }
  else
    {
      int sa[10];

      sa[0] = 35;
      sa[2] = 37;      

      if (c == 1)
	{
	  return sa; /* 4. Stack-allocated storage sa reachable ... */
	}
      else
	{
	  return &sa[0]; /* 5. Stack-allocated storage sa reachable ... */
	}
    }
}




syntax highlighted by Code2HTML, v. 0.9.1