[clang] e34e021 - [clang] Fix tests requiring Z3 headers in standalone builds (#146200)

[via cfe-commits]

Author: Michał Górny
Date: 2025-06-28T09:10:49+02:00
New Revision: e34e02128ec5eb89e36a8f0f7307dcbcfecabbee

URL: https://github.com/llvm/llvm-project/commit/e34e02128ec5eb89e36a8f0f7307dcbcfecabbee
DIFF: https://github.com/llvm/llvm-project/commit/e34e02128ec5eb89e36a8f0f7307dcbcfecabbee.diff

LOG: [clang] Fix tests requiring Z3 headers in standalone builds (#146200)

Fix running tests that require Z3 headers in standalone build. They were
wrongly relying on `Z3_INCLUDE_DIR` being passed through from LLVM,
which is not the case for a standalone build. Instead, perform
`find_package(Z3)` again to find Z3 development files and set
`Z3_INCLUDE_DIR`. While at it, handle the possibility that Z3
development package is no longer installed -- run the tests only if both
LLVM has been built against Z3, and the headers are still available.

https://github.com/llvm/llvm-project/pull/145731#issuecomment-3009487525

Signed-off-by: Michał Górny <mgorny at gentoo.org>

Added: 
    

Modified: 
    clang/CMakeLists.txt
    clang/test/Analysis/z3-crosscheck-max-attempts.cpp
    clang/test/Analysis/z3/D83660.c
    clang/test/CMakeLists.txt
    clang/test/lit.cfg.py
    clang/test/lit.site.cfg.py.in

Removed: 
    


################################################################################
diff  --git a/clang/CMakeLists.txt b/clang/CMakeLists.txt
index 94607a8e8473c..1bb73599970c1 100644
--- a/clang/CMakeLists.txt
+++ b/clang/CMakeLists.txt
@@ -150,6 +150,12 @@ if(CLANG_BUILT_STANDALONE)
     endif()
 
     umbrella_lit_testsuite_begin(check-all)
+
+    # If LLVM was built with Z3, check if we still have the headers around.
+    # They are used by a few tests.
+    if (LLVM_WITH_Z3)
+      find_package(Z3 4.8.9)
+    endif()
   endif() # LLVM_INCLUDE_TESTS
 endif() # standalone
 

diff  --git a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
index 572e452fdcac2..312e442f23f4f 100644
--- a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
+++ b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
@@ -32,7 +32,7 @@
 // RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT"   %{mocked_clang} %{attempts}=3 -verify=accepted
 
 
-// REQUIRES: z3, asserts, shell, system-linux
+// REQUIRES: z3, z3-devel, asserts, shell, system-linux
 
 // refuted-no-diagnostics
 

diff  --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index 0a7c8bab8e345..2ca4a4d0b53e9 100644
--- a/clang/test/Analysis/z3/D83660.c
+++ b/clang/test/Analysis/z3/D83660.c
@@ -8,7 +8,7 @@
 // RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer \
 // RUN:   -analyzer-checker=core %s -verify
 //
-// REQUIRES: z3, asserts, shell, system-linux
+// REQUIRES: z3, z3-devel, asserts, shell, system-linux
 //
 // Works only with the z3 constraint manager.
 // expected-no-diagnostics

diff  --git a/clang/test/CMakeLists.txt b/clang/test/CMakeLists.txt
index e5b4a3bb84645..8baea5b0ca937 100644
--- a/clang/test/CMakeLists.txt
+++ b/clang/test/CMakeLists.txt
@@ -29,6 +29,14 @@ llvm_canonicalize_cmake_booleans(
   LLVM_EXPERIMENTAL_KEY_INSTRUCTIONS
   )
 
+# Run tests requiring Z3 headers only if LLVM was built with Z3
+# and the headers are available while building Clang -- the latter may
+# not be the case when building standalone against installed LLVM.
+set(TEST_WITH_Z3_DEVEL 0)
+if(LLVM_WITH_Z3 AND Z3_FOUND)
+  set(TEST_WITH_Z3_DEVEL 1)
+endif()
+
 configure_lit_site_cfg(
   ${CMAKE_CURRENT_SOURCE_DIR}/lit.site.cfg.py.in
   ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg.py

diff  --git a/clang/test/lit.cfg.py b/clang/test/lit.cfg.py
index bbd95ef4b77de..6375e73f5df82 100644
--- a/clang/test/lit.cfg.py
+++ b/clang/test/lit.cfg.py
@@ -201,9 +201,11 @@ def have_host_clang_repl_cuda():
 
     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_devel:
+            config.available_features.add("z3-devel")
+            config.substitutions.append(
+                ("%z3_include_dir", config.clang_staticanalyzer_z3_include_dir)
+            )
     else:
         config.available_features.add("no-z3")
 

diff  --git a/clang/test/lit.site.cfg.py.in b/clang/test/lit.site.cfg.py.in
index 00480d34852da..ec0e4aa10ed79 100644
--- a/clang/test/lit.site.cfg.py.in
+++ b/clang/test/lit.site.cfg.py.in
@@ -27,6 +27,7 @@ config.clang_default_pie_on_linux = @CLANG_DEFAULT_PIE_ON_LINUX@
 config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@"
 config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@
 config.clang_staticanalyzer_z3 = @LLVM_WITH_Z3@
+config.clang_staticanalyzer_z3_devel = @TEST_WITH_Z3_DEVEL@
 config.clang_staticanalyzer_z3_include_dir = "@Z3_INCLUDE_DIR@"
 config.clang_enable_cir = @CLANG_ENABLE_CIR@
 config.clang_examples = @CLANG_BUILD_EXAMPLES@