1- What architecture?
2- ------------------
1+ # What architecture?
32
43CPROVER now needs a C++11 compliant compiler and works in the following
54environments:
65
76- Linux
8-
97- MacOS X
10-
118- Solaris 11
12-
139- FreeBSD 11
10+ - Cygwin (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or
11+ above.)
12+ - Microsoft's Visual Studio version 12 (2013), version 14 (2015), or version 15
13+ (older versions won't work)
1414
15- - Cygwin
16- (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or above.)
17-
18- - Microsoft's Visual Studio version 12 (2013), version 14 (2015),
19- or version 15 (older versions won't work)
20-
21- The rest of this document is split up into three parts: compilation on
22- Linux, MacOS, Windows. Please read the section appropriate for your
23- machine.
15+ The rest of this document is split up into three parts: compilation on Linux,
16+ MacOS, Windows. Please read the section appropriate for your machine.
2417
25-
26- COMPILATION ON LINUX
27- --------------------
18+ # COMPILATION ON LINUX
2819
2920We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
3021
31- 0) You need a C/C++ compiler, Flex and Bison, and GNU make.
22+ 1 . You need a C/C++ compiler, Flex and Bison, and GNU make.
3223 The GNU Make needs to be version 3.81 or higher.
3324 On Debian-like distributions, do
34-
25+ ```
3526 apt-get install g++ gcc flex bison make git libwww-perl patch
36-
27+ ```
3728 On Red Hat/Fedora or derivates, do
38-
29+ ```
3930 yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
40-
31+ ```
4132 Note that you need g++ version 4.9 or newer.
42-
43- 1) As a user, get the CBMC source via
44-
33+ 2 . As a user, get the CBMC source via
34+ ```
4535 git clone https://github.com/diffblue/cbmc cbmc-git
46-
47- 2) On Debian or Ubuntu, do
48-
36+ ```
37+ 3 . On Debian or Ubuntu, do
38+ ```
4939 cd cbmc-git/src
5040 make minisat2-download
5141 make
52-
42+ ```
5343 On Redhat/Fedora etc., do
54-
44+ ```
5545 cd cbmc-git/src
5646 make minisat2-download
5747 scl enable devtoolset-6 bash
5848 make
49+ ```
5950
51+ # COMPILATION ON SOLARIS 11
6052
61- COMPILATION ON SOLARIS 11
62- -------------------------
63-
64- 1) As root, get the necessary development tools:
65-
53+ 1 . As root, get the necessary development tools:
54+ ```
6655 pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git
6756 pkg install --accept developer/gcc/gcc-c++-5
68-
69- 2) As a user, get the CBMC source via
70-
57+ ```
58+ 2 . As a user, get the CBMC source via
59+ ```
7160 git clone https://github.com/diffblue/cbmc cbmc-git
72-
73- 3) Get MiniSat2 by entering
74-
61+ ```
62+ 3 . Get MiniSat2 by entering
63+ ```
7564 cd cbmc-git
7665 wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
7766 gtar xfz minisat_2.2.1.orig.tar.gz
7867 mv minisat2-2.2.1 minisat-2.2.1
7968 (cd minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch)
80-
81- 4) Type
82-
69+ ```
70+ 4 . Type
71+ ```
8372 cd src; gmake
84-
73+ ```
8574 That should do it. To run, you will need
86-
75+ ```
8776 export LD_LIBRARY_PATH=/usr/gcc/4.9/lib
77+ ```
8878
79+ # COMPILATION ON FREEBSD 11
8980
90- COMPILATION ON FREEBSD 11
91- -------------------------
92-
93- 1) As root, get the necessary tools:
94-
81+ 1 . As root, get the necessary tools:
82+ ```
9583 pkg install bash gmake git www/p5-libwww patch flex bison
96-
97- 2) As a user, get the CBMC source via
98-
84+ ```
85+ 2 . As a user, get the CBMC source via
86+ ```
9987 git clone https://github.com/diffblue/cbmc cbmc-git
100-
101- 3) Do
102-
88+ ```
89+ 3 . Do
90+ ```
10391 cd cbmc-git/src
104-
105- 4) Do
106-
92+ ```
93+ 4 . Do
94+ ```
10795 gmake minisat2-download
10896 gmake
97+ ```
10998
110-
111- COMPILATION ON MACOS X
112- ----------------------
99+ # COMPILATION ON MACOS X
113100
114101Follow these instructions:
115102
116- 0) You need a C/C++ compiler, Flex and Bison, and GNU make. To this
117- end, first install the XCode from the App-store and then type
118-
103+ 1 . You need a C/C++ compiler, Flex and Bison, and GNU make. To this end, first
104+ install the XCode from the App-store and then type
105+ ```
119106 xcode-select --install
120-
107+ ```
121108 in a terminal window.
122-
123- 1) Then get the CBMC source via
124-
109+ 2 . Then get the CBMC source via
110+ ```
125111 git clone https://github.com/diffblue/cbmc cbmc-git
126-
127- 2) Then type
128-
112+ ```
113+ 3 . Then type
114+ ```
129115 cd cbmc-git/src
130116 make minisat2-download
131117 make
118+ ```
132119
120+ # COMPILATION ON WINDOWS
133121
134- COMPILATION ON WINDOWS
135- ----------------------
136-
137- There are two options: compilation using g++ from Cygwin, or using
138- Visual Studio's compiler. As Cygwin has significant overhead during
139- process creation, we advise you use Visual Studio.
122+ There are two options: compilation using g++ from Cygwin, or using Visual
123+ Studio's compiler. As Cygwin has significant overhead during process creation,
124+ we advise you use Visual Studio.
140125
141126Follow these instructions:
142127
143- 0) You need a C/C++ compiler, Flex and Bison, GNU tar, gzip2,
144- GNU make, and patch. The GNU Make needs to be version 3.81 or
145- higher. If you don't already have the above, we recommend you install
146- Cygwin.
147-
148- 1) You need a SAT solver (in source). We recommend MiniSat2. Using a
128+ 1 . You need a C/C++ compiler, Flex and Bison, GNU tar, gzip2, GNU make, and
129+ patch. The GNU Make needs to be version 3.81 or higher. If you don't
130+ already have the above, we recommend you install Cygwin.
131+ 2 . You need a SAT solver (in source). We recommend MiniSat2. Using a
149132 browser, download from
150-
133+ ```
151134 http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz
152-
135+ ```
153136 and then unpack with
154-
137+ ```
155138 tar xfz minisat-2.2.1.tar.gz
156139 mv minisat minisat-2.2.1
157140 cd minisat-2.2.1
158141 patch -p1 < ../scripts/minisat-2.2.1-patch
159-
160- The patch removes the dependency on zlib and prevents a problem
161- with a header file that is often unavailable on Windows.
162-
163- 2A) To compile with Cygwin, install the mingw compilers, and adjust
164- the second line of config.inc to say
165-
166- BUILD_ENV = MinGW
167-
168- 2B) To compile with Visual Studio, make sure you have at least Visual
169- Studio version 12 (2013), and adjust the second line of config.inc to say
170-
171- BUILD_ENV = MSVC
172-
173- Open the Visual Studio Command prompt, and then bash.exe -login from
174- Cygwin from in there.
175-
176- 3) Type cd src; make - that should do it.
177-
142+ ```
143+ The patch removes the dependency on zlib and prevents a problem with a
144+ header file that is often unavailable on Windows.
145+ 1 . To compile with Cygwin, install the mingw compilers, and adjust
146+ the second line of config.inc to say
147+ ```
148+ BUILD_ENV = MinGW
149+ ```
150+ 2. To compile with Visual Studio, make sure you have at least Visual
151+ Studio version 12 (2013), and adjust the second line of config.inc to say
152+ ```
153+ BUILD_ENV = MSVC
154+ ```
155+ Open the Visual Studio Command prompt, and then bash.exe -login from
156+ Cygwin from in there.
157+ 3. Type cd src; make - that should do it.
178158
179159(Optional) A Visual Studio project file can be generated with the script
180- "generate_vcxproj" that is in the subdirectory "scripts". The project file
181- is helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and
182- can be used for building with MSBuild. Note that you still need to run
183- flex/bison using "make generated_files" before opening the project.
184-
160+ "generate_vcxproj" that is in the subdirectory "scripts". The project file is
161+ helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and can
162+ be used for building with MSBuild. Note that you still need to run flex/bison
163+ using "make generated_files" before opening the project.
185164
186- WORKING WITH CMAKE (EXPERIMENTAL)
187- ---------------------------------
165+ # WORKING WITH CMAKE (EXPERIMENTAL)
188166
189167There is an experimental build based on CMake instead of hand-written
190168makefiles. It should work on a wider variety of systems than the standard
191169makefile build, and can integrate better with IDEs and static-analysis tools.
192170
193- 0) Run `cmake --version`. If you get a command-not-found error, or the installed
194- version is lower than 3.2, go and install a new version. Most Linux
195- distributions have a package for CMake, and Mac users can get it through
196- Homebrew. Windows users should download it manually from cmake.org.
197-
198- 1) Create a directory to store your build:
199- `mkdir build`
171+ 1. Run `cmake --version`. If you get a command-not-found error, or the
172+ installed version is lower than 3.2, go and install a new version. Most
173+ Linux distributions have a package for CMake, and Mac users can get it
174+ through Homebrew. Windows users should download it manually from cmake.org.
175+ 2. Create a directory to store your build:
176+ ```
177+ mkdir build
178+ ```
200179 Run this from the *top level* folder of the project. This is different from
201180 the other builds, which require you to `cd src` first.
202-
203- 2) Generate build files with CMake:
204- `cmake -H. -Bbuild`
181+ 3. Generate build files with CMake:
182+ ```
183+ cmake -H. -Bbuild
184+ ```
205185 This command tells CMake to use the configuration in the current directory,
206- and to generate build files into the `build` directory.
207- This is the point to specify custom build settings, such as compilers and
208- build back-ends. You can use clang (for example) by adding the argument
209- `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell
210- CMake to generate IDE projects by supplying the `-G` flag.
211- Run `cmake -G` for a comprehensive list of supported back-ends.
186+ and to generate build files into the `build` directory. This is the point
187+ to specify custom build settings, such as compilers and build back-ends. You
188+ can use clang (for example) by adding the argument
189+ `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell CMake
190+ to generate IDE projects by supplying the `-G` flag. Run `cmake -G` for a
191+ comprehensive list of supported back-ends.
212192
213193 Generally it is not necessary to manually specify individual compiler or
214- linker flags, as CMake defines a number of "build modes" including Debug
215- and Release modes. To build in a particular mode, add the flag
194+ linker flags, as CMake defines a number of "build modes" including Debug and
195+ Release modes. To build in a particular mode, add the flag
216196 `-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation.
217197
218198 If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and
@@ -222,44 +202,35 @@ makefile build, and can integrate better with IDEs and static-analysis tools.
222202 Finally, to enable building universal binaries on macOS, you can pass the
223203 flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
224204 the build will just be for the architecture of your machine.
225-
226- 3) Run the build:
227- `cmake --build build`
205+ 4. Run the build:
206+ ```
207+ cmake --build build
208+ ```
228209 This command tells CMake to invoke the correct tool to run the build in the
229210 `build` directory. You can also use the build back-end directly by invoking
230211 `make`, `ninja`, or opening the generated IDE project as appropriate.
231212
232-
233- WORKING WITH ECLIPSE
234- --------------------
213+ # WORKING WITH ECLIPSE
235214
236215To work with Eclipse, do the following:
237216
238- 1) Select File -> New -> Makefile Project with Existing Code
239-
240- 2) Type "cprover" as "Project Name"
241-
242- 3) Select the "src" subdirectory as "Existing Code Location"
243-
244- 4) Select a toolchain appropriate for your platform
245-
246- 5) Click "Finish"
247-
248- 6) Select Project -> Build All
249-
250-
251- CODE COVERAGE
252- -------------
253-
254- Code coverage metrics are provided using gcov and lcov. Ensure that you
255- have installed lcov from http://ltp.sourceforge.net/coverage/lcov.php
256- note for ubuntu lcov is available in the standard apt-get repos.
217+ 1. Select File -> New -> Makefile Project with Existing Code
218+ 2. Type "cprover" as "Project Name"
219+ 3. Select the "src" subdirectory as "Existing Code Location"
220+ 4. Select a toolchain appropriate for your platform
221+ 5. Click "Finish"
222+ 6. Select Project -> Build All
257223
258- To get coverage metrics run the following script from the regression
259- directory:
224+ # CODE COVERAGE
260225
261- get_coverage.sh
226+ Code coverage metrics are provided using gcov and lcov. Ensure that you have
227+ installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for
228+ ubuntu lcov is available in the standard apt-get repos.
262229
230+ To get coverage metrics run the following script from the regression directory:
231+ ```
232+ get_coverage.sh
233+ ```
263234This will:
264235 1) Rebuild CBMC with gcov enabled
265236 2) Run all the regression tests
0 commit comments