2011-05-11 21:13:55 +08:00
|
|
|
What architecture?
|
|
|
|
------------------
|
|
|
|
|
2011-06-13 20:47:32 +08:00
|
|
|
CPROVER compiles in the following environments:
|
2011-07-14 19:47:56 +08:00
|
|
|
|
2011-05-11 21:13:55 +08:00
|
|
|
- Linux
|
2011-07-14 19:47:56 +08:00
|
|
|
|
2011-05-11 21:13:55 +08:00
|
|
|
- MacOS X
|
2011-07-14 19:47:56 +08:00
|
|
|
|
2011-08-10 20:11:34 +08:00
|
|
|
- Cygwin
|
|
|
|
(We recommend g++-3. Don't use the i686-pc-mingw32-g++ cross compiler.)
|
2011-07-14 19:47:56 +08:00
|
|
|
|
2012-09-16 04:00:18 +08:00
|
|
|
- Microsoft's Visual Studio 2010 or 2012 (older versions won't work)
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
The rest of this document is split up into three parts: compilation on
|
|
|
|
Linux, MacOS, Windows. Please read the section appropriate for your
|
|
|
|
machine.
|
2011-05-11 21:13:55 +08:00
|
|
|
|
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
COMPILATION ON LINUX
|
|
|
|
--------------------
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
We assume that you have a Debian/Ubuntu-like distribution.
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2011-06-13 20:47:32 +08:00
|
|
|
0) You need a C/C++ compiler, Flex and Bison, and GNU make.
|
2012-09-16 04:00:18 +08:00
|
|
|
The GNU Make needs to be version 3.81 or higher. Do
|
2011-06-13 20:47:32 +08:00
|
|
|
|
2013-05-15 19:40:27 +08:00
|
|
|
apt-get install g++ gcc flex bison make subversion libz-dev libwww-perl patch
|
2011-06-13 20:47:32 +08:00
|
|
|
|
2013-01-11 13:46:58 +08:00
|
|
|
WARNING: g++ 4.5.x has been observed to mis-optimize code in
|
|
|
|
MiniSat with -O3. Use a different version (or -O1).
|
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
1) You need a SAT solver (in source). We recommend MiniSat2. Do
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
cd src
|
|
|
|
make minisat2-download
|
2012-09-16 04:00:18 +08:00
|
|
|
|
2013-05-15 19:53:11 +08:00
|
|
|
2) Type cd src; make - that should do it.
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
|
|
|
|
COMPILATION ON MACOS X
|
|
|
|
----------------------
|
|
|
|
|
|
|
|
Follow these instructions:
|
|
|
|
|
|
|
|
0) You need a C/C++ compiler, Flex and Bison, and GNU make. To this
|
2013-05-15 19:53:11 +08:00
|
|
|
end, install the XCode command-line utilities (installing XCode is
|
2012-10-21 19:15:17 +08:00
|
|
|
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
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2013-05-15 19:53:11 +08:00
|
|
|
2) Type cd src; make - that should do it.
|
2012-10-21 19:15:17 +08:00
|
|
|
|
|
|
|
|
|
|
|
COMPILATION ON WINDOWS
|
|
|
|
----------------------
|
|
|
|
|
2012-11-15 16:35:16 +08:00
|
|
|
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.
|
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
Follow these instructions:
|
|
|
|
|
|
|
|
0) You need a C/C++ compiler, Flex and Bison, GNU tar, gzip2,
|
2013-05-15 19:48:39 +08:00
|
|
|
zlib, 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.
|
2012-10-21 19:15:17 +08:00
|
|
|
|
2013-01-11 13:46:58 +08:00
|
|
|
WARNING: g++ 4.5.x has been observed to mis-optimize code in
|
|
|
|
MiniSat with -O3. Use a different version (or -O1).
|
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
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
|
2013-05-15 19:48:39 +08:00
|
|
|
cd minisat-2.2.0
|
|
|
|
patch -p1 < ../scripts/minisat-2.2.0-patch
|
2012-10-21 19:15:17 +08:00
|
|
|
|
2013-05-15 19:48:39 +08:00
|
|
|
The patch removes the dependency on zlib and prevents a problem
|
|
|
|
with a header file that is often unavailable on Windows.
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2011-07-14 19:47:56 +08:00
|
|
|
2) Adjust src/config.inc for the paths to item 1).
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2013-05-15 19:53:11 +08:00
|
|
|
3A) To compile with Cygwin, install the mingw compilers, and adjust
|
2012-10-21 19:15:17 +08:00
|
|
|
the second line of config.inc to say
|
|
|
|
|
|
|
|
BUILD_ENV = MinGW
|
|
|
|
|
2013-05-15 19:53:11 +08:00
|
|
|
3B) To compile with Visual Studio, make sure you have at least Visual
|
2012-10-21 19:15:17 +08:00
|
|
|
Studio 10, and adjust the second line of config.inc to say
|
2011-07-14 19:47:56 +08:00
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
BUILD_ENV = MSVC
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2012-10-21 19:15:17 +08:00
|
|
|
Open the Visual Studio Command prompt, and then run the bash.exe
|
|
|
|
from Cygwin from in there.
|
2011-05-11 21:13:55 +08:00
|
|
|
|
2013-05-15 19:53:11 +08:00
|
|
|
4) Type cd src; make - that should do it.
|
2013-03-04 18:02:33 +08:00
|
|
|
Note that "nmake" is not expected to work. Use "make".
|
|
|
|
|
|
|
|
|