diff options
| author | Leonardo Alt <leonardoaltt@gmail.com> | 2018-04-07 00:01:40 +0800 |
|---|---|---|
| committer | Alex Beregszaszi <alex@rtfs.hu> | 2018-04-17 19:26:58 +0800 |
| commit | ae3350ae0320d140a427d2fa318e7002745a73a5 (patch) | |
| tree | e4da5e3619baa56b09509004c58b1b5d12594e48 /libsolidity/CMakeLists.txt | |
| parent | 842fd0cd2cef3c11c392b7820e178fd0d034fa07 (diff) | |
| download | dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.tar.gz dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.tar.zst dexon-solidity-ae3350ae0320d140a427d2fa318e7002745a73a5.zip | |
[SMTChecker] Integration with CVC4
Diffstat (limited to 'libsolidity/CMakeLists.txt')
| -rw-r--r-- | libsolidity/CMakeLists.txt | 26 |
1 files changed, 23 insertions, 3 deletions
diff --git a/libsolidity/CMakeLists.txt b/libsolidity/CMakeLists.txt index 99612c40..97b01c83 100644 --- a/libsolidity/CMakeLists.txt +++ b/libsolidity/CMakeLists.txt @@ -6,10 +6,25 @@ find_package(Z3 QUIET) if (${Z3_FOUND}) include_directories(${Z3_INCLUDE_DIR}) add_definitions(-DHAVE_Z3) - message("Z3 SMT solver found. This enables optional SMT checking.") + message("Z3 SMT solver found. This enables optional SMT checking with Z3.") + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") else() - message("Z3 SMT solver NOT found. Optional SMT checking will not be available. Please install Z3 if it is desired.") list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/Z3Interface.cpp") + 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() + else() + message("No SMT solver found (Z3 or CVC4). Optional SMT checking will not be available. Please install Z3 or CVC4 if it is desired.") + list(REMOVE_ITEM sources "${CMAKE_CURRENT_SOURCE_DIR}/formal/CVC4Interface.cpp") + endif() endif() add_library(solidity ${sources} ${headers}) @@ -17,4 +32,9 @@ target_link_libraries(solidity PUBLIC evmasm devcore) if (${Z3_FOUND}) target_link_libraries(solidity PUBLIC ${Z3_LIBRARY}) -endif()
\ No newline at end of file +endif() + +if (${CVC4_FOUND} AND ${GMP_FOUND}) + target_link_libraries(solidity PUBLIC ${CVC4_LIBRARY}) + target_link_libraries(solidity PUBLIC ${GMP_LIBRARY}) +endif() |