Szelethus created this revision.
Szelethus added reviewers: NoQ, dkrupp, steakhal, martong, balazske.
Szelethus added a project: clang.
Herald added subscribers: ASDenysPetrov, gamesh411, donat.nagy,
mikhail.ramalho, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun.
Szelethus requested review of this revision.
Herald added a subscriber: cfe-commits.
Exactly what it says on the tin! We had a nasty crash with the following
incovation:
$ clang --analyze -Xclang -analyzer-constraints=z3 test.c
fatal error: error in backend: LLVM was not compiled with Z3 support, rebuild
with -DLLVM_ENABLE_Z3_SOLVER=ON
... <stack trace> ...
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D120325
Files:
clang/include/clang/Basic/DiagnosticDriverKinds.td
clang/lib/Frontend/CompilerInvocation.cpp
clang/test/Analysis/missing-z3-nocrash.c
clang/test/lit.cfg.py
Index: clang/test/lit.cfg.py
===================================================================
--- clang/test/lit.cfg.py
+++ clang/test/lit.cfg.py
@@ -100,6 +100,8 @@
if config.clang_staticanalyzer_z3:
config.available_features.add('z3')
+ else:
+ config.available_features.add('no-z3')
check_analyzer_fixit_path = os.path.join(
config.test_source_root, "Analysis", "check-analyzer-fixit.py")
Index: clang/test/Analysis/missing-z3-nocrash.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/missing-z3-nocrash.c
@@ -0,0 +1,5 @@
+// RUN: not %clang_analyze_cc1 -analyzer-constraints=z3 %s 2>&1 | FileCheck %s
+// REQUIRES: no-z3
+
+// CHECK: error: analyzer constraint manager 'z3' is only available if LLVM
+// CHECK: was built with -DLLVM_ENABLE_Z3_SOLVER=ON
Index: clang/lib/Frontend/CompilerInvocation.cpp
===================================================================
--- clang/lib/Frontend/CompilerInvocation.cpp
+++ clang/lib/Frontend/CompilerInvocation.cpp
@@ -915,6 +915,11 @@
Diags.Report(diag::err_drv_invalid_value)
<< A->getAsString(Args) << Name;
} else {
+#if !LLVM_WITH_Z3
+ if (Value == AnalysisConstraints::Z3ConstraintsModel) {
+ Diags.Report(diag::err_analyzer_not_built_with_z3);
+ }
+#endif // LLVM_WITH_Z3
Opts.AnalysisConstraintsOpt = Value;
}
}
Index: clang/include/clang/Basic/DiagnosticDriverKinds.td
===================================================================
--- clang/include/clang/Basic/DiagnosticDriverKinds.td
+++ clang/include/clang/Basic/DiagnosticDriverKinds.td
@@ -441,6 +441,9 @@
"invalid input for checker option '%0', that expects %1">;
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">;
def warn_drv_needs_hvx : Warning<
"%0 requires HVX, use -mhvx/-mhvx= to enable it">,
Index: clang/test/lit.cfg.py
===================================================================
--- clang/test/lit.cfg.py
+++ clang/test/lit.cfg.py
@@ -100,6 +100,8 @@
if config.clang_staticanalyzer_z3:
config.available_features.add('z3')
+ else:
+ config.available_features.add('no-z3')
check_analyzer_fixit_path = os.path.join(
config.test_source_root, "Analysis", "check-analyzer-fixit.py")
Index: clang/test/Analysis/missing-z3-nocrash.c
===================================================================
--- /dev/null
+++ clang/test/Analysis/missing-z3-nocrash.c
@@ -0,0 +1,5 @@
+// RUN: not %clang_analyze_cc1 -analyzer-constraints=z3 %s 2>&1 | FileCheck %s
+// REQUIRES: no-z3
+
+// CHECK: error: analyzer constraint manager 'z3' is only available if LLVM
+// CHECK: was built with -DLLVM_ENABLE_Z3_SOLVER=ON
Index: clang/lib/Frontend/CompilerInvocation.cpp
===================================================================
--- clang/lib/Frontend/CompilerInvocation.cpp
+++ clang/lib/Frontend/CompilerInvocation.cpp
@@ -915,6 +915,11 @@
Diags.Report(diag::err_drv_invalid_value)
<< A->getAsString(Args) << Name;
} else {
+#if !LLVM_WITH_Z3
+ if (Value == AnalysisConstraints::Z3ConstraintsModel) {
+ Diags.Report(diag::err_analyzer_not_built_with_z3);
+ }
+#endif // LLVM_WITH_Z3
Opts.AnalysisConstraintsOpt = Value;
}
}
Index: clang/include/clang/Basic/DiagnosticDriverKinds.td
===================================================================
--- clang/include/clang/Basic/DiagnosticDriverKinds.td
+++ clang/include/clang/Basic/DiagnosticDriverKinds.td
@@ -441,6 +441,9 @@
"invalid input for checker option '%0', that expects %1">;
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">;
def warn_drv_needs_hvx : Warning<
"%0 requires HVX, use -mhvx/-mhvx= to enable it">,
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
