[clang] [llvm] [analyzer] Revert Z3 changes (PR #95916)
via llvm-commits
llvm-commits at lists.llvm.org
Tue Jun 18 05:56:25 PDT 2024
llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT-->
@llvm/pr-subscribers-clang-static-analyzer-1
Author: Balazs Benics (steakhal)
<details>
<summary>Changes</summary>
Requested in:
https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007
Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation"
This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a. This reverts commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab.
---
Patch is 37.47 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/95916.diff
14 Files Affected:
- (modified) clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def (-20)
- (modified) clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (+23)
- (removed) clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h (-92)
- (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (+1-4)
- (modified) clang/lib/StaticAnalyzer/Core/BugReporter.cpp (+6-30)
- (modified) clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (+76)
- (modified) clang/lib/StaticAnalyzer/Core/CMakeLists.txt (-1)
- (removed) clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp (-160)
- (modified) clang/test/Analysis/analyzer-config.c (-3)
- (removed) clang/test/Analysis/z3/crosscheck-statistics.c (-33)
- (modified) clang/unittests/StaticAnalyzer/CMakeLists.txt (-1)
- (removed) clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp (-143)
- (modified) llvm/include/llvm/Support/SMTAPI.h (-19)
- (modified) llvm/lib/Support/Z3Solver.cpp (+20-96)
``````````diff
diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
index 29aa6a3b8a16e..f008c9c581d95 100644
--- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
+++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
@@ -184,26 +184,6 @@ ANALYZER_OPTION(bool, ShouldCrosscheckWithZ3, "crosscheck-with-z3",
"constraint manager backend.",
false)
-ANALYZER_OPTION(
- unsigned, Z3CrosscheckEQClassTimeoutThreshold,
- "crosscheck-with-z3-eqclass-timeout-threshold",
- "Set a timeout for bug report equivalence classes in milliseconds. "
- "If we exhaust this threshold, we will drop the bug report eqclass "
- "instead of doing more Z3 queries. Set 0 for no timeout.", 700)
-
-ANALYZER_OPTION(
- unsigned, Z3CrosscheckTimeoutThreshold,
- "crosscheck-with-z3-timeout-threshold",
- "Set a timeout for individual Z3 queries in milliseconds. "
- "Set 0 for no timeout.", 300)
-
-ANALYZER_OPTION(
- unsigned, Z3CrosscheckRLimitThreshold,
- "crosscheck-with-z3-rlimit-threshold",
- "Set the Z3 resource limit threshold. This sets a deterministic cutoff "
- "point for Z3 queries, as longer queries usually consume more resources. "
- "Set 0 for unlimited.", 400'000)
-
ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile,
"report-in-main-source-file",
"Whether or not the diagnostic report should be always "
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
index f97514955a591..cc3d93aabafda 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -597,6 +597,29 @@ class SuppressInlineDefensiveChecksVisitor final : public BugReporterVisitor {
PathSensitiveBugReport &BR) override;
};
+/// The bug visitor will walk all the nodes in a path and collect all the
+/// constraints. When it reaches the root node, will create a refutation
+/// manager and check if the constraints are satisfiable
+class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
+private:
+ /// Holds the constraints in a given path
+ ConstraintMap Constraints;
+
+public:
+ FalsePositiveRefutationBRVisitor();
+
+ void Profile(llvm::FoldingSetNodeID &ID) const override;
+
+ PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
+ BugReporterContext &BRC,
+ PathSensitiveBugReport &BR) override;
+
+ void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
+ PathSensitiveBugReport &BR) override;
+ void addConstraints(const ExplodedNode *N,
+ bool OverwriteConstraintsOnExistingSyms);
+};
+
/// The visitor detects NoteTags and displays the event notes they contain.
class TagVisitor : public BugReporterVisitor {
public:
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
deleted file mode 100644
index 439f37fa8604f..0000000000000
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
+++ /dev/null
@@ -1,92 +0,0 @@
-//===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===//
-//
-// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-//
-// This file defines the visitor and utilities around it for Z3 report
-// refutation.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
-#define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
-
-#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
-
-namespace clang::ento {
-
-/// The bug visitor will walk all the nodes in a path and collect all the
-/// constraints. When it reaches the root node, will create a refutation
-/// manager and check if the constraints are satisfiable.
-class Z3CrosscheckVisitor final : public BugReporterVisitor {
-public:
- struct Z3Result {
- std::optional<bool> IsSAT = std::nullopt;
- unsigned Z3QueryTimeMilliseconds = 0;
- unsigned UsedRLimit = 0;
- };
- Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
- const AnalyzerOptions &Opts);
-
- void Profile(llvm::FoldingSetNodeID &ID) const override;
-
- PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
- BugReporterContext &BRC,
- PathSensitiveBugReport &BR) override;
-
- void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
- PathSensitiveBugReport &BR) override;
-
-private:
- void addConstraints(const ExplodedNode *N,
- bool OverwriteConstraintsOnExistingSyms);
-
- /// Holds the constraints in a given path.
- ConstraintMap Constraints;
- Z3Result &Result;
- const AnalyzerOptions &Opts;
-};
-
-/// The oracle will decide if a report should be accepted or rejected based on
-/// the results of the Z3 solver and the statistics of the queries of a report
-/// equivalenece class.
-class Z3CrosscheckOracle {
-public:
- explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
-
- enum Z3Decision {
- AcceptReport, // The report was SAT.
- RejectReport, // The report was UNSAT or UNDEF.
- RejectEQClass, // The heuristic suggests to skip the current eqclass.
- };
-
- /// Updates the internal state with the new Z3Result and makes a decision how
- /// to proceed:
- /// - Accept the report if the Z3Result was SAT.
- /// - Suggest dropping the report equvalence class based on the accumulated
- /// statistics.
- /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF.
- ///
- /// Conditions for dropping the equivalence class:
- /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass.
- /// - Hit the 300ms query timeout in the report eqclass.
- /// - Hit the 400'000 rlimit in the report eqclass.
- ///
- /// All these thresholds are configurable via the analyzer options.
- ///
- /// Refer to
- /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to
- /// see why this heuristic was chosen.
- Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta);
-
-private:
- const AnalyzerOptions &Opts;
- unsigned AccumulatedZ3QueryTimeInEqClass = 0; // ms
-};
-
-} // namespace clang::ento
-
-#endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index bf18c353b8508..5116a4c06850d 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -34,10 +34,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
public:
SMTConstraintManager(clang::ento::ExprEngine *EE,
clang::ento::SValBuilder &SB)
- : SimpleConstraintManager(EE, SB) {
- Solver->setBoolParam("model", true); // Enable model finding
- Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/);
- }
+ : SimpleConstraintManager(EE, SB) {}
virtual ~SMTConstraintManager() = default;
//===------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index e2002bfbe594a..14ca507a16d55 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -35,7 +35,6 @@
#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
#include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
-#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
#include "clang/StaticAnalyzer/Core/Checker.h"
#include "clang/StaticAnalyzer/Core/CheckerManager.h"
#include "clang/StaticAnalyzer/Core/CheckerRegistryData.h"
@@ -87,14 +86,6 @@ STATISTIC(MaxValidBugClassSize,
"The maximum number of bug reports in the same equivalence class "
"where at least one report is valid (not suppressed)");
-STATISTIC(NumTimesReportPassesZ3, "Number of reports passed Z3");
-STATISTIC(NumTimesReportRefuted, "Number of reports refuted by Z3");
-STATISTIC(NumTimesReportEQClassAborted,
- "Number of times a report equivalence class was aborted by the Z3 "
- "oracle heuristic");
-STATISTIC(NumTimesReportEQClassWasExhausted,
- "Number of times all reports of an equivalence class was refuted");
-
BugReporterVisitor::~BugReporterVisitor() = default;
void BugReporterContext::anchor() {}
@@ -2843,7 +2834,6 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
ArrayRef<PathSensitiveBugReport *> &bugReports,
PathSensitiveBugReporter &Reporter) {
- Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
@@ -2874,35 +2864,21 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
// If crosscheck is enabled, remove all visitors, add the refutation
// visitor and check again
R->clearVisitors();
- Z3CrosscheckVisitor::Z3Result CrosscheckResult;
- R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
- Reporter.getAnalyzerOptions());
+ R->addVisitor<FalsePositiveRefutationBRVisitor>();
// We don't overwrite the notes inserted by other visitors because the
// refutation manager does not add any new note to the path
generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
- switch (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
- case Z3CrosscheckOracle::RejectReport:
- ++NumTimesReportRefuted;
- R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
- continue;
- case Z3CrosscheckOracle::RejectEQClass:
- ++NumTimesReportEQClassAborted;
- return {};
- case Z3CrosscheckOracle::AcceptReport:
- ++NumTimesReportPassesZ3;
- break;
- }
}
- assert(R->isValid());
- return PathDiagnosticBuilder(std::move(BRC), std::move(BugPath->BugPath),
- BugPath->Report, BugPath->ErrorNode,
- std::move(visitorNotes));
+ // Check if the bug is still valid
+ if (R->isValid())
+ return PathDiagnosticBuilder(
+ std::move(BRC), std::move(BugPath->BugPath), BugPath->Report,
+ BugPath->ErrorNode, std::move(visitorNotes));
}
}
- ++NumTimesReportEQClassWasExhausted;
return {};
}
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index 68dac65949117..487a3bd16b674 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -3446,6 +3446,82 @@ UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC,
return nullptr;
}
+//===----------------------------------------------------------------------===//
+// Implementation of FalsePositiveRefutationBRVisitor.
+//===----------------------------------------------------------------------===//
+
+FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
+ : Constraints(ConstraintMap::Factory().getEmptyMap()) {}
+
+void FalsePositiveRefutationBRVisitor::finalizeVisitor(
+ BugReporterContext &BRC, const ExplodedNode *EndPathNode,
+ PathSensitiveBugReport &BR) {
+ // Collect new constraints
+ addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
+
+ // Create a refutation manager
+ llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
+ ASTContext &Ctx = BRC.getASTContext();
+
+ // Add constraints to the solver
+ for (const auto &I : Constraints) {
+ const SymbolRef Sym = I.first;
+ auto RangeIt = I.second.begin();
+
+ llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
+ RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true);
+ while ((++RangeIt) != I.second.end()) {
+ SMTConstraints = RefutationSolver->mkOr(
+ SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+ RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true));
+ }
+
+ RefutationSolver->addConstraint(SMTConstraints);
+ }
+
+ // And check for satisfiability
+ std::optional<bool> IsSAT = RefutationSolver->check();
+ if (!IsSAT)
+ return;
+
+ if (!*IsSAT)
+ BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+}
+
+void FalsePositiveRefutationBRVisitor::addConstraints(
+ const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
+ // Collect new constraints
+ ConstraintMap NewCs = getConstraintMap(N->getState());
+ ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
+
+ // Add constraints if we don't have them yet
+ for (auto const &C : NewCs) {
+ const SymbolRef &Sym = C.first;
+ if (!Constraints.contains(Sym)) {
+ // This symbol is new, just add the constraint.
+ Constraints = CF.add(Constraints, Sym, C.second);
+ } else if (OverwriteConstraintsOnExistingSyms) {
+ // Overwrite the associated constraint of the Symbol.
+ Constraints = CF.remove(Constraints, Sym);
+ Constraints = CF.add(Constraints, Sym, C.second);
+ }
+ }
+}
+
+PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
+ const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+ addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
+ return nullptr;
+}
+
+void FalsePositiveRefutationBRVisitor::Profile(
+ llvm::FoldingSetNodeID &ID) const {
+ static int Tag = 0;
+ ID.AddPointer(&Tag);
+}
+
//===----------------------------------------------------------------------===//
// Implementation of TagVisitor.
//===----------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
index fb9394a519eb7..8672876c0608d 100644
--- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
@@ -51,7 +51,6 @@ add_clang_library(clangStaticAnalyzerCore
SymbolManager.cpp
TextDiagnostics.cpp
WorkList.cpp
- Z3CrosscheckVisitor.cpp
LINK_LIBS
clangAST
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
deleted file mode 100644
index 739db951b3e18..0000000000000
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ /dev/null
@@ -1,160 +0,0 @@
-//===- Z3CrosscheckVisitor.cpp - Crosscheck reports with Z3 -----*- C++ -*-===//
-//
-// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
-// See https://llvm.org/LICENSE.txt for license information.
-// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
-//
-//===----------------------------------------------------------------------===//
-//
-// This file declares the visitor and utilities around it for Z3 report
-// refutation.
-//
-//===----------------------------------------------------------------------===//
-
-#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
-#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
-#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
-#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
-#include "llvm/ADT/Statistic.h"
-#include "llvm/Support/SMTAPI.h"
-#include "llvm/Support/Timer.h"
-
-#define DEBUG_TYPE "Z3CrosscheckOracle"
-
-STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
-STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
-STATISTIC(NumTimesZ3ExhaustedRLimit,
- "Number of times Z3 query exhausted the rlimit");
-STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
- "Number of times report equivalenece class was cut because it spent "
- "too much time in Z3");
-
-STATISTIC(NumTimesZ3QueryAcceptsReport,
- "Number of Z3 queries accepting a report");
-STATISTIC(NumTimesZ3QueryRejectReport,
- "Number of Z3 queries rejecting a report");
-STATISTIC(NumTimesZ3QueryRejectEQClass,
- "Number of times rejecting an report equivalenece class");
-
-using namespace clang;
-using namespace ento;
-
-Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
- const AnalyzerOptions &Opts)
- : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
- Opts(Opts) {}
-
-void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
- const ExplodedNode *EndPathNode,
- PathSensitiveBugReport &BR) {
- // Collect new constraints
- addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
-
- // Create a refutation manager
- llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
- if (Opts.Z3CrosscheckRLimitThreshold)
- RefutationSolver->setUnsignedParam("rlimit",
- Opts.Z3CrosscheckRLimitThreshold);
- if (Opts.Z3CrosscheckTimeoutThreshold)
- RefutationSolver->setUnsignedParam("timeout",
- Opts.Z3CrosscheckTimeoutThreshold); // ms
-
- ASTContext &Ctx = BRC.getASTContext();
-
- // Add constraints to the solver
- for (const auto &[Sym, Range] : Constraints) {
- auto RangeIt = Range.begin();
-
- llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
- RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
- /*InRange=*/true);
- while ((++RangeIt) != Range.end()) {
- SMTConstraints = RefutationSolver->mkOr(
- SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- RangeIt->From(), RangeIt->To(),
- /*InRange=*/true));
- }
- RefutationSolver->addConstraint(SMTConstraints);
- }
-
- // And check for satisfiability
- llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true);
- std::optional<bool> IsSAT = RefutationSolver->check();
- llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false);
- Diff -= Start;
- Result = Z3Result{
- IsSAT,
- static_cast<unsigned>(Diff.getWallTime() * 1000),
- RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
- };
-}
-
-void Z3CrosscheckVisitor::addConstraints(
- const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
- // Collect new constraints
- ConstraintMap NewCs = getConstraintMap(N->getState());
- ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
-
- // Add constraints if we don't have them yet
- for (auto const &[Sym, Range] : NewCs) {
- if (!Constraints.contains(Sym)) {
- // This symbol is new, just add the constraint.
- Constraints = CF.add(Constraints, Sym, Range);
- } else if (OverwriteConstraintsOnExistingSyms) {
- // Overwrite the associated constraint of the Symbol.
- Constraints = CF.remove(Constraints, Sym);
- Constraints = CF.add(Constraints, Sym, Range);
- }
- }
-}
-
-PathDiagnosticPieceRef
-Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
- ...
[truncated]
``````````
</details>
https://github.com/llvm/llvm-project/pull/95916
More information about the llvm-commits
mailing list