[clang] [analyzer] Fix tests broken by empty %z3_include_dir (PR #146042)

[Balazs Benics via cfe-commits]

=?utf-8?q?Donát?= Nagy <donat.nagy at ericsson.com>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/146042 at 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