2 \page compilation-and-development Compilation and Development
4 \author Martin Brain, Peter Schrammel, Owen Jones
6 \section compilation-and-development-section-compilation Compilation
8 The CBMC source code is available on
9 [its GitHub page](https://github.com/diffblue/cbmc).
12 \subsection compilation-and-development-subsection-makefiles Makefiles
14 Instructions for compiling CBMC using makefiles are
16 [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#what-architecture)
17 in the root of the CBMC repository. They cover Linux, Solaris 11,
18 FreeBSD 11, MacOS X and Windows.
21 \subsection compilation-and-development-subsection-cmake-files CMake files
23 There is also support for compiling using CMake. Instructions are
25 [COMPILING.md](https://github.com/diffblue/cbmc/blob/develop/COMPILING.md#working-with-cmake)
26 in the root of the CBMC repository.
29 \subsection compilation-and-development-subsection-personal-configuration Personal configuration
31 \subsubsection compilation-and-development-subsubsection-config-inc config.inc
34 [config.inc](https://github.com/diffblue/cbmc/blob/develop/src/config.inc) and
35 [common](https://github.com/diffblue/cbmc/blob/develop/src/common), are
36 included in every makefile.
37 [config.inc](https://github.com/diffblue/cbmc/blob/develop/src/config.inc)
38 contains configuration options
39 relating to compilation so that they can be conveniently edited in one place.
40 [common](https://github.com/diffblue/cbmc/blob/develop/src/common)
41 contains commands that are needed in every makefile but which the
42 developer is not expected to edit. (There is also
43 [another config.inc](https://github.com/diffblue/cbmc/blob/develop/jbmc/src/config.inc)
44 which is also included in every makefile in the `jbmc` folder.)
46 Note, these files are not involved in the CMake build.
49 \subsubsection compilation-and-development-subsubsection-macro-debug Macro DEBUG
51 If the macro `DEBUG` is defined during compilation of CBMC (for example by
52 using a compiler flag) then extra debug code will be included. This includes
53 print statements and code checking that data structures are as expected.
56 \section compilation-and-development-section-running-tests Running tests
58 \subsection compilation-and-development-subsection-regression-tests Regression tests
60 The regression tests are contained in `regression/` and `jbmc/regression/`.
61 Inside these folders there is a directory for each of the modules. Each
62 of these contains multiple test directories, with names describing
63 what they test. When there are multiple tests in a test directory then
64 they should all test very similar aspects of the program's behaviour. Each
65 test directory contains input files and one or more test description files,
66 which have the ending `.desc`. The test description files specify what command
67 to run, what output is expected and so on. The test framework is a
69 [test.pl](https://github.com/diffblue/cbmc/blob/develop/regression/test.pl),
70 located in `regression/test.pl`.
72 The `--help` option to `test.pl` outlines the
73 format of the test description files. Most importantly, the first word in a
74 test description file is its level, which is one of: `CORE` (should be run in
75 CI, should succeed), `THOROUGH` (takes too long to be run in CI, should
76 succeed), `FUTURE` (will succeed when a planned feature is added) or
77 `KNOWNBUG` (will succeed when a bug is fixed).
79 \subsubsection compilation-and-development-subsubsection-running-regression-tests-with-make Running regression tests with make
81 If you have compiled using `make` then you can run the regression tests
82 using `make test`. Run it from `regression/` to run all the regression tests,
83 or any of its subfolders to just run the tests for that module. The number
84 of tests that are run in parallel can be controlled through the environment
85 variable `TESTPL_JOBS`.
87 If you have not compiled using `make` then this won't work, because the
88 makefile is expecting to find binaries like `cbmc` and `jbmc` in the source
91 \subsubsection compilation-and-development-subsubsection-running-regression-tests-with-ctest Running regression tests with CTest
93 If you have compiled using CMake then you can run the regression tests using
94 CTest. (Note: this will also run the unit tests.)
96 Here are two example commands, to be run from the `build/` directory:
98 ctest -V -L CORE -R cpp
99 ctest -V -L CORE -R cpp -E cbmc-cpp
101 `-V` makes it print out more
102 useful output. `-L CORE` makes it only run tests that have been tagged
103 `CORE`. `-R regular_expression` can be used to limit which tests are run to
104 those which match the given regular expression, and `-E regex` excludes tests
105 to those which match the given regular expression.
106 So the first command will run all the CORE tests in `regression/cbmc/cpp` and
107 `regression/cbmc/cbmc-cpp`, and the second will run all the CORE tests in
108 `regression/cbmc/cpp` only. Another useful option is `-N`, which makes CTest
109 list which tests it will run without actually running them.
112 \subsubsection compilation-and-development-subsubsection-running-individual-regression-tests-directly-with-test-pl Running individual regression tests directly with test.pl
114 It can be useful to run a single test folder in isolation. This can be done by
115 running `regression/test.pl` directly. The way that `test.pl` is run varies between the
116 different modules, and can be ascertained by looking at the `test` target in
117 the makefile. The simple case is when there isn't a file called `chain.sh`.
118 Then you can directly run `test.pl` on a single test folder with the
119 following command from the module directory (note that it is recommended to
120 use absolute paths as it avoids many issues, e.g. the path to the binary
121 should be relative to `<test-folder>`):
123 <absolute-path-to-test.pl> -p -c <absolute-path-to-binary> <test-folder>
125 `-p` makes it print a log of failed tests and `-c` tells it where to find the
126 binary to run, e.g. `cbmc`, `jbmc` or `goto-analyzer`.
127 If `<test-folder>` is not provided then all test directories are run. The
128 `--help` option lists all command line options, including `-j` for running
129 multiple tests in parallel and `-C`, `-T`, `-F` and `-K` for controlling
130 whether `CORE`, `THOROUGH`, `FUTURE` or `KNOWNBUG` tests are run.
132 When there is a file called `chain.sh` then the command should look like
134 <absolute-path-to-test.pl> -p -c '<absolute-path-to-chain-sh> <arg-1> ... <arg-n>' <test-folder>
136 Note that the test binary and its initial command line arguments are a single
137 value for the -c option, so they must be be wrapped in quotes if they contain
138 any unescaped spaces. What to put for the
139 arguments `<arg-1>` to `<arg-n>` varies from module to module. To find
140 out, look in `chain.sh` and see what arguments it expects. You can also look in
141 the `Makefile` and see how it calls `chain.sh` in the `test` target.
144 \subsection compilation-and-development-subsection-unit-tests Unit tests
146 The unit tests are contained in the `unit/` folder. They are written using the
147 [Catch](https://github.com/philsquared/Catch) unit test framework.
149 If you have compiled with `make`, you can run the unit tests for CBMC directly
150 by going to `unit/`, running `make` to compile the unit tests and then
151 `make test` to run them. You can run the unit tests for JBMC directly by going
152 to `jbmc/unit/` and running the same commands.
154 If you have compiled with CMake, you can run the unit tests for CBMC directly
155 by going to `unit/` and running
157 ../<build-folder>/bin/unit
159 and you can run the unit tests for JBMC directly by going to `jbmc/unit/` and
162 ../../<build-folder>/bin/java-unit
164 If you have compiled with CMake you can also run the unit tests through CTest,
165 with the names `unit` and `java-unit`. So, from the `build/` directory, run
167 ctest -V -L CORE -R ^unit
168 ctest -V -L CORE -R java-unit
170 to run the CBMC unit tests and the JBMC unit tests respectively. (The `^` is
171 needed to make it a regular expression that matches `unit` but not `java-unit`.)
173 Note that some tests run which are expected to fail - see the summary at
174 the end of the run to see how many tests passed, how many failed which were
175 expected to and how many tests failed which were not expected to.
177 For more information on the structure of `unit/` and how to tag tests, see
178 [the section on unit tests in `CODING_STANDARD.md` in the root of the CBMC
179 repository](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#unit-tests)
182 \subsection compilation-and-development-subsection-sat-solver Using a different SAT solver
184 By default, CBMC will assume MiniSat 2 as the SAT back-end. Several other
185 solvers are supported (see also
186 [config.inc](compilation-and-development-subsubsection-config-inc) above). As a
187 more general option, which is not limited to a single SAT solver, you may use
188 the IPASIR interface. For example, to use the SAT solver RISS, proceed as
191 1) Build RISS (in particular its IPASIR configuration):
193 git clone https://github.com/conp-solutions/riss riss.git
198 make riss-coprocessor-lib-static
201 2) Build CBMC while enabling the IPASIR back-end:
202 make -C src IPASIR=../../riss.git/riss \
203 LIBS="../../riss.git/build/lib/libriss-coprocessor.a -lpthread"
205 3) Run CBMC - note that RISS is highly configurable via the RISSCONFIG
206 environment variable:
207 export RISSCONFIG=VERBOSE:BMC1
211 \section compilation-and-development-section-documentation Documentation
213 Apart from the (user-orientated) CBMC user manual and this document, most
214 of the rest of the documentation is inline in the code as `doxygen` and
215 some comments. A man page for CBMC, goto-cc and goto-instrument is
216 contained in the `doc/` directory and gives some options for these
217 tools. All of these could be improved and patches are very welcome. In
218 some cases the algorithms used are described in the relevant papers.
220 The doxygen documentation can be [accessed online](http://cprover.diffblue.com).
221 To build it locally, run `scripts/run_doxygen.sh`. HTML output will be created
222 in `doc/html/`. The index page is `doc/html/index.html`. This script will
223 filter out expected warning messages from doxygen, so that new problems are more
224 obvious. It is important to use the correct version of doxygen, as specified
225 in `run_doxygen.sh`, so that there are no unexpected changes to the list of
226 expected warnings. In the event that any change fixes an old warning, then the
227 corresponding line(s) should be deleted from
228 `scripts/expected_doxygen_warnings.txt`. We want to avoid adding any more
229 warnings to this list of expected warnings, but that can be done to work around
230 limitations in Doxygen (where the code and documentation are completely correct).
233 \section compilation-and-development-section-formatting Formatting
236 href="https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md">
237 `CODING_STANDARD.md`</a> file in the root of the CBMC repository contains
238 guidance on how to write code for the CBMC repository. This includes
239 which language features can be used and formatting rules.
241 C++ code can be automatically reformatted in the correct way by running
242 `clang-format`. There are more details in
243 [CODING_STANDARD.md](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#using-clang-format).
246 \section compilation-and-development-section-linting Linting
248 There is also a linting script, `scripts/cpplint.py`. There is a wrapper
249 script to run `cpplint.py` only on lines that differ from another
250 branch, e.g. to run it on lines that have been changed from `develop`:
252 scripts/run_lint.sh develop
254 There are also instructions for adding this as a git pre-commit hook in
255 [CODING_STANDARD.md](https://github.com/diffblue/cbmc/blob/develop/CODING_STANDARD.md#pre-commit-hook-to-run-cpplint-locally).