blob: 36eb474db900c681cc531d2472c8aec3dc5d5c2b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
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
|
