Skip to content

Commit d63f9b7

Browse files
committed
Implement suggestions from #6109 and some further cleanup.
Implement some suggestions presented as comments in #6109 (we had to merge the PR before we could get a chance to incorporate them, so we are compensating now) and do some other minor cleanup of the COMPILING.md file.
1 parent 49f603a commit d63f9b7

File tree

1 file changed

+25
-20
lines changed

1 file changed

+25
-20
lines changed

COMPILING.md

Lines changed: 25 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ following environments:
1010
The above environments are currently tested as part of our continuous
1111
integration system. It separately tests both the CMake build system and the
1212
hand-written make files. The latest build steps being used in CI can be
13-
[referenced here](https://github.com/diffblue/cbmc/blob/develop/.github/workflows/pull-request-checks.yaml).
13+
[found here](https://github.com/diffblue/cbmc/blob/develop/.github/workflows/pull-request-checks.yaml).
1414

1515
The environments below have been used successfully in the
1616
past, but are not actively tested:
@@ -22,7 +22,7 @@ past, but are not actively tested:
2222

2323
Building with CMake is supported across Linux, MacOS X and Windows with Visual
2424
Studio 2019. There are also hand-written make files which can be used to build
25-
separate binaries independently. Usage of the hand-written make files is
25+
separate targets independently. Usage of the hand-written make files is
2626
explained in a separate section. The CMake build can build the complete
2727
repository in fewer steps and supports better integration with various IDEs and
2828
static-analysis tools. On Windows, the CMake build has the advantage of not
@@ -47,9 +47,6 @@ files.
4747
```
4848
You should also install [Homebrew](https://brew.sh), after which you can
4949
run `brew install cmake` to install CMake.
50-
- On platforms where installing the Java Development Kit and Maven is
51-
difficult, you can avoid needing these dependencies by not building
52-
JBMC. Just pass `-DWITH_JBMC=OFF` to `cmake` in step (4) below.
5350
- On Windows, ensure you have Visual Studio 2019 or later installed. The
5451
developer command line that comes with Visual Studio 2019 has CMake
5552
already available. You will also need to ensure that you have winflexbison
@@ -103,6 +100,10 @@ files.
103100
`-DCMAKE_EXE_LINKER_FLAGS=...`. This is useful for enabling clang's
104101
sanitizers.
105102
103+
**Note: Building without JBMC**: On platforms where installing the Java
104+
Development Kit and Maven is difficult, you can avoid needing these
105+
dependencies by not building JBMC. Just pass `-DWITH_JBMC=OFF` to `cmake`.
106+
106107
Finally, to enable building universal binaries on macOS, you can pass the
107108
flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag,
108109
the built binaries will only work on the architecture of the machine being
@@ -115,15 +116,19 @@ files.
115116
This command tells CMake to invoke the correct tool to run the build in the
116117
`build` directory. You can also use the build back-end directly by invoking
117118
`make`, `ninja`, or opening the generated IDE project as appropriate. The
118-
complete set of built binaries can be found in `./build/bin` once the build
119+
complete set of built binaries can be found in `build/bin/` once the build
119120
is complete.
120121
121-
# Building using hand-written make files.
122+
*Parellel building*: You can pass `-j<numjobs>` to `make` to indicate how many
123+
jobs to run simultaneously. `ninja` defaults to building with `# of cores + 2`
124+
jobs at the same time.
125+
126+
# Building using Make
122127
123-
The rest of this section is split up based on the platform being built on.
124-
Please read the section appropriate for your machine.
128+
The rest of this section is split up based on the platform being built on.
129+
Please read the section appropriate for your platform.
125130
126-
## COMPILATION ON LINUX
131+
## Compiling with Make on Linux
127132
128133
We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
129134
@@ -175,7 +180,7 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
175180
make -C jbmc/src
176181
```
177182
178-
## COMPILATION ON MACOS X
183+
## Compiling with Make on MacOS
179184
180185
Follow these instructions:
181186
@@ -202,7 +207,7 @@ Follow these instructions:
202207
make -C jbmc/src
203208
```
204209
205-
## COMPILATION ON SOLARIS 11
210+
## Compiling with Make on Solaris
206211
207212
We assume Solaris 11.4 or newer. To build JBMC, you'll need to install
208213
Maven 3 manually.
@@ -227,7 +232,7 @@ Maven 3 manually.
227232
gmake -C jbmc/src
228233
```
229234
230-
## COMPILATION ON FREEBSD 11
235+
## Compiling with Make on FreeBSD
231236
232237
1. As root, get the necessary tools:
233238
```
@@ -253,7 +258,7 @@ Maven 3 manually.
253258
gmake -C jbmc/src
254259
```
255260
256-
# Working with IDEs
261+
# Working with IDEs and Docker
257262
258263
## Working with Visual Studio on Windows
259264
@@ -290,23 +295,23 @@ the need to integrate JBMC as a separate project. Be aware that you need to
290295
change the build location (Select project in Eclipse -> Properties -> C/C++
291296
Build) to one of the src directories.
292297
293-
# WORKING WITH DOCKER
298+
## Working with Docker
294299
295300
To compile and run the tools in a Docker container, do the following:
296301
297302
1. From the root folder of the project, run `$ docker build -t cbmc .`
298-
2. After the building phase has finished, there should be a new
303+
2. After the building phase has finished, there should be a new
299304
image with the CProver binaries installed under `/usr/local/bin/`.
300305
301306
To start a container using that image as a base, run `$ docker run -i -t cbmc`
302307
This will result in dropping you to a new terminal inside the container. To
303308
load files for analysis into the container, one way is by mounting the folder
304309
that contains the tests to the container. A possible invocation that does that
305-
is: `$ docker run --mount type=bind,source=local/path/with/files,target=/mnt/analysis -i t cbmc`. In the
306-
resulting container, the files present in the local file system under
307-
`local/path/with/files` will be present under `/mnt/analysis`.
310+
is: `$ docker run --mount type=bind,source=local/path/with/files,target=/mnt/analysis -i t cbmc`.
311+
In the resulting container, the files present in the local file system under
312+
`local/path/with/files` will be present under `/mnt/analysis`.
308313
309-
# OPTIONS AND VARIABLES
314+
# Compilation options and configuration
310315
311316
## Compiling with CUDD
312317

0 commit comments

Comments
 (0)