forked from OSchip/llvm-project
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 llvm-svn: 353371
This commit is contained in:
parent
c9cd507263
commit
c1f8cad191
|
@ -26,12 +26,11 @@ namespace clang {
|
||||||
namespace ento {
|
namespace ento {
|
||||||
|
|
||||||
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
|
class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
|
||||||
SMTSolverRef &Solver;
|
mutable SMTSolverRef Solver = CreateZ3Solver();
|
||||||
|
|
||||||
public:
|
public:
|
||||||
SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
|
SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB)
|
||||||
SMTSolverRef &S)
|
: SimpleConstraintManager(SE, SB) {}
|
||||||
: SimpleConstraintManager(SE, SB), Solver(S) {}
|
|
||||||
virtual ~SMTConstraintManager() = default;
|
virtual ~SMTConstraintManager() = default;
|
||||||
|
|
||||||
//===------------------------------------------------------------------===//
|
//===------------------------------------------------------------------===//
|
||||||
|
|
|
@ -814,14 +814,6 @@ public:
|
||||||
}
|
}
|
||||||
}; // end class Z3Solver
|
}; // 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
|
} // end anonymous namespace
|
||||||
|
|
||||||
#endif
|
#endif
|
||||||
|
@ -839,12 +831,5 @@ SMTSolverRef clang::ento::CreateZ3Solver() {
|
||||||
|
|
||||||
std::unique_ptr<ConstraintManager>
|
std::unique_ptr<ConstraintManager>
|
||||||
ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
|
ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) {
|
||||||
#if CLANG_ANALYZER_WITH_Z3
|
return llvm::make_unique<SMTConstraintManager>(Eng, StMgr.getSValBuilder());
|
||||||
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
|
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue