Skip to content

Commit 47f413a

Browse files
author
Daniel Kroening
committed
fix compilation instructions
1 parent 8f6dab8 commit 47f413a

File tree

1 file changed

+40
-39
lines changed

1 file changed

+40
-39
lines changed

COMPILING.md

Lines changed: 40 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -21,45 +21,39 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
2121
The GNU Make needs to be version 3.81 or higher.
2222
On Debian-like distributions, do
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
```
2626
On Red Hat/Fedora or derivates, do
2727
```
28-
yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 java-1.7.0-openjdk-devel
28+
yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6
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-
3433
For the JDK, on Debian-like distributions, do
3534
```
36-
apt-get install openjdk-7-jdk
35+
apt-get install openjdk-8-jdk
3736
```
3837
On Red Hat/Fedora or derivates, do
3938
```
40-
yum install java-1.7.0-openjdk-devel
41-
```
42-
For the models library, do
43-
```
44-
make -C jbmc/src java-models-library-download
39+
yum 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
5045
```
46+
5147
3. On Debian or Ubuntu, do
5248
```
53-
cd cbmc-git/src
54-
make minisat2-download
55-
make
49+
make -C cbmc-git/src minisat2-download
50+
make -C cbmc-git/src
5651
```
5752
On Redhat/Fedora etc., do
5853
```
59-
cd cbmc-git/src
60-
make minisat2-download
6154
scl enable devtoolset-6 bash
62-
make
55+
make -C cbmc-git/src minisat2-download
56+
make -C cbmc-git/src
6357
```
6458

6559
4. Linking against an IPASIR SAT solver
@@ -75,6 +69,12 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
7569
make -C src IPASIR=../../ipasir LIBSOLVER=$(pwd)/ipasir/libipasir.a
7670
```
7771

72+
5. To compile JBMC, do
73+
```
74+
make -C cbmc-git/jbmc/src java-models-library-download
75+
make -C cbmc-git/jbmc/src
76+
```
77+
7878
# COMPILATION ON SOLARIS 11
7979

8080
1. As root, get the necessary development tools:
@@ -88,42 +88,40 @@ We assume that you have a Debian/Ubuntu or Red Hat-like distribution.
8888
export PATH=/opt/csw/bin:$PATH
8989
git clone https://github.com/diffblue/cbmc cbmc-git
9090
```
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
91+
3. To compile CBMC, type
9792
```
98-
gmake
93+
gmake -C cbmc-git/src minisat2-download DOWNLOADER=wget TAR=gtar
94+
gmake -C cbmc-git/src
9995
```
100-
That should do it. To run, you will need
96+
4. To compile JBMC, type
10197
```
102-
export LD_LIBRARY_PATH=/usr/gcc/5.0/lib
98+
gmake -C cbmc-git/jbmc/src java-models-library-download
99+
gmake -C cbmc-git/jbmc/src
103100
```
104101

105102
# COMPILATION ON FREEBSD 11
106103

107104
1. As root, get the necessary tools:
108105
```
109-
pkg install bash gmake git www/p5-libwww patch flex bison openjdk
106+
pkg install bash gmake git www/p5-libwww patch flex bison
110107
```
111108
To compile JBMC, additionally install
112109
```
113-
pkg install openjdk
110+
pkg install openjdk8 wget
114111
```
115-
2. As a user, get the CBMC source via
112+
2. As a user, get the CBMC source via
116113
```
117114
git clone https://github.com/diffblue/cbmc cbmc-git
118115
```
119-
3. Do
116+
3. To compile CBMC, do
120117
```
121-
cd cbmc-git/src
118+
gmake -C cbmc-git/src minisat2-download
119+
gmake -C cbmc-git/src
122120
```
123-
4. Do
121+
4. To compile JBMC, do
124122
```
125-
gmake minisat2-download
126-
gmake
123+
gmake -C cbmc-git/jbmc/src java-models-library-download
124+
gmake -C cbmc-git/jbmc/src
127125
```
128126

129127
# COMPILATION ON MACOS X
@@ -140,11 +138,15 @@ Follow these instructions:
140138
```
141139
git clone https://github.com/diffblue/cbmc cbmc-git
142140
```
143-
3. Then type
141+
3. To compile CBMC, do
142+
```
143+
make -C cbmc-git/src minisat2-download
144+
make -C cbmc-git/src
145+
```
146+
4. To compile JBMC, do
144147
```
145-
cd cbmc-git/src
146-
make minisat2-download
147-
make
148+
make -C cbmc-git/jbmc/src java-models-library-download
149+
make -C cbmc-git/jbmc/src
148150
```
149151

150152
# COMPILATION ON WINDOWS
@@ -180,9 +182,8 @@ Follow these instructions:
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 cbmc-git/src DOWNLOADER=wget minisat2-download
186+
make -C cbmc-git/src
186187
```
187188
188189
(Optional) A Visual Studio project file can be generated with the script

0 commit comments

Comments
 (0)