1 typedef /*@abstract@*/ int *abst1;
2 typedef /*@abstract@*/ int abst2;
9 return x; /* 1. Function returns reference to parameter x,
10 2. Implicitly temp storage x returned as implicitly only: x */
13 abst1 f2 (/*@exposed@*/ int *x)
15 return (abst1) x; /* 3. Implicitly dependent storage x returned as implicitly only */