test/fields.c

   1 typedef struct
   2 {
   3   /*@owned@*/ int *x;
   4   /*@owned@*/ int *y;
   5   /*@dependent@*/ int *z;
   6 } *pair;
   7
   8 extern /*@only@*/ /*@out@*/ void *smalloc (size_t);
   9
  10 /*@only@*/ pair pair_create (void)
  11 {
  12   pair p = (pair) smalloc (sizeof (*p));
  13
  14   p->x = smalloc (sizeof (int));
  15   p->y = smalloc (sizeof (int));
  16   p->z = p->y;
  17
  18   *(p->x) = 3;
  19   *(p->y) = 12;
  20
  21   return p;
  22 }
  23
  24 /*@only@*/ pair pair_create1 (void)
  25 {
  26   pair p = (pair) smalloc (sizeof (*p));
  27
  28   p->x = smalloc (sizeof (int));
  29   p->y = smalloc (sizeof (int));
  30   p->z = p->y;
  31   *(p->y) = 12;
  32
  33   *(p->x) = 3;
  34   p->y = smalloc (sizeof (int));
  35   *(p->y) = 12;
  36
  37   return p; /* 1. Returned storage p->z is only (should be dependant): p */
  38 }
  39
  40 void mangle (/*@temp@*/ pair p)
  41 {
  42   free (p->x);
  43 } /* 2. Released storage p->x reachable from parameter */
  44
  45 void mangle2 (/*@temp@*/ pair p)
  46 {
  47   free (p->x);
  48   p->x = p->y;
  49 } /* 3. Storage p->y reachable from parameter is dependant */
  50
  51 /*@only@*/ pair mangle3 (/*@only@*/ pair p)
  52 {
  53   free (p->x);
  54   p->x = p->y;
  55   return p; /* 4. Storage p->y reachable from return value is dependant (should be */
  56 }
  57
  58 int f (pair p)
  59 {
  60   p->x = NULL; /* 5. Only storage p->x not released before assignment: p->x = NULL */
  61
  62   return *(p->y);
  63 }
  64
  65 void swap (pair p)
  66 {
  67   int *tmp = p->x;
  68
  69   p->x = p->y;
  70   p->y = tmp;
  71 }
  72
  73 void mangleok (/*@temp@*/ pair p)
  74 {
  75   int *loc = p->x;
  76   *loc = 8;
  77 }