2017-10-16 21:28:38 +08:00
|
|
|
# WHAT ARCHITECTURE?
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2015-10-05 23:49:47 +08:00
|
|
|
CPROVER now needs a C++11 compliant compiler and works in the following
|
|
|
|
environments:
|
2011-07-14 19:47:56 +08:00
|
|
|
|
2011-05-11 21:13:55 +08:00
|
|
|
- Linux
|
|
|
|
- MacOS X
|
2014-06-16 21:42:10 +08:00
|
|
|
- Solaris 11
|
2017-03-19 06:13:05 +08:00
|
|
|
- FreeBSD 11
|
2017-10-24 19:24:52 +08:00
|
|
|
- Cygwin
|
|
|
|
- Microsoft Visual Studio
|
2014-11-22 20:46:10 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
The rest of this document is split up into three parts: compilation on Linux,
|
|
|
|
MacOS, Windows. Please read the section appropriate for your machine.
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
# COMPILATION ON LINUX
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2013-12-11 23:03:32 +08:00
|
|
|
We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
1. You need a C/C++ compiler, Flex and Bison, and GNU make.
|
2017-03-19 06:13:05 +08:00
|
|
|
The GNU Make needs to be version 3.81 or higher.
|
2018-06-22 16:35:10 +08:00
|
|
|
On Debian-like distributions, do as root:
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
apt-get install g++ gcc flex bison make git libwww-perl patch
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
On Red Hat/Fedora or derivates, do as root:
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
dnf install gcc gcc-c++ flex bison perl-libwww-perl patch
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-12 22:37:03 +08:00
|
|
|
Note that you need g++ version 5.0 or newer.
|
2018-05-15 23:33:45 +08:00
|
|
|
|
2018-07-26 16:50:43 +08:00
|
|
|
On Amazon Linux and similar distributions, do as root:
|
|
|
|
```
|
|
|
|
yum install gcc72-c++ flex bison perl-libwww-perl patch
|
|
|
|
```
|
|
|
|
|
2018-05-22 23:40:13 +08:00
|
|
|
To compile JBMC, you additionally need the JDK and the java-models-library.
|
2018-06-22 16:35:10 +08:00
|
|
|
For the JDK, on Debian-like distributions, do as root:
|
2018-05-15 23:33:45 +08:00
|
|
|
```
|
2018-06-30 16:08:28 +08:00
|
|
|
apt-get install unzip openjdk-8-jdk
|
2018-05-15 23:33:45 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
On Red Hat/Fedora or derivates, do as root:
|
2018-05-15 23:33:45 +08:00
|
|
|
```
|
2018-06-30 16:08:28 +08:00
|
|
|
dnf install unzip java-1.8.0-openjdk-devel
|
2018-05-22 23:40:13 +08:00
|
|
|
```
|
2018-05-15 23:33:45 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
2. As a user, get the CBMC source via
|
|
|
|
```
|
2016-04-03 00:18:30 +08:00
|
|
|
git clone https://github.com/diffblue/cbmc cbmc-git
|
2018-06-22 16:35:10 +08:00
|
|
|
cd cbmc-git
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
|
|
|
|
3. To compile, do
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
make -C src minisat2-download
|
|
|
|
make -C src
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2017-03-23 16:50:03 +08:00
|
|
|
|
2017-10-15 20:07:15 +08:00
|
|
|
4. Linking against an IPASIR SAT solver
|
|
|
|
|
|
|
|
Get an IPASIR package and build picosat by default
|
|
|
|
```
|
|
|
|
make -C src ipasir-build
|
|
|
|
```
|
|
|
|
|
|
|
|
Build CBMC with IPASIR and link against the ipasir solver library
|
|
|
|
Note: the LIBSOLVER variable could be pointed towards other solvers
|
|
|
|
```
|
|
|
|
make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a
|
|
|
|
```
|
|
|
|
|
2018-06-22 16:35:10 +08:00
|
|
|
5. To compile JBMC, do
|
|
|
|
```
|
2018-07-10 18:21:17 +08:00
|
|
|
make -C jbmc/src setup-submodules
|
2018-06-22 16:35:10 +08:00
|
|
|
make -C jbmc/src
|
|
|
|
```
|
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
# COMPILATION ON SOLARIS 11
|
2013-12-11 23:03:32 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
1. As root, get the necessary development tools:
|
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
pkg install system/header
|
2018-06-19 21:40:37 +08:00
|
|
|
pkgadd -d http://get.opencsw.org/now
|
|
|
|
/opt/csw/bin/pkgutil -U
|
|
|
|
/opt/csw/bin/pkgutil -i gcc5g++ bison flex git
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
|
|
|
2. As a user, get the CBMC source via
|
|
|
|
```
|
2018-06-19 21:40:37 +08:00
|
|
|
export PATH=/opt/csw/bin:$PATH
|
2016-04-03 00:18:30 +08:00
|
|
|
git clone https://github.com/diffblue/cbmc cbmc-git
|
2018-06-22 16:35:10 +08:00
|
|
|
cd cbmc-git
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
3. To compile CBMC, type
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
gmake -C src minisat2-download DOWNLOADER=wget TAR=gtar
|
|
|
|
gmake -C src
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
4. To compile JBMC, type
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-07-10 18:21:17 +08:00
|
|
|
gmake -C jbmc/src setup-submodules
|
2018-06-22 16:35:10 +08:00
|
|
|
gmake -C jbmc/src
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2013-12-11 23:03:32 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
# COMPILATION ON FREEBSD 11
|
2012-10-21 19:15:17 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
1. As root, get the necessary tools:
|
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
pkg install bash gmake git www/p5-libwww patch flex bison
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-05-15 23:33:45 +08:00
|
|
|
To compile JBMC, additionally install
|
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
pkg install openjdk8 wget
|
2018-05-15 23:33:45 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
2. As a user, get the CBMC source via
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2016-04-03 00:18:30 +08:00
|
|
|
git clone https://github.com/diffblue/cbmc cbmc-git
|
2018-06-22 16:35:10 +08:00
|
|
|
cd cbmc-git
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
3. To compile CBMC, do
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
gmake -C src minisat2-download
|
|
|
|
gmake -C src
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
4. To compile JBMC, do
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-07-10 18:21:17 +08:00
|
|
|
gmake -C jbmc/src setup-submodules
|
2018-06-22 16:35:10 +08:00
|
|
|
gmake -C jbmc/src
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2014-11-22 20:46:10 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
# COMPILATION ON MACOS X
|
2012-10-21 19:15:17 +08:00
|
|
|
|
|
|
|
Follow these instructions:
|
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
1. 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
|
|
|
|
```
|
2016-01-13 03:50:20 +08:00
|
|
|
xcode-select --install
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2016-01-13 03:50:20 +08:00
|
|
|
in a terminal window.
|
2017-10-16 21:26:37 +08:00
|
|
|
2. Then get the CBMC source via
|
|
|
|
```
|
2016-04-03 00:18:30 +08:00
|
|
|
git clone https://github.com/diffblue/cbmc cbmc-git
|
2018-06-22 16:35:10 +08:00
|
|
|
cd cbmc-git
|
|
|
|
```
|
|
|
|
3. To compile CBMC, do
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
make -C src minisat2-download
|
|
|
|
make -C src
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
4. To compile JBMC, do
|
|
|
|
```
|
2018-07-10 18:21:17 +08:00
|
|
|
make -C jbmc/src setup-submodules
|
2018-06-22 16:35:10 +08:00
|
|
|
make -C jbmc/src
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2012-10-21 19:15:17 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
# COMPILATION ON WINDOWS
|
2012-10-21 19:15:17 +08:00
|
|
|
|
2017-10-24 19:24:52 +08:00
|
|
|
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.
|
2012-11-15 16:35:16 +08:00
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
Follow these instructions:
|
|
|
|
|
2017-10-24 19:24:52 +08:00
|
|
|
1. First install Cygwin, then from the Cygwin setup facility install the
|
2017-11-28 23:36:10 +08:00
|
|
|
following packages: `flex, bison, tar, gzip, git, make, wget, patch,
|
|
|
|
libwww-perl`.
|
2017-10-24 19:24:52 +08:00
|
|
|
2. Get the CBMC source via
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2017-10-24 19:24:52 +08:00
|
|
|
git clone https://github.com/diffblue/cbmc cbmc-git
|
2018-06-22 16:35:10 +08:00
|
|
|
cd cbmc-git
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
2017-10-24 19:24:52 +08:00
|
|
|
3. Depending on your choice of compiler:
|
2017-10-25 00:09:06 +08:00
|
|
|
1. To compile with Visual Studio, change the second line of `src/config.inc`
|
|
|
|
to
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
|
|
|
BUILD_ENV = MSVC
|
|
|
|
```
|
2017-10-24 19:24:52 +08:00
|
|
|
Open the Developer Command Prompt for Visual Studio, then start the
|
2018-06-22 16:35:10 +08:00
|
|
|
Cygwin shell with
|
|
|
|
```
|
|
|
|
bash.exe -login
|
|
|
|
```
|
2017-10-24 19:24:52 +08:00
|
|
|
2. To compile with MinGW, use Cygwin setup to install a mingw g++ compiler
|
2017-10-25 00:09:06 +08:00
|
|
|
package, i.e. one of `mingw{32,64}-{x86_64,i686}-gcc-g++`. You may also
|
|
|
|
have to adjust the section in `src/common` that defines `CC` and `CXX`
|
|
|
|
for BUILD_ENV = Cygwin.
|
|
|
|
Then start the Cygwin shell.
|
2018-06-30 16:08:28 +08:00
|
|
|
4. To compile CMBC, open the Cygwin shell and type
|
2017-10-24 19:24:52 +08:00
|
|
|
```
|
2018-06-22 16:35:10 +08:00
|
|
|
make -C src DOWNLOADER=wget minisat2-download
|
|
|
|
make -C src
|
2017-10-24 19:24:52 +08:00
|
|
|
```
|
2018-07-10 21:05:20 +08:00
|
|
|
5. To compile JBMC, open the Cygwin shell and type
|
2018-06-30 16:08:28 +08:00
|
|
|
```
|
2018-07-10 18:21:17 +08:00
|
|
|
make -C jbmc/src setup-submodules
|
2018-06-30 16:08:28 +08:00
|
|
|
make -C jbmc/src
|
|
|
|
```
|
2013-03-04 18:02:33 +08:00
|
|
|
|
2013-06-16 23:14:44 +08:00
|
|
|
(Optional) A Visual Studio project file can be generated with the script
|
2017-10-16 21:26:37 +08:00
|
|
|
"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.
|
2014-10-31 02:33:40 +08:00
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
# WORKING WITH CMAKE (EXPERIMENTAL)
|
2017-08-25 01:24:15 +08:00
|
|
|
|
|
|
|
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.
|
2017-11-29 22:30:39 +08:00
|
|
|
On Windows, the CMake build does not depend on Cygwin or MinGW, and doesn't
|
|
|
|
require manual modification of build files.
|
2017-08-25 01:24:15 +08:00
|
|
|
|
2017-10-25 17:46:15 +08:00
|
|
|
1. Ensure you have all the build dependencies installed. Build dependencies are
|
|
|
|
the same as for the makefile build, but with the addition of CMake version
|
|
|
|
3.2 or higher. The installed CMake version can be queried with `cmake
|
2018-05-15 23:33:45 +08:00
|
|
|
--version`. To install cmake:
|
2017-10-25 17:46:15 +08:00
|
|
|
- On Debian-like distributions, do
|
|
|
|
```
|
2018-05-15 23:33:45 +08:00
|
|
|
apt-get install cmake
|
2017-10-25 17:46:15 +08:00
|
|
|
```
|
|
|
|
- On Red Hat/Fedora or derivates, do
|
|
|
|
```
|
2018-05-15 23:33:45 +08:00
|
|
|
yum install cmake
|
2017-10-25 17:46:15 +08:00
|
|
|
```
|
|
|
|
- On macOS, do
|
|
|
|
```
|
|
|
|
xcode-select --install
|
|
|
|
```
|
|
|
|
You shoud also install [Homebrew](https://brew.sh), after which you can
|
|
|
|
run `brew install cmake` to install CMake.
|
2017-11-29 22:30:39 +08:00
|
|
|
- On Windows, ensure you have Visual Studio 2013 or later installed.
|
|
|
|
Then, download CMake from the [official download
|
|
|
|
page](https://cmake.org/download).
|
|
|
|
You'll also need `git` and `patch`, which are both provided by the
|
|
|
|
[git for Windows](git-scm.com/download/win) package.
|
|
|
|
Finally, Windows builds of flex and bison should be installed from
|
|
|
|
[the sourceforge page](sourceforge.net/projects/winflexbison).
|
|
|
|
The easiest way to 'install' these executables is to unzip them and to
|
|
|
|
drop the entire unzipped package into the CBMC source directory.
|
2017-10-25 17:46:15 +08:00
|
|
|
- Use of CMake has not been tested on Solaris or FreeBSD. However, it should
|
|
|
|
be possible to install CMake from the system package manager or the
|
|
|
|
[official download page](https://cmake.org/download) on those systems.
|
|
|
|
The dependencies (as listed in the relevant sections above) will also be
|
|
|
|
required, and should be installed using the suggested methods.
|
|
|
|
2. Navigate to the *top level* folder of the project. This is different from
|
|
|
|
the Makefile build, which requires you to navigate to the `src` directory
|
|
|
|
first.
|
2018-07-10 18:21:17 +08:00
|
|
|
3. Update git submodules:
|
|
|
|
```
|
2018-07-10 22:40:18 +08:00
|
|
|
git submodule update --init
|
2018-07-10 18:21:17 +08:00
|
|
|
```
|
|
|
|
4. Generate build files with CMake:
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
|
|
|
cmake -H. -Bbuild
|
|
|
|
```
|
2017-08-25 01:24:15 +08:00
|
|
|
This command tells CMake to use the configuration in the current directory,
|
2017-10-16 21:26:37 +08:00
|
|
|
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. Run `cmake -G` for a
|
|
|
|
comprehensive list of supported back-ends.
|
2017-08-25 01:24:15 +08:00
|
|
|
|
|
|
|
Generally it is not necessary to manually specify individual compiler or
|
2017-10-16 21:26:37 +08:00
|
|
|
linker flags, as CMake defines a number of "build modes" including Debug and
|
|
|
|
Release modes. To build in a particular mode, add the flag
|
2017-08-25 01:24:15 +08:00
|
|
|
`-DCMAKE_BUILD_TYPE=Debug` (or `Release`) 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.
|
2018-07-10 18:21:17 +08:00
|
|
|
5. Run the build:
|
2017-10-16 21:26:37 +08:00
|
|
|
```
|
|
|
|
cmake --build build
|
|
|
|
```
|
2017-08-25 01:24:15 +08:00
|
|
|
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 invoking
|
|
|
|
`make`, `ninja`, or opening the generated IDE project as appropriate.
|
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
# WORKING WITH ECLIPSE
|
2014-10-31 02:33:40 +08:00
|
|
|
|
|
|
|
To work with Eclipse, do the following:
|
|
|
|
|
2017-10-16 21:26:37 +08:00
|
|
|
1. Select File -> New -> Makefile Project with Existing Code
|
|
|
|
2. Type "cprover" as "Project Name"
|
|
|
|
3. Select the "src" subdirectory as "Existing Code Location"
|
|
|
|
4. Select a toolchain appropriate for your platform
|
|
|
|
5. Click "Finish"
|
|
|
|
6. Select Project -> Build All
|
2017-01-04 21:36:14 +08:00
|
|
|
|