Skip to content

Update documentation for building cbmc on windows. #1504

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Oct 24, 2017
Merged

Update documentation for building cbmc on windows. #1504

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
bcf8ff3
Update documentation for building cbmc on windows.
andreast271 Oct 21, 2017
08c512d
Make Windows compilation instructions more prescriptive
andreast271 Oct 24, 2017
dff22b8
Make Windows compilation instructions more prescriptive
andreast271 Oct 24, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 28 additions & 32 deletions COMPILING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down
8 changes: 5 additions & 3 deletions src/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This enables the user to set an alternative download program without editing the Makefile.
E.g. to use wget on Windows under Cygwin, do
make DOWNLOADER=wget minisat2-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
Expand All @@ -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 ../
Expand Down
8 changes: 5 additions & 3 deletions src/common
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For the static compilation problems, see Multiple definition error in static compilation with g++ under cygwin

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
Copy link
Contributor Author

@andreast271 andreast271 Oct 21, 2017 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

32 bit compilers (more precisely compilers where sizeof(size_t) == 4) will not work because of justified errors like this:

interpreter.cpp: In member function ‘size_t interpretert::get_size(const typet&):
interpreter.cpp:971:20: error: large integer implicitly truncated to unsigned type [-Werror=overflow]
return 2ULL << 32ULL;

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's a suggestion to fix this: #987

ifeq ($(origin YACC),default)
YACC = bison -y
Expand Down