r353371 - Got rid of the `Z3ConstraintManager` class
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Feb 6 19:18:10 PST 2019
Author: mramalho
Date: Wed Feb 6 19:18:10 2019
New Revision: 353371
URL: http://llvm.org/viewvc/llvm-project?rev=353371&view=rev
Log:
Got rid of the `Z3ConstraintManager` class
Now, instead of passing the reference to a shared_ptr, we pass the shared_ptr instead.
I've also removed the check if Z3 is present in CreateZ3ConstraintManager as this function already calls CreateZ3Solver that performs the exactly same check.
Differential Revision: https://reviews.llvm.org/D54976
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=353371&r1=353370&r2=353371&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Feb 6 19:18:10 2019
@@ -26,12 +26,11 @@ namespace clang {
namespace ento {
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
- SMTSolverRef &Solver;
+ mutable SMTSolverRef Solver = CreateZ3Solver();
public:
- SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
- SMTSolverRef &S)
- : SimpleConstraintManager(SE, SB), Solver(S) {}
+ SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
+ : SimpleConstraintManager(SE, SB) {}
virtual ~SMTConstraintManager() = default;
//===------------------------------------------------------------------===//
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=353371&r1=353370&r2=353371&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Feb 6 19:18:10 2019
@@ -814,14 +814,6 @@ public:
}
}; // end class Z3Solver
-class Z3ConstraintManager : public SMTConstraintManager {
- SMTSolverRef Solver = CreateZ3Solver();
-
-public:
- Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
- : SMTConstraintManager(SE, SB, Solver) {}
-}; // end class Z3ConstraintManager
-
} // end anonymous namespace
#endif
@@ -839,12 +831,5 @@ SMTSolverRef clang::ento::CreateZ3Solver
std::unique_ptr<ConstraintManager>
ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
-#if CLANG_ANALYZER_WITH_Z3
- return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
-#else
- llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
- "with -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=ON",
- false);
- return nullptr;
-#endif
+ return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
}
More information about the cfe-commits
mailing list