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 /unittests | |
parent | e9d77be6c688836d68a2be5f3f0a02e63f392bb8 (diff) | |
download | klee-ac0fa15ab0679fe1b5067b07647b0701ae3bc347.tar.gz |
use unique_ptr all throughout the solver chain
Diffstat (limited to 'unittests')
-rw-r--r-- | unittests/Solver/SolverTest.cpp | 10 | ||||
-rw-r--r-- | unittests/Solver/Z3SolverTest.cpp | 8 |
2 files changed, 8 insertions, 10 deletions
diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index d5d207a0..2137602f 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -131,11 +131,11 @@ void testOpcode(Solver &solver, bool tryBool = true, bool tryZero = true, } TEST(SolverTest, Evaluation) { - Solver *solver = klee::createCoreSolver(CoreSolverToUse); + auto solver = klee::createCoreSolver(CoreSolverToUse); - solver = createCexCachingSolver(solver); - solver = createCachingSolver(solver); - solver = createIndependentSolver(solver); + solver = createCexCachingSolver(std::move(solver)); + solver = createCachingSolver(std::move(solver)); + solver = createIndependentSolver(std::move(solver)); testOpcode<SelectExpr>(*solver); testOpcode<ZExtExpr>(*solver); @@ -165,8 +165,6 @@ TEST(SolverTest, Evaluation) { testOpcode<SleExpr>(*solver); testOpcode<SgtExpr>(*solver); testOpcode<SgeExpr>(*solver); - - delete solver; } } diff --git a/unittests/Solver/Z3SolverTest.cpp b/unittests/Solver/Z3SolverTest.cpp index eab43d79..e81ff19e 100644 --- a/unittests/Solver/Z3SolverTest.cpp +++ b/unittests/Solver/Z3SolverTest.cpp @@ -19,6 +19,8 @@ #include "klee/Expr/Expr.h" #include "klee/Solver/Solver.h" +#include <memory> + using namespace klee; namespace { @@ -26,13 +28,11 @@ ArrayCache AC; } class Z3SolverTest : public ::testing::Test { protected: + std::unique_ptr<Solver> Z3Solver_; + Z3SolverTest() : Z3Solver_(createCoreSolver(CoreSolverType::Z3_SOLVER)) { Z3Solver_->setCoreSolverTimeout(time::Span("10s")); } - - virtual ~Z3SolverTest() { delete Z3Solver_; } - - Solver *Z3Solver_; }; TEST_F(Z3SolverTest, GetConstraintLog) { |