From 6388940391f7563b0b367468e18da7dda8c4bfa7 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 29 Nov 2017 14:20:45 +0000 Subject: [PATCH 1/4] Fix 'missing return statement' errors in miniBDD_new --- unit/miniBDD_new.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/unit/miniBDD_new.cpp b/unit/miniBDD_new.cpp index b61b0e54093..14ae84e668e 100644 --- a/unit/miniBDD_new.cpp +++ b/unit/miniBDD_new.cpp @@ -64,6 +64,7 @@ class bdd_propt:public propt literalt lor(literalt a, literalt b) override { UNREACHABLE; + return {}; } literalt land(const bvt &bv) override @@ -94,16 +95,19 @@ class bdd_propt:public propt literalt lxor(const bvt &bv) override { UNREACHABLE; + return {}; } literalt lnand(literalt a, literalt b) override { UNREACHABLE; + return {}; } literalt lnor(literalt a, literalt b) override { UNREACHABLE; + return {}; } literalt lequal(literalt a, literalt b) override @@ -114,11 +118,13 @@ class bdd_propt:public propt literalt limplies(literalt a, literalt b) override { UNREACHABLE; + return {}; } literalt lselect(literalt a, literalt b, literalt c) override { UNREACHABLE; + return {}; } void lcnf(const bvt &bv) override @@ -144,11 +150,13 @@ class bdd_propt:public propt resultt prop_solve() override { UNREACHABLE; + return {}; } tvt l_get(literalt a) const override { UNREACHABLE; + return {}; } expanding_vectort bdd_map; From adb7f553b05cd830c3255fd6d382d81e4cb68ac6 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 29 Nov 2017 14:30:39 +0000 Subject: [PATCH 2/4] Add Windows dependency information to the COMPILING file --- COMPILING.md | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/COMPILING.md b/COMPILING.md index dcc822f890d..64ad28c9737 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -177,6 +177,8 @@ using "make generated_files" before opening the project. There is an experimental build based on CMake instead of hand-written makefiles. It should work on a wider variety of systems than the standard makefile build, and can integrate better with IDEs and static-analysis tools. +On Windows, the CMake build does not depend on Cygwin or MinGW, and doesn't +require manual modification of build files. 1. Ensure you have all the build dependencies installed. Build dependencies are the same as for the makefile build, but with the addition of CMake version @@ -196,9 +198,15 @@ makefile build, and can integrate better with IDEs and static-analysis tools. ``` You shoud also install [Homebrew](https://brew.sh), after which you can run `brew install cmake` to install CMake. - - On Windows, install Cygwin, then from the Cygwin setup facility install - `cmake`, `flex`, `bison`, `tar`, `gzip`, `git`, `make`, `wget`, and - `patch`. + - On Windows, ensure you have Visual Studio 2013 or later installed. + Then, download CMake from the [official download + page](https://cmake.org/download). + You'll also need `git` and `patch`, which are both provided by the + [git for Windows](git-scm.com/download/win) package. + Finally, Windows builds of flex and bison should be installed from + [the sourceforge page](sourceforge.net/projects/winflexbison). + The easiest way to 'install' these executables is to unzip them and to + drop the entire unzipped package into the CBMC source directory. - Use of CMake has not been tested on Solaris or FreeBSD. However, it should be possible to install CMake from the system package manager or the [official download page](https://cmake.org/download) on those systems. From 33d71aa53d9a7e43ab3689cb3097dbd903083b34 Mon Sep 17 00:00:00 2001 From: reuk Date: Wed, 29 Nov 2017 13:52:06 +0000 Subject: [PATCH 3/4] Disable use of unistd in flex outputs Also use never-interactive option --- src/assembler/scanner.l | 7 ++----- src/jsil/scanner.l | 6 ++---- src/json/scanner.l | 6 ++---- src/xmllang/scanner.l | 6 ++---- 4 files changed, 8 insertions(+), 17 deletions(-) mode change 100644 => 100755 src/assembler/scanner.l mode change 100644 => 100755 src/jsil/scanner.l mode change 100644 => 100755 src/json/scanner.l mode change 100644 => 100755 src/xmllang/scanner.l diff --git a/src/assembler/scanner.l b/src/assembler/scanner.l old mode 100644 new mode 100755 index fce0d352b40..816e61616dc --- a/src/assembler/scanner.l +++ b/src/assembler/scanner.l @@ -1,13 +1,10 @@ %option nounput %option noinput +%option nounistd +%option never-interactive %{ -#ifdef _WIN32 -#define YY_NO_UNISTD_H -static int isatty(int) { return 0; } -#endif - #define PARSER assembler_parser #define YYSTYPE unsigned #undef ECHO diff --git a/src/jsil/scanner.l b/src/jsil/scanner.l old mode 100644 new mode 100755 index f31ab0f8ad1..c8e5c46d626 --- a/src/jsil/scanner.l +++ b/src/jsil/scanner.l @@ -1,12 +1,10 @@ %option nounput %option noinput +%option nounistd +%option never-interactive %option stack %{ -#ifdef _WIN32 -#define YY_NO_UNISTD_H -static int isatty(int) { return 0; } -#endif #include diff --git a/src/json/scanner.l b/src/json/scanner.l old mode 100644 new mode 100755 index 7bda01fd033..ad854544950 --- a/src/json/scanner.l +++ b/src/json/scanner.l @@ -5,14 +5,12 @@ %option 8bit nodefault %option nounput %option noinput +%option nounistd +%option never-interactive %option noyywrap %{ -#ifdef _WIN32 -#define YY_NO_UNISTD_H -static int isatty(int) { return 0; } -#endif #define PARSER json_parser diff --git a/src/xmllang/scanner.l b/src/xmllang/scanner.l old mode 100644 new mode 100755 index e262b927112..5726c75afee --- a/src/xmllang/scanner.l +++ b/src/xmllang/scanner.l @@ -1,12 +1,10 @@ %option 8bit nodefault %option nounput %option noinput +%option nounistd +%option never-interactive %{ -#ifdef _WIN32 -#define YY_NO_UNISTD_H -static int isatty(int) { return 0; } -#endif #include #include From 6c3fb17c69c76cdf0ba8ec645bb378c92ebdc655 Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 1 Dec 2017 14:54:01 +0000 Subject: [PATCH 4/4] Update appveyor config --- appveyor.yml | 20 ++++++++------------ 1 file changed, 8 insertions(+), 12 deletions(-) diff --git a/appveyor.yml b/appveyor.yml index c61f77b99b4..f50e3ce8c53 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -12,18 +12,14 @@ install: md deps } cd deps - if (!(Test-Path bin\bison.exe)) { - & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/bison-2.4.1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=JAPFzNPMJDI4IViAVlJAEc6l8aHB3k17NpZRdoWDMLbALaJNX88vfwocuezU1tfhyrSJxfo2fTK4rgP5OULkikJs7MBZI9ovp2V%2BMT6yg87KDdH9EIOlMgltGfbP%2BoZkwBY7kXb3W5puSlt4OTE%2Bw7CRlHF9MNqFXVBqVBfa%2BGw0gXDe5Jd9qV%2BvUXZzRuBl9ERSQkSD%2B%2B%2BxFo24FZoOeYkgBHJz03%2BHuIMnlmcLgneTB2aiZZU3%2B6UTPceUxLus9%2Bksb5UbqEVaVE06TIXl76VKwqAgXM2LWaNyeJDog%2BT%2BhjW4v4ypxh6mIBo5KRNXVLPc1MxSPFQB3ITlIXv9Zg%3D%3D" - & 7z x bison-2.4.1-bin.zip - } - if (!(Test-Path bin\flex.exe)) { - & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/flex-2.5.4a-1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=WriP8S047Mmq271ZHWL0MCPGx1gEFsuc%2BKMmChoXhXFRkn0GlIgCxZEiOu52ke9fT1kAvycWXePNBFAyCHjpF%2BJkXCwisQ6FLIf3NL%2F92849YgQKdJkDUOcZ%2Bh82XVTwNBrljKIkExkak7QEyhOf3buTC1oeuatCUV5Ez42RZjgtRiJaqcFW6xLbhfuVONr39KxH5hGx%2FDUi2RRXPbgoKDwavc9s56NP1rNbWMTE6NdNHzJeaf43E%2BSMemlVO%2BhhIY6W0f%2FtaQ7fYF%2F6YaqxdQ0sB8W5DnG4Hb%2F0CyQlrTZpGDXGr301rV0M4WBkYLmfauq4IyJsBaR095tXGW%2BzmA%3D%3D" - & 7z x flex-2.5.4a-1-bin.zip - } - if (!(Test-Path include\FlexLexer.h)) { - & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/flex-2.5.4a-1-lib.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=H%2FLeKGv2QqKAGDTP%2F6TYPhDzuL6K%2F5dFOt61HfYBm1vUWVUNmAYVGvUAcvnUqBnhEHwZgtc8vZt1H7k3W8azxCUc7l6ZhlCDbqQ6Mg2VhfpBaQMbL1V%2BjSq5ePpWcuLMBntKk2br38PF1NtiAwCCpRTRPptaYPeGs%2BOjAH%2BN8aIIxjvj45QAgt9mcg6dfBsyfj5fdJmpHRQFuJ7%2FnsG50fmN5JDvdvmBWloB6rjxVWaN4XO6VTWZFZ34JWFyOqgWNEw9aDN3HdsSuJ0Uz19AbdwZBIWe5Elrl71rRJjn1lijCknDB7D4sAmP33k71e%2BB0qvsNl1Shuh9FkY8Z6y05Q%3D%3D" - & 7z x flex-2.5.4a-1-lib.zip - } + appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/win_flex_bison-latest.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1543674503&Signature=CojdaOYrFl50gbxCQL%2BlfVtuo7j9v1OzfWD6jYIkfv1h7xzCacigAM51%2BVjaVx%2B8yvUjk%2B4MOU%2FKmLzev7dABWNi5n7p7SvlXYPFVVwDE57Me35Xi7BzW%2FhoSaPnVIGuhAmDfxjGoHhB0Of%2Fd2FfMl4cklGgc2YafTpFX3agNCE4dcc1UyG0SY5CbvTGTuBP%2B99zaQ69lNT1TSNUNp0PW2Hhj%2FPylts0IdDm713RA4wcNIHvLTTppBiNwMm0y%2B0qRG1op3R4vc5gahz%2B6dTUnCevYWO5l%2FIvmXQyo4XNkgqLKIRgk4wisLjtSuRh5vPyD%2FQPOrn2ubT53YnDcW6geA%3D%3D" + 7z x win_flex_bison-latest.zip + Move-Item win_bison.exe bin\bison.exe -force + Move-Item win_flex.exe bin\flex.exe -force + Move-Item FlexLexer.h include\FlexLexer.h -force + Move-Item data bin\data -force + bison -V + flex -V if (!(Test-Path bin\iconv.exe)) { & appveyor DownloadFile "https://storage.googleapis.com/diffblue-mirror/appveyor-deps/libiconv-1.9.2-1-bin.zip?GoogleAccessId=diffbluemaster@diffblue-cr.iam.gserviceaccount.com&Expires=1519839050&Signature=sS3Y2lC1oWOhBDsL8C9ASuO4LOM%2BpB%2F8PwG5w5CdB9JnPfLqhb3FnA1zkkZJoSNuIYS3DM6CN2qxoWjpJbLEtVQe0PpxziQZjLpJw2MpxXdJiJHRDu8x9THgzwuZ3ze5BWHzPoCBQPdRkKzVPezf1HwptUsm3Y9c2jlWljQjhc8NVsI4iPmjEOwT8E%2BYpR5fsLs2GsRjuoyqKa%2Bi4JJ6MbpXVX1IgR4fzp1Li9SnE39ujHDb%2FyI3c96eCdVm1Oa6jNxzSJNfq%2FgOZM8BIxlR55a%2BtM3oBQhU0voEtDOABwuO7ZBay8dLt%2FG5vz1%2Bi%2FIlRLFxQfICaprPLzw6pXRm8Q%3D%3D" & 7z x libiconv-1.9.2-1-bin.zip