diff options
| -rw-r--r-- | Changelog.md | 1 | ||||
| -rw-r--r-- | cmake/FindCLN.cmake | 3 | ||||
| -rw-r--r-- | cmake/FindCVC4.cmake | 20 | ||||
| -rw-r--r-- | docs/types.rst | 2 | ||||
| -rw-r--r-- | libsolidity/CMakeLists.txt | 17 | ||||
| -rw-r--r-- | libsolidity/formal/CVC4Interface.h | 11 |
6 files changed, 40 insertions, 14 deletions
diff --git a/Changelog.md b/Changelog.md index eec62736..b2f9bf05 100644 --- a/Changelog.md +++ b/Changelog.md @@ -80,6 +80,7 @@ Compiler Features: * Removed ``pragma experimental "v0.5.0";``. Bugfixes: + * Build System: Support versions of CVC4 linked against CLN instead of GMP. In case of compilation issues due to the experimental SMT solver support, the solvers can be disabled when configuring the project with CMake using ``-DUSE_CVC4=OFF`` or ``-DUSE_Z3=OFF``. * Tests: Fix chain parameters to make ipc tests work with newer versions of cpp-ethereum. * Code Generator: Fix allocation of byte arrays (zeroed out too much memory). * Code Generator: Properly handle negative number literals in ABIEncoderV2. diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake new file mode 100644 index 00000000..f2234bb4 --- /dev/null +++ b/cmake/FindCLN.cmake @@ -0,0 +1,3 @@ +find_library(CLN_LIBRARY NAMES cln) +include(FindPackageHandleStandardArgs) +find_package_handle_standard_args(CLN DEFAULT_MSG CLN_LIBRARY) diff --git a/cmake/FindCVC4.cmake b/cmake/FindCVC4.cmake index 90b7ebd5..2649d7c7 100644 --- a/cmake/FindCVC4.cmake +++ b/cmake/FindCVC4.cmake @@ -1,8 +1,26 @@ if (USE_CVC4) find_path(CVC4_INCLUDE_DIR cvc4/cvc4.h) - find_library(CVC4_LIBRARY NAMES cvc4 ) + find_library(CVC4_LIBRARY NAMES cvc4) include(FindPackageHandleStandardArgs) find_package_handle_standard_args(CVC4 DEFAULT_MSG CVC4_LIBRARY CVC4_INCLUDE_DIR) + if(CVC4_FOUND) + # CVC4 may depend on either CLN or GMP. + # We can assume that the one it requires is present on the system, + # so we quietly try to find both and link against them, if they are + # present. + find_package(CLN QUIET) + find_package(GMP QUIET) + + set(CVC4_LIBRARIES ${CVC4_LIBRARY}) + + if (CLN_FOUND) + set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${CLN_LIBRARY}) + endif () + + if (GMP_FOUND) + set(CVC4_LIBRARIES ${CVC4_LIBRARIES} ${GMP_LIBRARY}) + endif () + endif() else() set(CVC4_FOUND FALSE) endif() diff --git a/docs/types.rst b/docs/types.rst index 208966be..bcd3ce9c 100644 --- a/docs/types.rst +++ b/docs/types.rst @@ -134,7 +134,7 @@ and to send Ether (in units of wei) to an address using the ``transfer`` functio if (x.balance < 10 && myAddress.balance >= 10) x.transfer(10); .. note:: - If ``x`` is a contract address, its code (more specifically: its fallback function, if present) will be executed together with the ``transfer`` call (this is a feature of the EVM and cannot be prevented). If that execution runs out of gas or fails in any way, the Ether transfer will be reverted and the current contract will stop with an exception. + If ``x`` is a contract address, its code (more specifically: its :ref:`fallback-function`, if present) will be executed together with the ``transfer`` call (this is a feature of the EVM and cannot be prevented). If that execution runs out of gas or fails in any way, the Ether transfer will be reverted and the current contract will stop with an exception. * ``send`` 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 |