[splint.git] / test / stack.c

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 ... */
	}
    }
}
Commit	Line	Data
885824d3	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