extern /*@only@*/ int *new_ip (void);

/*@only@*/ int *f(void)
{
  int *x = new_ip ();
  int *y;

  if (3 > 4)
    {
      y = x;
    }
  else
    {
      free (x);
      y = new_ip ();
    }

  return y;
}


syntax highlighted by Code2HTML, v. 0.9.1