Merge pull request #1504 from andreast271/update-windows-build

Update documentation for building cbmc on windows.

Author: Daniel Kroening

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

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 ../

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