This revision was automatically updated to reflect the committed changes.
Closed by commit rC353371: Got rid of the `Z3ConstraintManager` class (authored
by mramalho, committed by ).
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
Changed prior to commit:
https://reviews.llvm.org/D54976?vs=176119&id=185696#toc
Repository:
rC Clang
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D54976/new/
https://reviews.llvm.org/D54976
Files:
include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -814,14 +814,6 @@
}
}; // 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 @@
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());
}
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -26,12 +26,11 @@
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;
//===------------------------------------------------------------------===//
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -814,14 +814,6 @@
}
}; // 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 @@
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());
}
Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -26,12 +26,11 @@
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;
//===------------------------------------------------------------------===//
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
