Boogie's new testing infrastructure (lit) is now in Boogie's default branch. I plan to remove the old testing infrastructure
soon but I'd like to give a little time for Boogie users to try out the new infrastructure and fix a few remaining issues.
I've written a
little documentation on the new infrastructure
. The new infrastructure is vastly superior to the old batch file infrastructure. Please try it out.
I've kept the old batch file testing scripts functioning (for now) so that it is possible to run either infrastructure on Windows. However both infrastructures use the same name (
) for their temporary output which causes problems if you run
one infrastructure and then try to run the other. To work around this please run the
script before switching between the testing infrastructures. This issue will go away as soon as we kill the old testing infrastructure
The following tests currently fail for the lit testing infrastructure
Failing Tests (10):
Boogie :: og/DeviceCacheSimplified.bpl
Boogie :: og/DeviceCacheWithBuffer.bpl
Boogie :: og/async.bpl
Boogie :: og/houd1.bpl
Boogie :: og/lock-introduced.bpl
Boogie :: og/termination.bpl
Boogie :: og/treiber-stack.bpl
Boogie :: test15/CaptureState.bpl
Boogie :: test21/Maps2.bpl
Boogie :: test21/test3_AddMethod_conv.bpl
does not fail on Windows using Z3 4.1 (http://research.microsoft.com/en-us/downloads/0a7db466-c2d7-4c51-8246-07e25900c7e7/
I tried using Z3 4.1.1 on Linux (https://github.com/delcypher/z3/tree/4.1.1-fixed
) and it's still broken. I'm not convinced they are actually the same version because the reported
version of the Z3 build on linux is
despite me taking this from the
git tag. Basically we need to agree on a common version of Z3 available to all users and fix this test.
All other tests listed above basically fail because someone left them in the repository but they were not being run in the old infrastructure! So I've left these tests partially implemented until we decide what to do with these.
There are also a bunch of test directories (
) that are currently disabled because they were broken (as far as could tell) in the old infrastructure.
is aware of these tests but I've instructed it to treat these directories as unsupported tests for now. If these tests are of no use they should be removed.