stack.c

int *glob;
 
/*@dependent@*/
int *f (int **x)
{
  int sa[2] = { 0, 1 };
  int loc = 3;
 
  glob = &loc;
  *x = &sa[0];
 
  return &loc; 
}