[analyzer] False positive refutation with Z3

Summary: This is a prototype of a bug reporter visitor that invalidates bug reports by re-checking constraints of certain states on the bug path using the Z3 constraint manager backend. The functionality is available under the `crosscheck-with-z3` analyzer config flag.

Reviewers: george.karpenkov, NoQ, dcoughlin, rnkovacs

Reviewed By: george.karpenkov

Subscribers: rnkovacs, NoQ, george.karpenkov, dcoughlin, xbolva00, ddcc, mikhail.ramalho, MTC, fhahn, whisperity, baloghadamsoftware, szepet, a.sidorin, gsd, dkrupp, xazax.hun, cfe-commits

Differential Revision: https://reviews.llvm.org/D45517

llvm-svn: 333903

1 files changed, 6 insertions, 0 deletions

diff --git a/clang/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp b/clang/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
index 33e482dd407..bddd4435a75 100644
--- a/clang/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ b/clang/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -296,6 +296,12 @@ bool AnalyzerOptions::shouldSuppressFromCXXStandardLibrary() {
                           /* Default = */ true);
 }
 
+bool AnalyzerOptions::shouldCrosscheckWithZ3() {
+  return getBooleanOption(CrosscheckWithZ3,
+                          "crosscheck-with-z3",
+                          /* Default = */ false);
+}
+
 bool AnalyzerOptions::shouldReportIssuesInMainSourceFile() {
   return getBooleanOption(ReportIssuesInMainSourceFile,
                           "report-in-main-source-file",