A slightly evil example

This is one of the simpler examples from a series of examples designed to be challenging to analyze by method of combining many featuress. 

The goal of this analyzer is to verify the assertions. This example involves interplay between integer constraints and aliasing, and also requires models for the Urn functions.


------------------------------

void func() {
  Urn u1 = new Urn();
  Urn u2 = new Urn();

  u1.putBall();
  u2.putBall();

  assert(u1.countBalls() == 1)
  assert(u2.countBalls() == 1)
  assert(u1.countBalls() == u2.countBalls())

  for (int i = 0; i < 5; i++) {
    u1.putBall()
  }

  assert(u1.countBalls() == 7);
  assert(u1.countBalls() > u2.countBalls());

  Urn *u3 = &u1;

  u3->putBall();

  assert(u1.countBalls() == 8);
  assert(u1.countBalls() > u2.countBalls());

  if (*) {
    u3->putBall();
  }

  assert(8 <= u1.countBalls() <= 9);
  assert(u1.countBalls() > u2.countBalls());

  while(*) {
    u1.putBall();
  }

  assert(u3->countBalls() > u2.countBalls());

  while (u2.countBalls() < u1.countBalls()) {
    u2.putBall();
  }

  assert(u2.countBalls() == u3->countBalls());

  Urn *u4;
  if (*) {
    u4 = &u1;
    u2.putBall();
  } else {
    u4 = &u2;
  }

  if (u2.countBalls() > u1.countBalls()) {
    u4->putBall();
    assert(u1.countBalls() == u2.countBalls());
  }

  u4.putBall();

  assert(u1.countBalls() <= u2.countBalls() <= u1.countBalls() + 1);

}