https://github.com/steakhal created https://github.com/llvm/llvm-project/pull/205370
The Z3 constraint manager backend (selected via -analyzer-constraints=z3) is unmaintained and known to crash on real-world input. Rename the user-facing flag to unsupported-z3 and reword its description so users see up front that the backend is unsupported and crash-prone -- patches welcome, crash reports are not. Assisted-By: claude From fc23d668622e552f4fe959bd73b66808d1b318c9 Mon Sep 17 00:00:00 2001 From: Balazs Benics <[email protected]> Date: Tue, 23 Jun 2026 16:50:10 +0100 Subject: [PATCH] [analyzer] Rename z3 constraint manager backend to unsupported-z3 The Z3 constraint manager backend (selected via -analyzer-constraints=z3) is unmaintained and known to crash on real-world input. Rename the user-facing flag to unsupported-z3 and reword its description so users see up front that the backend is unsupported and crash-prone -- patches welcome, crash reports are not. Assisted-By: claude --- clang/docs/ReleaseNotes.rst | 4 ++++ clang/include/clang/Basic/DiagnosticDriverKinds.td | 4 ++-- clang/include/clang/StaticAnalyzer/Core/Analyses.def | 4 +++- clang/test/Analysis/missing-z3-nocrash.c | 6 +++--- clang/test/Analysis/z3/D83660.c | 2 +- clang/test/Analysis/z3/pretty-dump.c | 2 +- clang/test/Analysis/z3/z3-unarysymexpr.c | 2 +- 7 files changed, 15 insertions(+), 9 deletions(-) diff --git a/clang/docs/ReleaseNotes.rst b/clang/docs/ReleaseNotes.rst index e86f1d9602bed..c54d252c84787 100644 --- a/clang/docs/ReleaseNotes.rst +++ b/clang/docs/ReleaseNotes.rst @@ -1036,6 +1036,10 @@ Code Completion Static Analyzer --------------- +- The ``-analyzer-constraints`` option ``z3`` was renamed to ``unsupported-z3`` + because the Z3-based (constraint) solver was known for crashing for years now. + Didn't receive support, so it was marked unsupported. + Crash and bug fixes ^^^^^^^^^^^^^^^^^^^ diff --git a/clang/include/clang/Basic/DiagnosticDriverKinds.td b/clang/include/clang/Basic/DiagnosticDriverKinds.td index 8edac14f4972a..3f8fc16e346cf 100644 --- a/clang/include/clang/Basic/DiagnosticDriverKinds.td +++ b/clang/include/clang/Basic/DiagnosticDriverKinds.td @@ -597,8 +597,8 @@ def err_analyzer_checker_option_invalid_input : Error< def err_analyzer_checker_incompatible_analyzer_option : Error< "checker cannot be enabled with analyzer option '%0' == %1">; def err_analyzer_not_built_with_z3 : Error< - "analyzer constraint manager 'z3' is only available if LLVM was built with " - "-DLLVM_ENABLE_Z3_SOLVER=ON">; + "analyzer constraint manager 'unsupported-z3' is only available if LLVM was " + "built with -DLLVM_ENABLE_Z3_SOLVER=ON">; def warn_drv_needs_hvx : Warning< "%0 requires HVX, use -mhvx/-mhvx= to enable it">, diff --git a/clang/include/clang/StaticAnalyzer/Core/Analyses.def b/clang/include/clang/StaticAnalyzer/Core/Analyses.def index 51803e7c1f0d2..8ef7f2e6c7d3f 100644 --- a/clang/include/clang/StaticAnalyzer/Core/Analyses.def +++ b/clang/include/clang/StaticAnalyzer/Core/Analyses.def @@ -18,7 +18,9 @@ ANALYSIS_CONSTRAINTS(RangeConstraints, "range", "Use constraint tracking of concrete value ranges", CreateRangeConstraintManager) -ANALYSIS_CONSTRAINTS(Z3Constraints, "z3", "Use Z3 contraint solver", +ANALYSIS_CONSTRAINTS(Z3Constraints, "unsupported-z3", + "[UNSUPPORTED] Z3 SMT solver. Known to crash; patches " + "welcome, crash reports are not.", CreateZ3ConstraintManager) #ifndef ANALYSIS_DIAGNOSTICS diff --git a/clang/test/Analysis/missing-z3-nocrash.c b/clang/test/Analysis/missing-z3-nocrash.c index 2e345ad00f5ab..ca2e4e038dc03 100644 --- a/clang/test/Analysis/missing-z3-nocrash.c +++ b/clang/test/Analysis/missing-z3-nocrash.c @@ -1,5 +1,5 @@ -// RUN: not %clang_analyze_cc1 -analyzer-constraints=z3 %s 2>&1 | FileCheck %s +// RUN: not %clang_analyze_cc1 -analyzer-constraints=unsupported-z3 %s 2>&1 | FileCheck %s // UNSUPPORTED: z3 -// CHECK: error: analyzer constraint manager 'z3' is only available if LLVM -// CHECK: was built with -DLLVM_ENABLE_Z3_SOLVER=ON +// CHECK: error: analyzer constraint manager 'unsupported-z3' is only available +// CHECK-SAME: if LLVM was built with -DLLVM_ENABLE_Z3_SOLVER=ON diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c index b4f0539f7e8a7..ad230de8a620d 100644 --- a/clang/test/Analysis/z3/D83660.c +++ b/clang/test/Analysis/z3/D83660.c @@ -1,6 +1,6 @@ // RUN: env Z3_SOLVER_RESULTS="SAT,SAT,SAT,SAT,UNDEF" \ // RUN: LD_PRELOAD="%llvmshlibdir/MockZ3SolverCheck%pluginext" \ -// RUN: %clang_analyze_cc1 -analyzer-constraints=z3 \ +// RUN: %clang_analyze_cc1 -analyzer-constraints=unsupported-z3 \ // RUN: -analyzer-checker=core %s -verify // // REQUIRES: z3, z3-mock, asserts, system-linux diff --git a/clang/test/Analysis/z3/pretty-dump.c b/clang/test/Analysis/z3/pretty-dump.c index e6cd6d83373b8..a20004c0c335d 100644 --- a/clang/test/Analysis/z3/pretty-dump.c +++ b/clang/test/Analysis/z3/pretty-dump.c @@ -1,4 +1,4 @@ -// RUN: %clang_analyze_cc1 -analyzer-constraints=z3 \ +// RUN: %clang_analyze_cc1 -analyzer-constraints=unsupported-z3 \ // RUN: -analyzer-checker=core,debug.ExprInspection %s 2>&1 | FileCheck %s // // REQUIRES: z3 diff --git a/clang/test/Analysis/z3/z3-unarysymexpr.c b/clang/test/Analysis/z3/z3-unarysymexpr.c index efe558c3146e8..bcdc2b6a66f10 100644 --- a/clang/test/Analysis/z3/z3-unarysymexpr.c +++ b/clang/test/Analysis/z3/z3-unarysymexpr.c @@ -1,5 +1,5 @@ // RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \ -// RUN: -analyzer-constraints=z3 +// RUN: -analyzer-constraints=unsupported-z3 // RUN: %clang_analyze_cc1 -verify %s \ // RUN: -analyzer-checker=core,debug.ExprInspection \ // RUN: -analyzer-config crosscheck-with-z3=true _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
