diff options
author | Daniel Schemmel <daniel@schemmel.net> | 2023-03-24 15:05:43 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-04-21 13:07:31 +0100 |
commit | ac0fa15ab0679fe1b5067b07647b0701ae3bc347 (patch) | |
tree | f2294eb5f0795ee9ce0f92d527242b7b7a507e79 /tools | |
parent | e9d77be6c688836d68a2be5f3f0a02e63f392bb8 (diff) | |
download | klee-ac0fa15ab0679fe1b5067b07647b0701ae3bc347.tar.gz |
use unique_ptr all throughout the solver chain
Diffstat (limited to 'tools')
-rw-r--r-- | tools/kleaver/main.cpp | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index eed4e4c9..51298dfb 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -29,12 +29,11 @@ #include "llvm/Support/ManagedStatic.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/raw_ostream.h" +#include "llvm/Support/Signals.h" #include <sys/stat.h> #include <unistd.h> - - -#include "llvm/Support/Signals.h" +#include <utility> using namespace llvm; using namespace klee; @@ -200,7 +199,7 @@ static bool EvaluateInputAST(const char *Filename, if (!success) return false; - Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); + std::unique_ptr<Solver> coreSolver = klee::createCoreSolver(CoreSolverToUse); if (CoreSolverToUse != DUMMY_SOLVER) { const time::Span maxCoreSolverTime(MaxCoreSolverTime); @@ -209,11 +208,11 @@ static bool EvaluateInputAST(const char *Filename, } } - Solver *S = constructSolverChain(coreSolver, - getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME)); + std::unique_ptr<Solver> S = constructSolverChain( + std::move(coreSolver), getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(ALL_QUERIES_KQUERY_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_KQUERY_FILE_NAME)); unsigned Index = 0; for (std::vector<Decl*>::iterator it = Decls.begin(), @@ -294,8 +293,6 @@ static bool EvaluateInputAST(const char *Filename, delete *it; delete P; - delete S; - if (uint64_t queries = *theStatisticManager->getStatisticByName("SolverQueries")) { llvm::outs() << "--\n" |