-
Notifications
You must be signed in to change notification settings - Fork 276
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.
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
Conversation
COMPILING
Outdated
|
||
BUILD_ENV = MinGW | ||
Open the Visual Studio Command prompt, and then start the Cygwin shell with |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BUILD_ENV should be Cygwin, which will be detected correctly if BUILD_ENV = AUTO and make is called from the cygwin shell.
# minisat 2 download, for your convenience | ||
# minisat2 and glucose download, for your convenience | ||
|
||
DOWNLOADER = lwp-download | ||
|
There was a problem hiding this comment.
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
@@ -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 |
There was a problem hiding this comment.
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
endif | ||
ifeq ($(origin CXX),default) | ||
#CXX = g++ | ||
CXX = i686-w64-mingw32-g++ | ||
CXX = x86_64-w64-mingw32-g++ | ||
endif |
There was a problem hiding this comment.
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;
There was a problem hiding this comment.
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
It should also be mentioned that the CYGWIN build isn't recommended. Among other reasons, you won't be able to do Unicode file names. |
One more: I doubt that g++ 5.4 still works; I believe we need at least 5.8, if not higher. |
Reading through the entire thing, I would recommend that we are more prescriptive. It's really hard to collect all the utilities (bison etc.) separately. Thus, I'd say "Get CYGWIN. Do this." I would scratch compilation with Cygwin, and only do MinGW and Visual Studio. |
Is BUILD_ENV==MINGW in the Makefiles useful, or could it be removed? |
I believe there is a corporate customer that uses this set up. |
Update makefiles to use reasonable default compiler for cygwin build. Allow alternative downloader selection from make command line.
29c6484
to
08c512d
Compare
src/util/config.cpp
Outdated
@@ -862,7 +862,8 @@ bool configt::set(const cmdlinet &cmdline) | |||
#endif | |||
|
|||
// MinGW has extra defines | |||
ansi_c.defines.push_back("__int64=\"long long\""); | |||
// defines are shell quoted, which gives the wrong result in this case | |||
ansi_c.preprocessor_options.push_back("-D__int64=\"long long\""); | |||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a bug fix related to the PR, because it affects usability of the mingw build on windows. Due to shell quoting, using ansi_c.defines eventually produces code like this:
"long long" n;
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can that be split out into a separate PR? There should be a proper solution for this that works for other defines as well.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks sensible, but suggest tagging someone else that can try to reproduce these who has a Win32 box in the office!
It does still work. |
26bc44b
to
dff22b8
Compare
739c7f5 Merge remote-tracking branch 'upstream/develop' into merge-develop-20171026 37b868a Merge pull request diffblue#251 from diffblue/feature/revert-recording-symbol-table 429c13f Merge pull request diffblue#1520 from smowton/smowton/fix/symbol_table_writer_erase d9f3a2f Revert "Disable OSX builds" 81bb39c Symbol-table writer: fix use of map key after erasure 021fe8f Merge pull request diffblue#1492 from tautschnig/perf-test 0729e3d Merge pull request diffblue#1517 from NathanJPhillips/bugfix/journaling-symbol-table-constructor 93ae9f3 Merge pull request diffblue#1527 from diffblue/revert-1510-always-inline c4ed1ae Revert security-scanner version of recording symbol table e83e307 Fixed scope of moved symbol 535f1df Revert "Fully process always_inline" 0096451 Replace broken copy constructor with move constructor a6adb19 Fix more catch std::string occurances 22a876f Merge pull request diffblue#1523 from reuk/reuk/update-compiling-instructions 8fe258b Update COMPILING with cmake setup instructions 99592b3 Merge pull request diffblue#1504 from andreast271/update-windows-build dff22b8 Make Windows compilation instructions more prescriptive bc3bc8f Merge pull request diffblue#1511 from tautschnig/fix-graphml 358829c Merge pull request diffblue#1510 from tautschnig/always-inline 3e77dd6 Merge pull request diffblue#1496 from smowton/smowton/feature/symbol_table_writer d115b4e catch by const ref instead of by value or non-const ref 444d824 Fix graphml output of concurrency witnesses 08c512d Make Windows compilation instructions more prescriptive bcf8ff3 Update documentation for building cbmc on windows. Update makefiles to use reasonable default compiler for cygwin build. Allow alternative downloader selection from make command line. 728dbb5 Merge pull request diffblue#1508 from smowton/smowton/1420-fragments/value_set_debugging 9d9e50d Merge pull request diffblue#1507 from smowton/smowton/1420-fragments/factor_java_object_init b2104b0 Merge pull request diffblue#1506 from smowton/smowton/1420-fragments/typecheck_expr_cleanup 7175efe Merge pull request diffblue#1505 from smowton/smowton/1420-fragments/invariants 7537302 Adding a java_lang_object_init function 86513ee Merge pull request diffblue#1324 from reuk/reuk/clang-format ea4a777 Merge pull request diffblue#1503 from reuk/reuk/rebuild-ansi-c-when-necessary d9c0598 [pointer-analysis] Better debugging information in pointer analysis 3146336 Remove unnecessary includes in java-typecheck 10b5c8e [java-bytecode/typecheck] Style: Changing assertions in preconditions 2afe377 Fully interpret __attribute__((always_inline)) 8eaf89e Apply symbol replacement in type_arg members 13a7553 Rebuild ansi-c library if non-source dependencies change b97a766 Merge pull request diffblue#1403 from karkhaz/kk-regenerate-arch-flags-binaries a4dc986 Merge pull request diffblue#1484 from diffblue/interpreter_size_t 9d4e0ca Merge pull request diffblue#1217 from KPouliasis/show_functions_dfs c3e6726 Script to automate performance evaluation of CBMC on AWS 912ee38 Improve symbol table style 6b1a49d Add missing goto-statistics file to Makefile d512204 Add cbmc and jbmc as install targets bc887c5 Merge commit '93e2d7626046f90e14de76abbaf16c57a0425d8a' into pull-support-20171019 c5c77ac Merge pull request diffblue#1495 from diffblue/codeowners2 f154d16 Merge pull request diffblue#1487 from martin-cs/goto-analyzer-6-part2 4955417 initialize_goto_model now returns a goto_model 56f924c Merge pull request diffblue#1483 from diffblue/signature_initialize_goto_model eef32db Methods for ai_baset to allow access to the ai_base_domaint for a location. aae984a Disable the regression test for now as it depends on the variable sensitivity domain. 3050c53 Don't stop when recursion found 93f2e1f Use is_bottom() to catch unreachable functions. 5b604ae Update the mock domain with the new ai_domain_baset interface. f9ca353 Add is_bottom() and is_top() to ai_domain_baset and derived domains. 88d8673 Rename the XML output to something a bit more meaningful. 2110cd1 Make formatting stage non-blocking on Travis a24ac3d Fixup compiling.md with more clang-format install instructions c3c24e2 Add symbol table writer 98643d7 initialize_goto_model now returns a goto_model fd6acc5 initial proposal for owners of code f39ae5c use mp_integer for addresses f6ae635 use std::size_t in interpreter 55e6594 Fixup cpplint.py 9d4b827 Update coding standard 8482b35 Add information about using clang-format 1dcc82c Convert COMPILING to markdown format 554cb54 Adjust cpplint to disable whitespace checks by default 6ce0dba Add travis style check f18979a Add clang-format config 622e2e3 Merge branch 'develop' into show_functions_dfs bea696a Regenerated cross-compiled arch flag test binaries 1fab1c1 Fixed show-call-sequences deature of goto instrument; added test suite git-subtree-dir: cbmc git-subtree-split: 739c7f5
Update makefiles to use reasonable default compiler for cygwin build.
Allow alternative downloader selection from make command line.