Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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);
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment