test/fields2.c

   1 typedef struct
   2 {
   3   int *x;
   4   int *y;
   5   /*@dependent@*/ int *z;
   6 } *pair;
   7
   8 extern void pair_keep (/*@keep@*/ pair p);
   9
  10 extern /*@only@*/ /*@out@*/ void *smalloc (size_t);
  11 extern /*@partial@*/ pair pair_part (void);
  12
  13 /*@only@*/ pair pair_copy (pair p)
  14 {
  15   pair ret = (pair) smalloc (sizeof (*ret));
  16
  17   ret->x = p->x;
  18   ret->y = p->y;
  19   ret->z = p->z;
  20
  21   return (ret); /* 1. Storage p->x reachable from parameter is kept (should be only) */
  22 }               /* 2. Storage p->y reachable from parameter is kept (should be only) */
  23
  24 /*@only@*/ pair pair_create (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; /* 3. Only storage p->y assigned to dependent: p->z = p-y */
  31
  32   *(p->x) = 3;
  33   *(p->y) = 12;
  34
  35   return p; /* 4. Storage p->y reachable from return value is unqualified */
  36 }
  37
  38 pair pair_swankle (/*@keep@*/ pair p)
  39 {
  40   pair ret = pair_part ();
  41
  42   ret->x = p->x;
  43   pair_keep (p); /* 5. Storage p->x reachable from passed parameter is kept */
  44   p->x = smalloc (sizeof (int));
  45   *p->x = 3;
  46   return ret;
  47 }