5 int sa[3] = { 0, 1, 2 } ;
10 } /* 1. Stack-allocated storage *x reachable from parameter x,
11 2. Stack-allocated storage glob reachable from global glob
14 /*@dependent@*/ int *f (int c)
20 return &x; /* 3. Stack-allocated storage &x reachable from return value */
31 return sa; /* 4. Stack-allocated storage sa reachable ... */
35 return &sa[0]; /* 5. Stack-allocated storage sa reachable ... */