diff options
| author | Daniel Kirchner <daniel@ekpyron.org> | 2018-08-09 21:45:52 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-09 21:45:52 +0800 |
| commit | b6e352f694caa3f2d540b0995042db7b742b1b56 (patch) | |
| tree | 20fda4d790accd70ecf8beb384edd33c5ac8015e /libsolidity | |
| parent | 5535fc0526788eb944589d255b1be842786287bf (diff) | |
| parent | 46b0feb6029719ed8db6c9fd30dfde31b9f78521 (diff) | |
| download | dexon-solidity-b6e352f694caa3f2d540b0995042db7b742b1b56.tar.gz dexon-solidity-b6e352f694caa3f2d540b0995042db7b742b1b56.tar.zst dexon-solidity-b6e352f694caa3f2d540b0995042db7b742b1b56.zip | |
Merge pull request #4767 from ethereum/cvc4Build
Add workarounds for building against CVC4 on ArchLinux.
Diffstat (limited to 'libsolidity')
| -rw-r--r-- | libsolidity/CMakeLists.txt | 17 | ||||
| -rw-r--r-- | libsolidity/formal/CVC4Interface.h | 11 |
2 files changed, 16 insertions, 12 deletions
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 49095fff..91a4678a 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -11,17 +11,11 @@ else() list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp") endif() -find_package(GMP QUIET) find_package(CVC4 QUIET) if (${CVC4_FOUND}) - if (${GMP_FOUND}) - include_directories(${CVC4_INCLUDE_DIR}) - add_definitions(-DHAVE_CVC4) - message("CVC4 SMT solver and GMP found. This enables optional SMT checking with CVC4.") - else() - message("CVC4 SMT solver found but its dependency GMP was NOT found. Optional SMT checking with CVC4 will not be available. Please install GMP if it is desired.") - list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") - endif() + include_directories(${CVC4_INCLUDE_DIR}) + add_definitions(-DHAVE_CVC4) + message("CVC4 SMT solver found. This enables optional SMT checking with CVC4.") else() list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") endif() @@ -38,7 +32,6 @@ if (${Z3_FOUND}) target_link_libraries(solidity PUBLIC ${Z3_LIBRARY}) endif() -if (${CVC4_FOUND} AND ${GMP_FOUND}) - target_link_libraries(solidity PUBLIC ${CVC4_LIBRARY}) - target_link_libraries(solidity PUBLIC ${GMP_LIBRARY}) +if (${CVC4_FOUND}) + target_link_libraries(solidity PUBLIC ${CVC4_LIBRARIES}) endif() diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h index dcd87525..cd6d761d 100644 --- a/libsolidity/formal/CVC4Interface.h +++ b/libsolidity/formal/CVC4Interface.h @@ -21,8 +21,19 @@ #include <boost/noncopyable.hpp> +#if defined(__GLIBC__) +// The CVC4 headers includes the deprecated system headers <ext/hash_map> +// and <ext/hash_set>. These headers cause a warning that will break the +// build, unless _GLIBCXX_PERMIT_BACKWARD_HASH is set. +#define _GLIBCXX_PERMIT_BACKWARD_HASH +#endif + #include <cvc4/cvc4.h> +#if defined(__GLIBC__) +#undef _GLIBCXX_PERMIT_BACKWARD_HASH +#endif + namespace dev { namespace solidity |