diff options
Diffstat (limited to 'Test/README.md')
-rw-r--r-- | Test/README.md | 348 |
1 files changed, 174 insertions, 174 deletions
diff --git a/Test/README.md b/Test/README.md index 36eb474d..6e315d13 100644 --- a/Test/README.md +++ b/Test/README.md @@ -1,174 +1,174 @@ -Testing infrastructure
-----------------------
-
-Boogie uses LLVM's [lit tool](http://llvm.org/docs/CommandGuide/lit.html) for
-testing and the [OutputCheck tool](https://github.com/stp/OutputCheck). 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](https://pypi.python.org/pypi). Install the
-[pip](http://pip.readthedocs.org/en/latest/installing.html) 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](http://virtualenv.readthedocs.org/en/latest/) 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.<FIXME> 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 completition 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 ``-someParamter`` is a paramter 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
-certains 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 to the Boogie executable with any set
- options and prefixed by ``mono`` on non Windows platforms. 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
-
-http://llvm.org/docs/CommandGuide/lit.html
-http://llvm.org/docs/TestingGuide.html#regression-test-structure
-https://github.com/stp/OutputCheck/blob/master/README.md
+Testing infrastructure +---------------------- + +Boogie uses LLVM's [lit tool](http://llvm.org/docs/CommandGuide/lit.html) for +testing and the [OutputCheck tool](https://github.com/stp/OutputCheck). 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](https://pypi.python.org/pypi). Install the +[pip](http://pip.readthedocs.org/en/latest/installing.html) 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](http://virtualenv.readthedocs.org/en/latest/) 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.<FIXME> 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 completition 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 ``-someParamter`` is a paramter 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 +certains 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 to the Boogie executable with any set + options and prefixed by ``mono`` on non Windows platforms. 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 + +http://llvm.org/docs/CommandGuide/lit.html +http://llvm.org/docs/TestingGuide.html#regression-test-structure +https://github.com/stp/OutputCheck/blob/master/README.md |