Author: Balázs Benics Date: 2026-07-02T12:31:30Z New Revision: 43082d6efa9c819a7b4ddf4ecfa963748caa82de
URL: https://github.com/llvm/llvm-project/commit/43082d6efa9c819a7b4ddf4ecfa963748caa82de DIFF: https://github.com/llvm/llvm-project/commit/43082d6efa9c819a7b4ddf4ecfa963748caa82de.diff LOG: [analyzer] Rename z3 constraint manager backend to unsupported-z3 (#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 Added: Modified: clang/docs/ReleaseNotes.md clang/include/clang/Basic/DiagnosticDriverKinds.td clang/include/clang/StaticAnalyzer/Core/Analyses.def clang/test/Analysis/missing-z3-nocrash.c clang/test/Analysis/z3/D83660.c clang/test/Analysis/z3/pretty-dump.c clang/test/Analysis/z3/z3-unarysymexpr.c Removed: ################################################################################ diff --git a/clang/docs/ReleaseNotes.md b/clang/docs/ReleaseNotes.md index fc8b0d369b979..0f252fdf3601b 100644 --- a/clang/docs/ReleaseNotes.md +++ b/clang/docs/ReleaseNotes.md @@ -1057,6 +1057,10 @@ latest release, please see the [Clang Web Site](https://clang.llvm.org) or the ### 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 - Fixed `security.VAList` checker producing false positives when analyzing 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
