diff options
| author | Enrico Steffinlongo <enrico.steffinlongo@gmail.com> | 2018-10-13 19:45:48 +0000 |
|---|---|---|
| committer | Enrico Steffinlongo <enrico.steffinlongo@gmail.com> | 2018-10-13 19:45:48 +0000 |
| commit | b4d73f48e2bec73dcfc2dbede2acc39ce6aee93b (patch) | |
| tree | 0e0d49051b5ff12d46e84153ea6ff8a5e8969057 /CMakeLists.txt | |
| parent | 8693e0ee6a25277d61bd482455d74a5089ea2add (diff) | |
| download | clang-b4d73f48e2bec73dcfc2dbede2acc39ce6aee93b.tar.gz | |
[analyzer] Improved cmake configuration for Z3
Summary:
Enhanced support for Z3 in the cmake configuration of clang; now it is possible to specify any arbitrary Z3 install prefix (CLANG_ANALYZER_Z3_PREFIX) to cmake with lib (or bin) and include folders. Before the patch only in cmake default locations
were searched (https://cmake.org/cmake/help/v3.4/command/find_path.html).
Specifying any CLANG_ANALYZER_Z3_PREFIX will force also CLANG_ANALYZER_BUILD_Z3 to ON.
Removed also Z3 4.5 version requirement since it was not checked, and now Clang works with Z3 4.7
Reviewers: NoQ, george.karpenkov, mikhail.ramalho
Reviewed By: george.karpenkov
Subscribers: rnkovacs, NoQ, esteffin, george.karpenkov, delcypher, ddcc, mgorny, xazax.hun, szepet, a.sidorin, Szelethus
Tags: #clang
Differential Revision: https://reviews.llvm.org/D50818
git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@344464 91177308-0d34-0410-b5e6-96231b3b80d8
Diffstat (limited to 'CMakeLists.txt')
| -rw-r--r-- | CMakeLists.txt | 35 |
1 files changed, 24 insertions, 11 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 93d73ffa53..3f5c3ae2ac 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -394,22 +394,35 @@ option(CLANG_BUILD_TOOLS option(CLANG_ENABLE_ARCMT "Build ARCMT." ON) option(CLANG_ENABLE_STATIC_ANALYZER "Build static analyzer." ON) -option(CLANG_ANALYZER_BUILD_Z3 - "Build the static analyzer with the Z3 constraint manager." OFF) +set(CLANG_ANALYZER_Z3_INSTALL_DIR "" CACHE STRING "Install directory of the Z3 solver.") -option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF) +find_package(Z3 4.7.1 EXACT) -if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_BUILD_Z3)) - message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") +if (CLANG_ANALYZER_Z3_INSTALL_DIR) + if (NOT Z3_FOUND) + message(FATAL_ERROR "Z3 4.7.1 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR: ${CLANG_ANALYZER_Z3_INSTALL_DIR}.") + endif() endif() -if(CLANG_ANALYZER_BUILD_Z3) - find_package(Z3 4.5) - if(Z3_FOUND) - set(CLANG_ANALYZER_WITH_Z3 1) - else() - message(FATAL_ERROR "Cannot find Z3 header file or shared library") +set(CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}") + +option(CLANG_ANALYZER_ENABLE_Z3_SOLVER + "Enable Support for the Z3 constraint solver in the Clang Static Analyzer." + ${CLANG_ANALYZER_ENABLE_Z3_SOLVER_DEFAULT} +) + +if (CLANG_ANALYZER_ENABLE_Z3_SOLVER) + if (NOT Z3_FOUND) + message(FATAL_ERROR "CLANG_ANALYZER_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.") endif() + + set(CLANG_ANALYZER_WITH_Z3 1) +endif() + +option(CLANG_ENABLE_PROTO_FUZZER "Build Clang protobuf fuzzer." OFF) + +if(NOT CLANG_ENABLE_STATIC_ANALYZER AND (CLANG_ENABLE_ARCMT OR CLANG_ANALYZER_ENABLE_Z3_SOLVER)) + message(FATAL_ERROR "Cannot disable static analyzer while enabling ARCMT or Z3") endif() if(CLANG_ENABLE_ARCMT) |