File: COMPILING

package info (click to toggle)
cbmc 4.9-4
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 40,588 kB
  • ctags: 19,198
  • sloc: cpp: 185,860; ansic: 16,162; yacc: 5,343; lex: 4,518; makefile: 954; pascal: 506; sh: 318; perl: 213; java: 206
file content (154 lines) | stat: -rw-r--r-- 4,361 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
What architecture?
------------------

CPROVER compiles in the following environments:

- Linux

- MacOS X

- Solaris 11

- Cygwin
  (We recommend g++-3. Don't use the i686-pc-mingw32-g++ cross compiler.)

- Microsoft's Visual Studio 2010 or 2012 (older versions won't work)

The rest of this document is split up into three parts: compilation on
Linux, MacOS, Windows.  Please read the section appropriate for your
machine.


COMPILATION ON LINUX
--------------------

We assume that you have a Debian/Ubuntu or Red Hat-like distribution.

0) You need a C/C++ compiler, Flex and Bison, and GNU make.
   The GNU Make needs to be version 3.81 or higher. On Debian-like
   distributions, do

   apt-get install g++ gcc flex bison make subversion libz-dev libwww-perl patch

   On Red Hat/Fedora, do

   yum install gcc gcc-c++ flex bison perl-libwww-perl patch

   WARNING: g++ 4.5.x has been observed to mis-optimize code in
   MiniSat with -O3. Use a different version (or -O1).

1) You need a SAT solver (in source). We recommend MiniSat2. Do

   cd src
   make minisat2-download

2) Type make - that should do it.


COMPILATION ON SOLARIS 11
-------------------------

0) We recommend you get OpenCSW. Follow the instructions at

   http://www.opencsw.org/manual/for-administrators/getting-started.html

1) As root, get the necessary development tools:

   pkg install system/header
   /opt/csw/bin/pkgutil -i gzip coreutils wget CSWpm-libwww-perl subversion flex bison CSWgcc4g++

2) As a user, get the CBMC source via

   svn co http://www.cprover.org/svn/cbmc/trunk cbmc-trunk

3) Get MiniSat2 by entering

   cd cbmc-trunk
   wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.0.orig.tar.gz
   gtar xfz minisat_2.2.0.orig.tar.gz
   (cd minisat-2.2.0; patch -p1 < ../scripts/minisat-2.2.0-patch)

4) Type

   cd src; gmake CXX=/opt/csw/bin/g++

   That should do it.

   Do not attempt to compile with gcc-45 that comes with Solaris 11.
   It will mis-optimize MiniSat2.


COMPILATION ON MACOS X
----------------------

Follow these instructions:

0) You need a C/C++ compiler, Flex and Bison, and GNU make. To this
   end, install the XCode command-line utilities (installing XCode is
   not enough). These are available at

   https://developer.apple.com/downloads/

1) You need a SAT solver (in source). We recommend MiniSat2. Do

   cd src
   make minisat2-download

2) Type cd src; make - that should do it.


COMPILATION ON WINDOWS
----------------------

There are two options: compilation using g++ from Cygwin, or using
Visual Studio's compiler. As Cygwin has significant overhead during
process creation, we advise you use Visual Studio.

Follow these instructions:

0) You need a C/C++ compiler, Flex and Bison, GNU tar, gzip2,
   GNU make, and patch. The GNU Make needs to be version 3.81 or
   higher.  If you don't already have the above, we recommend you install
   Cygwin.

   WARNING: g++ 4.5.x has been observed to mis-optimize code in
   MiniSat with -O3. Use a different version (or -O1).

1) You need a SAT solver (in source). We recommend MiniSat2. Using a
   browser, download from

   http://minisat.se/downloads/minisat-2.2.0.tar.gz

   and then unpack with

   tar xfz minisat-2.2.0.tar.gz
   mv minisat minisat-2.2.0
   cd minisat-2.2.0
   patch -p1 < scripts/minisat-2.2.0-patch

   The patch removes the dependency on zlib and prevents a problem
   with a header file that is often unavailable on Windows.

2) Adjust src/config.inc for the paths to item 1).

3A) To compile with Cygwin, install the mingw compilers, and adjust
   the second line of config.inc to say

   BUILD_ENV = MinGW

3B) To compile with Visual Studio, make sure you have at least Visual
   Studio 10, and adjust the second line of config.inc to say

   BUILD_ENV = MSVC

   Open the Visual Studio Command prompt, and then run the make.exe
   from Cygwin from in there.

4) Type cd src; make - that should do it.
   Note that "nmake" is not expected to work. Use "make".

(Optional) A Visual Studio project file can be generated with the script
"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.