diff --git a/COMPILING.md b/COMPILING.md index b6003e4ee89..6257cda40da 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -7,10 +7,8 @@ environments: - MacOS X - Solaris 11 - FreeBSD 11 -- Cygwin (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or - above.) -- Microsoft's Visual Studio version 12 (2013), version 14 (2015), or version 15 - (older versions won't work) +- Cygwin +- Microsoft Visual Studio The rest of this document is split up into three parts: compilation on Linux, MacOS, Windows. Please read the section appropriate for your machine. @@ -119,42 +117,40 @@ Follow these instructions: # 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. +There are two options: the Visual Studio compiler with version 12 (2013) or +later, or the MinGW cross compiler with version 5.4 or later. +We recommend Visual Studio. Follow these instructions: -1. 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. -2. You need a SAT solver (in source). We recommend MiniSat2. Using a - browser, download from +1. First install Cygwin, then from the Cygwin setup facility install the + following packages: `flex, bison, tar, gzip, git, make, wget, patch`. +2. Get the CBMC source via ``` - http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz - ``` - and then unpack with - ``` - tar xfz minisat-2.2.1.tar.gz - mv minisat minisat-2.2.1 - cd minisat-2.2.1 - patch -p1 < ../scripts/minisat-2.2.1-patch + git clone https://github.com/diffblue/cbmc cbmc-git ``` - The patch removes the dependency on zlib and prevents a problem with a - header file that is often unavailable on Windows. - 1. To compile with Cygwin, install the mingw compilers, and adjust - the second line of config.inc to say - ``` - BUILD_ENV = MinGW - ``` - 2. To compile with Visual Studio, make sure you have at least Visual - Studio version 12 (2013), and adjust the second line of config.inc to say +3. Depending on your choice of compiler: + 1. To compile with Visual Studio, change the second line of `src/config.inc` + to ``` BUILD_ENV = MSVC ``` - Open the Visual Studio Command prompt, and then bash.exe -login from - Cygwin from in there. -3. Type cd src; make - that should do it. + Open the Developer Command Prompt for Visual Studio, then start the + Cygwin shell with + ``` + bash.exe -login + ``` + 2. To compile with MinGW, use Cygwin setup to install a mingw g++ compiler + package, i.e. one of `mingw{32,64}-{x86_64,i686}-gcc-g++`. You may also + have to adjust the section in `src/common` that defines `CC` and `CXX` + for BUILD_ENV = Cygwin. + Then start the Cygwin shell. +4. In the Cygwin shell, type + ``` + cd cbmc-git/src + make DOWNLOADER=wget minisat2-download + 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 diff --git a/src/Makefile b/src/Makefile index 447218d3291..3f53a79fc32 100644 --- a/src/Makefile +++ b/src/Makefile @@ -63,11 +63,13 @@ clean: $(patsubst %, %_clean, $(DIRS)) $(patsubst %, %_clean, $(DIRS)): $(MAKE) $(MAKEARGS) -C $(patsubst %_clean, %, $@) clean ; \ -# minisat 2 download, for your convenience +# minisat2 and glucose download, for your convenience + +DOWNLOADER = lwp-download minisat2-download: @echo "Downloading Minisat 2.2.1" - @lwp-download http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz + @$(DOWNLOADER) http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz @tar xfz minisat2_2.2.1.orig.tar.gz @rm -Rf ../minisat-2.2.1 @mv minisat2-2.2.1 ../minisat-2.2.1 @@ -76,7 +78,7 @@ minisat2-download: glucose-download: @echo "Downloading glucose-syrup" - @lwp-download http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz + @$(DOWNLOADER) http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz @tar xfz glucose-syrup.tgz @rm -Rf ../glucose-syrup @mv glucose-syrup ../ diff --git a/src/common b/src/common index 323bdbf4367..ad74f211928 100644 --- a/src/common +++ b/src/common @@ -101,17 +101,19 @@ else ifeq ($(BUILD_ENV_),Cygwin) CXXFLAGS ?= -Wall -O2 CP_CFLAGS = -MMD -MP CP_CXXFLAGS += -MMD -MP -std=c++11 -U__STRICT_ANSI__ + # Cygwin-g++ has problems with statically linking exception code. + # If linking fails, remove -static. LINKFLAGS = -static -std=c++11 LINKLIB = ar rcT $@ $^ - LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) -static + LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS) LINKNATIVE = $(HOSTCXX) -std=c++11 -o $@ $^ -static ifeq ($(origin CC),default) #CC = gcc - CC = i686-w64-mingw32-gcc + CC = x86_64-w64-mingw32-gcc endif ifeq ($(origin CXX),default) #CXX = g++ - CXX = i686-w64-mingw32-g++ + CXX = x86_64-w64-mingw32-g++ endif ifeq ($(origin YACC),default) YACC = bison -y