typedef struct 
{
  /*@only@*/ int *x;
  /*@only@*/ int *y;
} *pair;  

# include "alias5.lh"

void incx1 (pair p)
{
  pair p2 = p;

  p2->x++; /* 1. Suspect modification of p->x through alias p2->x: p2->x++ */
}

void incx2 (pair p)
{
  pair p2 = p;

  p2 = pair_create ();
  p2->x++;
} /* 2. Fresh storage p2 not released before return */

void incx3 (pair p)
{
  pair p2 = pair_create ();
  p2->x = p->x; /* 3. Only storage p2->x not released before assignment: p2->x = p->x */
  *(p2->x) = 3; /* 4. Suspect modification of *(p->x) through alias *(p2->x): */
  pair_free (p2);
} /* 5. Storage p->x reachable from parameter is kept (should be only) */