test/alias5.c

   1 typedef struct
   2 {
   3   /*@only@*/ int *x;
   4   /*@only@*/ int *y;
   5 } *pair;
   6
   7 # include "alias5.lh"
   8
   9 void incx1 (pair p)
  10 {
  11   pair p2 = p;
  12
  13   p2->x++; /* 1. Suspect modification of p->x through alias p2->x: p2->x++ */
  14 }
  15
  16 void incx2 (pair p)
  17 {
  18   pair p2 = p;
  19
  20   p2 = pair_create ();
  21   p2->x++;
  22 } /* 2. Fresh storage p2 not released before return */
  23
  24 void incx3 (pair p)
  25 {
  26   pair p2 = pair_create ();
  27   p2->x = p->x; /* 3. Only storage p2->x not released before assignment: p2->x = p->x */
  28   *(p2->x) = 3; /* 4. Suspect modification of *(p->x) through alias *(p2->x): */
  29   pair_free (p2);
  30 } /* 5. Storage p->x reachable from parameter is kept (should be only) */
  31
  32
  33