1 typedef /*@abstract@*/ int *abst1;
2 typedef /*@abstract@*/ int abst2;
3
4 /*@access abst1@*/
5 /*@access abst2@*/
6
f1(int * x)7 abst1 f1 (int *x)
8 {
9 return x; /* 1. Function returns reference to parameter x,
10 2. Implicitly temp storage x returned as implicitly only: x */
11 }
12
f2(int * x)13 abst1 f2 (/*@exposed@*/ int *x)
14 {
15 return (abst1) x; /* 3. Implicitly dependent storage x returned as implicitly only */
16 }
17
g1(int x)18 abst2 g1 (int x)
19 {
20 return x;
21 }
22
g2(int x)23 abst2 g2 (int x)
24 {
25 return (abst2) x;
26 }
27