Author: esteffin
Date: Sat Oct 13 12:45:48 2018
New Revision: 344464
URL: http://llvm.org/viewvc/llvm-project?rev=344464&view=rev
Log:
[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
Modified:
cfe/trunk/CMakeLists.txt
cfe/trunk/cmake/modules/FindZ3.cmake
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/CMakeLists.txt
URL:
http://llvm.org/viewvc/llvm-project/cfe/trunk/CMakeLists.txt?rev=344464&r1=344463&r2=344464&view=diff
==
--- cfe/trunk/CMakeLists.txt (original)
+++ cfe/trunk/CMakeLists.txt Sat Oct 13 12:45:48 2018
@@ -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)
Modified: cfe/trunk/cmake/modules/FindZ3.cmake
URL:
http://llvm.org/viewvc/llvm-project/cfe/trunk/cmake/modules/FindZ3.cmake?rev=344464&r1=344463&r2=344464&view=diff
==
--- cfe/trunk/cmake/modules/FindZ3.cmake (original)
+++ cfe/trunk/cmake/modules/FindZ3.cmake Sat Oct 13 12:45:48 2018
@@ -1,13 +1,36 @@
+# Looking for Z3 in CLANG_ANALYZER_Z3_INSTALL_DIR
find_path(Z3_INCLUDE_DIR NAMES z3.h
+ NO_DEFAULT_PATH
+ PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}/include
PATH_SUFFIXES libz3 z3
)
find_library(Z3_LIBRARIES NAMES z3 libz3
+ NO_DEFAULT_PATH
+ PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
+ PATH_SUFFIXES lib bin
)
-find_program(Z3_EXECUTABLE z3)
+find_program(Z3_EXECUTABLE z3
+ NO_DEFAULT_PATH
+ PATHS ${CLANG_ANALYZER_Z3_INSTALL_DIR}
+ PATH_SUFFIXES bin
+ )
+
+# If Z3 has not been found in CLANG_ANALYZER_Z3_INSTALL_DIR look in the
default directories
+find_path(Z3_INCLUDE_DIR NAMES z3.h
+ PATH_SUFFIXES libz3 z3
+ )
+
+find_library(Z3_LIBRARIES NAMES z3 libz3
+ PATH_SUFFIXES lib bin
+ )
+
+find_program(Z3_EXECUTABLE z3
+ PATH_SUFFIXES bin
+ )
-if(Z3_INCLUDE_DIR AND Z3_EXECUTABLE)
+if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
execute_process (COMMAND ${Z3_EXECUTABLE} -version
OUTPUT_VARIABLE libz3_version_str
ERROR_QUIET
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL:
http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=344464&r1=344463&r2=344464&view=diff
==
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3Const
