Skip to content

Commit 001f684

Browse files
kroeningkroening
committed
fix compilation instructions
1 parent 8f6dab8 commit 001f684

File tree

2 files changed

+147
-145
lines changed

2 files changed

+147
-145
lines changed

‎CODING_STANDARD.md‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -240,3 +240,97 @@ or use a symbolic link. Then, when running git commit, you should get the
240240
linter output (if any) before being prompted to enter a commit message. To
241241
bypass the check (e.g. if there was a false positive), add the option
242242
`--no-verify`.
243+
244+
# CODE COVERAGE
245+
246+
Code coverage metrics are provided using gcov and lcov. Ensure that you have
247+
installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for
248+
ubuntu lcov is available in the standard apt-get repos.
249+
250+
To get coverage metrics run the following script from the regression directory:
251+
```
252+
get_coverage.sh
253+
```
254+
This will:
255+
1) Rebuild CBMC with gcov enabled
256+
2) Run all the regression tests
257+
3) Collate the coverage metrics
258+
4) Provide an HTML report of the current coverage
259+
260+
# USING CLANG-FORMAT
261+
262+
CBMC uses clang-format to ensure that the formatting of new patches is readable
263+
and consistent. There are two main ways of running clang-format: remotely, and
264+
locally.
265+
266+
## RUNNING CLANG-FORMAT REMOTELY
267+
268+
When patches are submitted to CBMC, they are automatically run through
269+
continuous integration (CI). One of the CI checks will run clang-format over
270+
the diff that your pull request introduces. If clang-format finds formatting
271+
issues at this point, the build will be failed, and a patch will be produced
272+
in the CI output that you can apply to your code so that it conforms to the
273+
style guidelines.
274+
275+
To apply the patch, copy and paste it into a local file (`patch.txt`) and then
276+
run:
277+
```
278+
patch -p1 -i patch.txt
279+
```
280+
Now, you can commit and push the formatting fixes.
281+
282+
## RUNNING CLANG-FORMAT LOCALLY
283+
284+
### INSTALLATION
285+
286+
To avoid waiting until you've made a PR to find formatting issues, you can
287+
install clang-format locally and run it against your code as you are working.
288+
289+
Different versions of clang-format have slightly different behaviors. CBMC uses
290+
clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and
291+
Homebrew.
292+
To install on a Unix-like system, try installing using the system package
293+
manager:
294+
```
295+
apt-get install clang-format-3.8 # Run this on Ubuntu, Debian etc.
296+
brew install [email protected] # Run this on a Mac with Homebrew installed
297+
```
298+
299+
If your platform doesn't have a package for clang-format, you can download a
300+
pre-built binary, or compile clang-format yourself using the appropriate files
301+
from the [LLVM Downloads page](http://releases.llvm.org/download.html).
302+
303+
An installer for Windows (along with a Visual Studio plugin) can be found at
304+
the [LLVM Snapshot Builds page](http://llvm.org/builds/).
305+
306+
### FORMATTING A RANGE OF COMMITS
307+
308+
Clang-format is distributed with a driver script called git-clang-format-3.8.
309+
This script can be used to format git diffs (rather than entire files).
310+
311+
After committing some code, it is recommended to run:
312+
```
313+
git-clang-format-3.8 upstream/develop
314+
```
315+
*Important:* If your branch is based on a branch other than `upstream/develop`,
316+
use the name or checksum of that branch instead. It is strongly recommended to
317+
rebase your work onto the tip of the branch it's based on before running
318+
`git-clang-format` in this way.
319+
320+
### RETROACTIVELY FORMATTING INDIVIDUAL COMMITS
321+
322+
If your works spans several commits and you'd like to keep the formatting
323+
correct in each individual commit, you can automatically rewrite the commits
324+
with correct formatting.
325+
326+
The following command will stop at each commit in the range and run
327+
clang-format on the diff at that point. This rewrites git history, so it's
328+
*unsafe*, and you should back up your branch before running this command:
329+
```
330+
git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \
331+
-- upstream/develop..HEAD
332+
```
333+
*Important*: `upstream/develop` should be changed in *both* places in the
334+
command above if your work is based on a different branch. It is strongly
335+
recommended to rebase your work onto the tip of the branch it's based on before
336+
running `git-clang-format` in this way.

‎COMPILING.md‎

Lines changed: 53 additions & 145 deletions
Original file line numberDiff line numberDiff line change
@@ -19,47 +19,36 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
1919

2020
1. You need a C/C++ compiler, Flex and Bison, and GNU make.
2121
The GNU Make needs to be version 3.81 or higher.
22-
On Debian-like distributions, do
22+
On Debian-like distributions, do as root:
2323
```
24-
apt-get install g++ gcc flex bison make git libwww-perl patch openjdk-7-jdk
24+
apt-get install g++ gcc flex bison make git libwww-perl patch
2525
```
26-
On Red Hat/Fedora or derivates, do
26+
On Red Hat/Fedora or derivates, do as root:
2727
```
28-
yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
28+
dnf install gcc gcc-c++ flex bison perl-libwww-perl patch
2929
```
3030
Note that you need g++ version 5.0 or newer.
3131

3232
To compile JBMC, you additionally need the JDK and the java-models-library.
33-
34-
For the JDK, on Debian-like distributions, do
35-
```
36-
apt-get install openjdk-7-jdk
33+
For the JDK, on Debian-like distributions, do as root:
3734
```
38-
On Red Hat/Fedora or derivates, do
35+
apt-get install openjdk-8-jdk
3936
```
40-
yum install java-1.7.0-openjdk-devel
37+
On Red Hat/Fedora or derivates, do as root:
4138
```
42-
For the models library, do
43-
```
44-
make -C jbmc/src java-models-library-download
39+
dnf install java-1.8.0-openjdk-devel
4540
```
4641

4742
2. As a user, get the CBMC source via
4843
```
4944
git clone https://github.com/diffblue/cbmc cbmc-git
45+
cd cbmc-git
5046
```
51-
3. On Debian or Ubuntu, do
52-
```
53-
cd cbmc-git/src
54-
make minisat2-download
55-
make
56-
```
57-
On Redhat/Fedora etc., do
47+
48+
3. To compile, do
5849
```
59-
cd cbmc-git/src
60-
make minisat2-download
61-
scl enable devtoolset-6 bash
62-
make
50+
make -C src minisat2-download
51+
make -C src
6352
```
6453

6554
4. Linking against an IPASIR SAT solver
@@ -75,10 +64,17 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
7564
make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a
7665
```
7766

67+
5. To compile JBMC, do
68+
```
69+
make -C jbmc/src java-models-library-download
70+
make -C jbmc/src
71+
```
72+
7873
# COMPILATION ON SOLARIS 11
7974

8075
1. As root, get the necessary development tools:
8176
```
77+
pkg install system/header
8278
pkgadd -d http://get.opencsw.org/now
8379
/opt/csw/bin/pkgutil -U
8480
/opt/csw/bin/pkgutil -i gcc5g++ bison flex git
@@ -87,43 +83,43 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
8783
```
8884
export PATH=/opt/csw/bin:$PATH
8985
git clone https://github.com/diffblue/cbmc cbmc-git
86+
cd cbmc-git
9087
```
91-
3. Get MiniSat2 by entering
92-
```
93-
cd cbmc-git/src
94-
gmake minisat2-download DOWNLOADER=wget TAR=gtar
95-
```
96-
4. To compile, type
88+
3. To compile CBMC, type
9789
```
98-
gmake
90+
gmake -C src minisat2-download DOWNLOADER=wget TAR=gtar
91+
gmake -C src
9992
```
100-
That should do it. To run, you will need
93+
4. To compile JBMC, type
10194
```
102-
export LD_LIBRARY_PATH=/usr/gcc/5.0/lib
95+
gmake -C jbmc/src java-models-library-download
96+
gmake -C jbmc/src
10397
```
10498

10599
# COMPILATION ON FREEBSD 11
106100

107101
1. As root, get the necessary tools:
108102
```
109-
pkg install bash gmake git www/p5-libwww patch flex bison openjdk
103+
pkg install bash gmake git www/p5-libwww patch flex bison
110104
```
111105
To compile JBMC, additionally install
112106
```
113-
pkg install openjdk
107+
pkg install openjdk8 wget
114108
```
115-
2. As a user, get the CBMC source via
109+
2. As a user, get the CBMC source via
116110
```
117111
git clone https://github.com/diffblue/cbmc cbmc-git
112+
cd cbmc-git
118113
```
119-
3. Do
114+
3. To compile CBMC, do
120115
```
121-
cd cbmc-git/src
116+
gmake -C src minisat2-download
117+
gmake -C src
122118
```
123-
4. Do
119+
4. To compile JBMC, do
124120
```
125-
gmake minisat2-download
126-
gmake
121+
gmake -C jbmc/src java-models-library-download
122+
gmake -C jbmc/src
127123
```
128124

129125
# COMPILATION ON MACOS X
@@ -139,12 +135,17 @@ Follow these instructions:
139135
2. Then get the CBMC source via
140136
```
141137
git clone https://github.com/diffblue/cbmc cbmc-git
138+
cd cbmc-git
139+
```
140+
3. To compile CBMC, do
142141
```
143-
3. Then type
142+
make -C src minisat2-download
143+
make -C src
144144
```
145-
cd cbmc-git/src
146-
make minisat2-download
147-
make
145+
4. To compile JBMC, do
146+
```
147+
make -C jbmc/src java-models-library-download
148+
make -C jbmc/src
148149
```
149150

150151
# COMPILATION ON WINDOWS
@@ -161,6 +162,7 @@ Follow these instructions:
161162
2. Get the CBMC source via
162163
```
163164
git clone https://github.com/diffblue/cbmc cbmc-git
165+
cd cbmc-git
164166
```
165167
3. Depending on your choice of compiler:
166168
1. To compile with Visual Studio, change the second line of `src/config.inc`
@@ -169,20 +171,19 @@ Follow these instructions:
169171
BUILD_ENV = MSVC
170172
```
171173
Open the Developer Command Prompt for Visual Studio, then start the
172-
Cygwin shell with
173-
```
174-
bash.exe -login
175-
```
174+
Cygwin shell with
175+
```
176+
bash.exe -login
177+
```
176178
2. To compile with MinGW, use Cygwin setup to install a mingw g++ compiler
177179
package, i.e. one of `mingw{32,64}-{x86_64,i686}-gcc-g++`. You may also
178180
have to adjust the section in `src/common` that defines `CC` and `CXX`
179181
for BUILD_ENV = Cygwin.
180182
Then start the Cygwin shell.
181183
4. In the Cygwin shell, type
182184
```
183-
cd cbmc-git/src
184-
make DOWNLOADER=wget minisat2-download
185-
make
185+
make -C src DOWNLOADER=wget minisat2-download
186+
make -C src
186187
```
187188
188189
(Optional) A Visual Studio project file can be generated with the script
@@ -277,96 +278,3 @@ To work with Eclipse, do the following:
277278
5. Click "Finish"
278279
6. Select Project -> Build All
279280
280-
# CODE COVERAGE
281-
282-
Code coverage metrics are provided using gcov and lcov. Ensure that you have
283-
installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for
284-
ubuntu lcov is available in the standard apt-get repos.
285-
286-
To get coverage metrics run the following script from the regression directory:
287-
```
288-
get_coverage.sh
289-
```
290-
This will:
291-
1) Rebuild CBMC with gcov enabled
292-
2) Run all the regression tests
293-
3) Collate the coverage metrics
294-
4) Provide an HTML report of the current coverage
295-
296-
# USING CLANG-FORMAT
297-
298-
CBMC uses clang-format to ensure that the formatting of new patches is readable
299-
and consistent. There are two main ways of running clang-format: remotely, and
300-
locally.
301-
302-
## RUNNING CLANG-FORMAT REMOTELY
303-
304-
When patches are submitted to CBMC, they are automatically run through
305-
continuous integration (CI). One of the CI checks will run clang-format over
306-
the diff that your pull request introduces. If clang-format finds formatting
307-
issues at this point, the build will be failed, and a patch will be produced
308-
in the CI output that you can apply to your code so that it conforms to the
309-
style guidelines.
310-
311-
To apply the patch, copy and paste it into a local file (`patch.txt`) and then
312-
run:
313-
```
314-
patch -p1 -i patch.txt
315-
```
316-
Now, you can commit and push the formatting fixes.
317-
318-
## RUNNING CLANG-FORMAT LOCALLY
319-
320-
### INSTALLATION
321-
322-
To avoid waiting until you've made a PR to find formatting issues, you can
323-
install clang-format locally and run it against your code as you are working.
324-
325-
Different versions of clang-format have slightly different behaviors. CBMC uses
326-
clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and
327-
Homebrew.
328-
To install on a Unix-like system, try installing using the system package
329-
manager:
330-
```
331-
apt-get install clang-format-3.8 # Run this on Ubuntu, Debian etc.
332-
brew install [email protected] # Run this on a Mac with Homebrew installed
333-
```
334-
335-
If your platform doesn't have a package for clang-format, you can download a
336-
pre-built binary, or compile clang-format yourself using the appropriate files
337-
from the [LLVM Downloads page](http://releases.llvm.org/download.html).
338-
339-
An installer for Windows (along with a Visual Studio plugin) can be found at
340-
the [LLVM Snapshot Builds page](http://llvm.org/builds/).
341-
342-
### FORMATTING A RANGE OF COMMITS
343-
344-
Clang-format is distributed with a driver script called git-clang-format-3.8.
345-
This script can be used to format git diffs (rather than entire files).
346-
347-
After committing some code, it is recommended to run:
348-
```
349-
git-clang-format-3.8 upstream/develop
350-
```
351-
*Important:* If your branch is based on a branch other than `upstream/develop`,
352-
use the name or checksum of that branch instead. It is strongly recommended to
353-
rebase your work onto the tip of the branch it's based on before running
354-
`git-clang-format` in this way.
355-
356-
### RETROACTIVELY FORMATTING INDIVIDUAL COMMITS
357-
358-
If your works spans several commits and you'd like to keep the formatting
359-
correct in each individual commit, you can automatically rewrite the commits
360-
with correct formatting.
361-
362-
The following command will stop at each commit in the range and run
363-
clang-format on the diff at that point. This rewrites git history, so it's
364-
*unsafe*, and you should back up your branch before running this command:
365-
```
366-
git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \
367-
-- upstream/develop..HEAD
368-
```
369-
*Important*: `upstream/develop` should be changed in *both* places in the
370-
command above if your work is based on a different branch. It is strongly
371-
recommended to rebase your work onto the tip of the branch it's based on before
372-
running `git-clang-format` in this way.

0 commit comments

Comments
 (0)