aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorDaniel Schemmel <daniel@schemmel.net>2023-03-24 15:05:43 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2023-04-21 13:07:31 +0100
commitac0fa15ab0679fe1b5067b07647b0701ae3bc347 (patch)
treef2294eb5f0795ee9ce0f92d527242b7b7a507e79 /tools
parente9d77be6c688836d68a2be5f3f0a02e63f392bb8 (diff)
downloadklee-ac0fa15ab0679fe1b5067b07647b0701ae3bc347.tar.gz
use unique_ptr all throughout the solver chain
Diffstat (limited to 'tools')
-rw-r--r--tools/kleaver/main.cpp19
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"