]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | typedef /*@abstract@*/ int *abst1; |
2 | typedef /*@abstract@*/ int abst2; | |
3 | ||
4 | /*@access abst1@*/ | |
5 | /*@access abst2@*/ | |
6 | ||
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 | ||
13 | abst1 f2 (/*@exposed@*/ int *x) | |
14 | { | |
15 | return (abst1) x; /* 3. Implicitly dependent storage x returned as implicitly only */ | |
16 | } | |
17 | ||
18 | abst2 g1 (int x) | |
19 | { | |
20 | return x; | |
21 | } | |
22 | ||
23 | abst2 g2 (int x) | |
24 | { | |
25 | return (abst2) x; | |
26 | } |