test/cast2.c

   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 }