Skip to content

Latest commit

 

History

History
176 lines (130 loc) · 5.3 KB

README.md

File metadata and controls

176 lines (130 loc) · 5.3 KB
Raw

Testing infrastructure

Boogie uses LLVM's lit tool for testing and the OutputCheck tool. This infrastructure should work on Linux, OSX and Windows.

Setting up the test environment

First make sure you have Python installed. We use Python 3.4 but older versions should work as well.

The lit and OutputCheck tools are both available in PyPi. Install the pip tool if you don't already have have it and then run

$ pip install lit
$ pip install OutputCheck

this will install the tools on your system. If you are running on Linux/OSX and do not have root access then you can use the virtualenv tool to install these tools without the need for root access.

Once installed check the tools are available on your PATH.

$ lit --help
Usage: lit [options] {file-or-path}

Options:
  -h, --help            show this help message and exit
...

$ OutputCheck --help
usage: OutputCheck [-h] [--file-to-check= FILE_TO_CHECK=]
                   [--check-prefix= CHECK_PREFIX=]
                   [-l {debug,info,warning,error}] [--comment= COMMENT=] [-d]
                   [--disable-substitutions]
                   check_file
...

On Windows it may be necessary to add the Python scripts folder (e.g. C:\Python34\Scripts\) to your PATH if the above commands do not work.

Other requirements

We currently require Z3 4. to be used with the test suite.

Running the tests

lit is a very flexible tool. You simply pass it one or more paths to directories or individual tests (usually .bpl files) and lit will build up a list of tests to run.

For example to run the whole test suite run the following command

$ cd Test
$ lit .

For example to run all tests in the test1 folder and the bla1.bpl and constants.bpl test run the following command

$ cd Test
$ lit test0/ livevars/bla1.bpl aitest0/constants.bpl

Note replace / with \ on Windows (tab completion is your friend).

If you would prefer to see less information when running tests you can use the -s flag to show progress information and a summary when tests finish.

$ cd Test
$ lit -s .

To pass additional flags to Boogie when running tests run the following command where -someParameter is a parameter Boogie supports.

$ cd Test
$ lit --param boogie_params='-someParameter' .

For more lit options run

$ lit --help

Debugging failing tests

You can pass the -v flag to get more verbose output to try to determine why certain tests are failing.

$ cd Test
$ lit -v livevars/bla1.bpl

Removing output produced by tests

lit will by default create a folder named Output in each directory that will contain temporary files created by tests. You can run the following to remove all these folders/files.

$ cd Test
$ ./clean.py

This script will also remove old files created by the legacy batch file based testing infrastructure (no longer in source tree). If temporary files are left behind from the old testing infrastructure it is necessary to run this script to remove those files before using lit.

Writing tests

Tests are driven my special comments written in .bpl files (each file is an individual test). These special comments (RUN lines) contain shell commands to run. If any command exits with a non zero exit code the test is considered to fail.

The RUN lines may use several substitutions

  • %boogie expands to the absolute path of the Boogie executable with any set options. This does not need to be quoted.

  • %parallel-boogie expands to the absolute path of the Boogie executable with any set options and /vcsCores:2. This does not need to be quoted.

  • %diff expands to the diff tool being used. This is diff on non Windows platforms and pydiff on Windows. Do not use the fc tool because it is buggy when tests are run concurrently. This does not need to be quoted.

  • %OutputCheck expands to the absolute path to the OutputCheck tool. This does not need to be quoted.

  • %s the absolute path to the current test file. You should make sure this is quoted so that tests work correctly for users who use spaces in their file paths.

  • %T the path to the temporary directory for this test. You should make sure this is quoted.

  • %t expands to the absolute path of a filename that can be used as a temporary file. This always expands to the same value in a single test so if you need multiple different temporary files append a unique value (e.g. %t1, %t2... etc). You should make sure this is quoted.

Currently most tests simply execute boogie recording its output which then compared to a file containing the expected output (.expect files) using %diff. This is incredibly fragile and it is recommended that new tests use the OutputCheck tool instead of relying on %diff.

For more information see

https://llvm.org/docs/CommandGuide/lit.html https://llvm.org/docs/TestingGuide.html#regression-test-structure https://github.com/stp/OutputCheck/blob/master/README.md