10 KiB
WHAT ARCHITECTURE?
CPROVER now needs a C++11 compliant compiler and works in the following environments:
- Linux
- MacOS X
- Solaris 11
- FreeBSD 11
- Cygwin
- Microsoft Visual Studio
The rest of this document is split up into three parts: compilation on Linux, MacOS, Windows. Please read the section appropriate for your machine.
COMPILATION ON LINUX
We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
- You need a C/C++ compiler, Flex and Bison, and GNU make.
The GNU Make needs to be version 3.81 or higher.
On Debian-like distributions, do
On Red Hat/Fedora or derivates, doapt-get install g++ gcc flex bison make git libwww-perl patch
Note that you need g++ version 4.9 or newer.yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
- As a user, get the CBMC source via
git clone https://github.com/diffblue/cbmc cbmc-git
- On Debian or Ubuntu, do
On Redhat/Fedora etc., docd cbmc-git/src make minisat2-download make
cd cbmc-git/src make minisat2-download scl enable devtoolset-6 bash make
COMPILATION ON SOLARIS 11
- As root, get the necessary development tools:
pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git pkg install --accept developer/gcc/gcc-c++-5
- As a user, get the CBMC source via
git clone https://github.com/diffblue/cbmc cbmc-git
- Get MiniSat2 by entering
cd cbmc-git wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz gtar xfz minisat_2.2.1.orig.tar.gz mv minisat2-2.2.1 minisat-2.2.1 (cd minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
- Type
That should do it. To run, you will needcd src; gmake
export LD_LIBRARY_PATH=/usr/gcc/4.9/lib
COMPILATION ON FREEBSD 11
- As root, get the necessary tools:
pkg install bash gmake git www/p5-libwww patch flex bison
- As a user, get the CBMC source via
git clone https://github.com/diffblue/cbmc cbmc-git
- Do
cd cbmc-git/src
- Do
gmake minisat2-download gmake
COMPILATION ON MACOS X
Follow these instructions:
- You need a C/C++ compiler, Flex and Bison, and GNU make. To this end, first
install the XCode from the App-store and then type
in a terminal window.xcode-select --install
- Then get the CBMC source via
git clone https://github.com/diffblue/cbmc cbmc-git
- Then type
cd cbmc-git/src make minisat2-download make
COMPILATION ON WINDOWS
There are two options: the Visual Studio compiler with version 12 (2013) or later, or the MinGW cross compiler with version 5.4 or later. We recommend Visual Studio.
Follow these instructions:
- First install Cygwin, then from the Cygwin setup facility install the
following packages:
flex, bison, tar, gzip, git, make, wget, patch
. - Get the CBMC source via
git clone https://github.com/diffblue/cbmc cbmc-git
- Depending on your choice of compiler:
- To compile with Visual Studio, change the second line of config.inc to
Open the Developer Command Prompt for Visual Studio, then start the Cygwin shell withBUILD_ENV = MSVC
bash.exe -login
- To compile with MinGW, use Cygwin setup to install a mingw g++ compiler
package, i.e. one of
mingw{32,64}-{x86_64,i686}-gcc-g++
. Then start the Cygwin shell.
- To compile with Visual Studio, change the second line of config.inc to
- In the Cygwin shell, type
cd cbmc-git/src make DOWNLOADER=wget minisat2-download make
(Optional) A Visual Studio project file can be generated with the script "generate_vcxproj" that is in the subdirectory "scripts". The project file is helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and can be used for building with MSBuild. Note that you still need to run flex/bison using "make generated_files" before opening the project.
WORKING WITH CMAKE (EXPERIMENTAL)
There is an experimental build based on CMake instead of hand-written makefiles. It should work on a wider variety of systems than the standard makefile build, and can integrate better with IDEs and static-analysis tools.
-
Run
cmake --version
. If you get a command-not-found error, or the installed version is lower than 3.2, go and install a new version. Most Linux distributions have a package for CMake, and Mac users can get it through Homebrew. Windows users should download it manually from cmake.org. -
Create a directory to store your build:
mkdir build
Run this from the top level folder of the project. This is different from the other builds, which require you to
cd src
first. -
Generate build files with CMake:
cmake -H. -Bbuild
This command tells CMake to use the configuration in the current directory, and to generate build files into the
build
directory. This is the point to specify custom build settings, such as compilers and build back-ends. You can use clang (for example) by adding the argument-DCMAKE_CXX_COMPILER=clang++
to the command line. You can also tell CMake to generate IDE projects by supplying the-G
flag. Runcmake -G
for a comprehensive list of supported back-ends.Generally it is not necessary to manually specify individual compiler or linker flags, as CMake defines a number of "build modes" including Debug and Release modes. To build in a particular mode, add the flag
-DCMAKE_BUILD_TYPE=Debug
(orRelease
) to the initial invocation.If you do need to manually add flags, use
-DCMAKE_CXX_FLAGS=...
and-DCMAKE_EXE_LINKER_FLAGS=...
. This is useful for enabling clang's sanitizers.Finally, to enable building universal binaries on macOS, you can pass the flag
-DCMAKE_OSX_ARCHITECTURES=i386;x86_64
. If you don't supply this flag, the build will just be for the architecture of your machine. -
Run the build:
cmake --build build
This command tells CMake to invoke the correct tool to run the build in the
build
directory. You can also use the build back-end directly by invokingmake
,ninja
, or opening the generated IDE project as appropriate.
WORKING WITH ECLIPSE
To work with Eclipse, do the following:
- Select File -> New -> Makefile Project with Existing Code
- Type "cprover" as "Project Name"
- Select the "src" subdirectory as "Existing Code Location"
- Select a toolchain appropriate for your platform
- Click "Finish"
- Select Project -> Build All
CODE COVERAGE
Code coverage metrics are provided using gcov and lcov. Ensure that you have installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for ubuntu lcov is available in the standard apt-get repos.
To get coverage metrics run the following script from the regression directory:
get_coverage.sh
This will:
- Rebuild CBMC with gcov enabled
- Run all the regression tests
- Collate the coverage metrics
- Provide an HTML report of the current coverage
USING CLANG-FORMAT
CBMC uses clang-format to ensure that the formatting of new patches is readable and consistent. There are two main ways of running clang-format: remotely, and locally.
RUNNING CLANG-FORMAT REMOTELY
When patches are submitted to CBMC, they are automatically run through continuous integration (CI). One of the CI checks will run clang-format over the diff that your pull request introduces. If clang-format finds formatting issues at this point, the build will be failed, and a patch will be produced in the CI output that you can apply to your code so that it conforms to the style guidelines.
To apply the patch, copy and paste it into a local file (patch.txt
) and then
run:
patch -p1 -i patch.txt
Now, you can commit and push the formatting fixes.
RUNNING CLANG-FORMAT LOCALLY
INSTALLATION
To avoid waiting until you've made a PR to find formatting issues, you can install clang-format locally and run it against your code as you are working.
Different versions of clang-format have slightly different behaviors. CBMC uses clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and Homebrew. To install on a Unix-like system, try installing using the system package manager:
apt-get install clang-format-3.8 # Run this on Ubuntu, Debian etc.
brew install clang-format@3.8 # Run this on a Mac with Homebrew installed
If your platform doesn't have a package for clang-format, you can download a pre-built binary, or compile clang-format yourself using the appropriate files from the LLVM Downloads page.
An installer for Windows (along with a Visual Studio plugin) can be found at the LLVM Snapshot Builds page.
FORMATTING A RANGE OF COMMITS
Clang-format is distributed with a driver script called git-clang-format-3.8. This script can be used to format git diffs (rather than entire files).
After committing some code, it is recommended to run:
git-clang-format-3.8 upstream/develop
Important: If your branch is based on a branch other than upstream/develop
,
use the name or checksum of that branch instead. It is strongly recommended to
rebase your work onto the tip of the branch it's based on before running
git-clang-format
in this way.
RETROACTIVELY FORMATTING INDIVIDUAL COMMITS
If your works spans several commits and you'd like to keep the formatting correct in each individual commit, you can automatically rewrite the commits with correct formatting.
The following command will stop at each commit in the range and run clang-format on the diff at that point. This rewrites git history, so it's unsafe, and you should back up your branch before running this command:
git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \
-- upstream/develop..HEAD
Important: upstream/develop
should be changed in both places in the
command above if your work is based on a different branch. It is strongly
recommended to rebase your work onto the tip of the branch it's based on before
running git-clang-format
in this way.