=?utf-8?q?Donát?= Nagy <donat.n...@ericsson.com>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/146...@github.com>
================
@@ -173,13 +173,16 @@ def have_host_clang_repl_cuda():
config.available_features.add("staticanalyzer")
tools.append("clang-check")
+ I_z3_include_dir = ""
if config.clang_staticanalyzer_z3:
config.available_features.add("z3")
- config.substitutions.append(
- ("%z3_include_dir", config.clang_staticanalyzer_z3_include_dir)
- )
+ if config.clang_staticanalyzer_z3_include_dir:
----------------
steakhal wrote:
If you check `llvm/cmake/modules/FindZ3.cmake`, then you can see that
`Z3_INCLUDE_DIR` and `Z3_LIBRARIES` cmake variables must be defined if Z3 is
detected.
By judging this section of code from llvm/CMakeLists.txt:
```
option(LLVM_ENABLE_Z3_SOLVER
"Enable Support for the Z3 constraint solver in LLVM."
${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
)
if (LLVM_ENABLE_Z3_SOLVER)
find_package(Z3 4.8.9)
if (LLVM_Z3_INSTALL_DIR)
if (NOT Z3_FOUND)
message(FATAL_ERROR "Z3 >= 4.8.9 has not been found in
LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
endif()
endif()
if (NOT Z3_FOUND)
message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not
available.")
endif()
set(LLVM_WITH_Z3 1)
endif()
set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
```
I think `LLVM_WITH_Z3` can only be true if `Z3_FOUND` is true, which is only
the case if `find_package(Z3 4.8.9)` find Z3 when executing
`llvm/cmake/modules/FindZ3.cmake`, which defines the `Z3_INCLUDE_DIR` and
`Z3_LIBRARIES` variables.
It has checks that `Z3_INCLUDE_DIR` must exist and contain a file called
`z3_version.h`.
So in sight of this, I don't think there is anything to be fixed here.
https://github.com/llvm/llvm-project/pull/146042
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
