From 9abe9572e68748002d8bbb789587e2a036ff760d Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 16:15:56 +0100 Subject: Renaming solver-related command-line options in order to decouple them from STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well. --- lib/Core/Executor.cpp | 36 +++++++++++++----------------------- lib/Core/Executor.h | 5 +++-- 2 files changed, 16 insertions(+), 25 deletions(-) (limited to 'lib/Core') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index d0ad811d..309c5fd5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -189,7 +189,7 @@ namespace { cl::opt MaxInstructionTime("max-instruction-time", - cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-stp"), + cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-solver"), cl::init(0)); cl::opt @@ -221,16 +221,6 @@ namespace { MaxMemoryInhibit("max-memory-inhibit", cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=on)"), cl::init(true)); - - cl::opt - UseForkedSTP("use-forked-stp", - cl::desc("Run STP in a forked process (default=off)")); - - cl::opt - STPOptimizeDivides("stp-optimize-divides", - cl::desc("Optimize constant divides into add/shift/multiplies before passing to STP (default=on)"), - cl::init(true)); - } @@ -258,11 +248,11 @@ Executor::Executor(const InterpreterOptions &opts, inhibitForking(false), haltExecution(false), ivcEnabled(false), - stpTimeout(MaxSTPTime != 0 && MaxInstructionTime != 0 - ? std::min(MaxSTPTime,MaxInstructionTime) - : std::max(MaxSTPTime,MaxInstructionTime)) { - if (stpTimeout) UseForkedSTP = true; - STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides); + coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 + ? std::min(MaxCoreSolverTime,MaxInstructionTime) + : std::max(MaxCoreSolverTime,MaxInstructionTime)) { + if (coreSolverTimeout) UseForkedCoreSolver = true; + STPSolver *stpSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); Solver *solver = constructSolverChain(stpSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), @@ -666,7 +656,7 @@ Executor::fork(ExecutionState ¤t, ref condition, bool isInternal) { } } - double timeout = stpTimeout; + double timeout = coreSolverTimeout; if (isSeeding) timeout *= it->second.size(); solver->setTimeout(timeout); @@ -982,7 +972,7 @@ ref Executor::toUnique(const ExecutionState &state, ref value; bool isTrue = false; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); if (solver->getValue(state, e, value) && solver->mustBeTrue(state, EqExpr::create(e, value), isTrue) && isTrue) @@ -2979,7 +2969,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, // fast path: single in-bounds resolution ObjectPair op; bool success; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); if (!state.addressSpace.resolveOne(state, solver, address, op, success)) { address = toConstant(state, address, "resolveOne failure"); success = state.addressSpace.resolveOne(cast(address), op); @@ -2996,7 +2986,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, ref offset = mo->getOffsetExpr(address); bool inBounds; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); bool success = solver->mustBeTrue(state, mo->getBoundsCheckOffset(offset, bytes), inBounds); @@ -3035,9 +3025,9 @@ void Executor::executeMemoryOperation(ExecutionState &state, // resolution with out of bounds) ResolutionList rl; - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); bool incomplete = state.addressSpace.resolve(state, solver, address, rl, - 0, stpTimeout); + 0, coreSolverTimeout); solver->setTimeout(0); // XXX there is some query wasteage here. who cares? @@ -3328,7 +3318,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, std::pair > > &res) { - solver->setTimeout(stpTimeout); + solver->setTimeout(coreSolverTimeout); ExecutionState tmp(state); if (!NoPreferCex) { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index c434c34c..a9d6b791 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -173,8 +173,9 @@ private: /// false, it is buggy (it needs to validate its writes). bool ivcEnabled; - /// The maximum time to allow for a single stp query. - double stpTimeout; + /// The maximum time to allow for a single core solver query. + /// (e.g. for a single STP query) + double coreSolverTimeout; llvm::Function* getTargetFunction(llvm::Value *calledVal, ExecutionState &state); -- cgit 1.4.1 From ca83defeab023dbfbbd21d8a497a42af9abdf7fd Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 17:59:08 +0100 Subject: Methods getConstraintLog() and setTimeout() made virtual and moved from STPSolver to base Solver and SolverImpl classes, and consequently redefined in derived classes to call the corresponding methods down the solver chain. Method setTimeout() renamed to setCoreSolverTimeout(). --- include/klee/IncompleteSolver.h | 2 ++ include/klee/Solver.h | 13 +++++++------ include/klee/SolverImpl.h | 9 ++++++++- lib/Core/TimingSolver.h | 6 +++++- lib/Solver/CachingSolver.cpp | 10 ++++++++++ lib/Solver/CexCachingSolver.cpp | 10 ++++++++++ lib/Solver/IncompleteSolver.cpp | 9 +++++++++ lib/Solver/IndependentSolver.cpp | 10 ++++++++++ lib/Solver/QueryLoggingSolver.cpp | 7 +++++++ lib/Solver/QueryLoggingSolver.h | 3 ++- lib/Solver/Solver.cpp | 28 +++++++++++++++++++++++----- tools/kleaver/main.cpp | 2 +- 12 files changed, 94 insertions(+), 15 deletions(-) (limited to 'lib/Core') diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h index 9a122c74..f589e3b3 100644 --- a/include/klee/IncompleteSolver.h +++ b/include/klee/IncompleteSolver.h @@ -102,6 +102,8 @@ public: std::vector< std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout); }; } diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 1af30870..8fe33c7c 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -194,6 +194,9 @@ namespace klee { // // FIXME: This should go into a helper class, and should handle failure. virtual std::pair< ref, ref > getRange(const Query&); + + virtual char *getConstraintLog(const Query& query); + virtual void setCoreSolverTimeout(double timeout); }; /// STPSolver - A complete solver based on STP. @@ -207,15 +210,13 @@ namespace klee { /// be optimized into add/shift/multiply operations. STPSolver(bool useForkedSTP, bool optimizeDivides = true); - - /// getConstraintLog - Return the constraint log for the given state in CVC /// format. - char *getConstraintLog(const Query&); - - /// setTimeout - Set constraint solver timeout delay to the given value; 0 + virtual char *getConstraintLog(const Query&); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0 /// is off. - void setTimeout(double timeout); + virtual void setCoreSolverTimeout(double timeout); }; /* *** */ diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h index e200205b..c17082a8 100644 --- a/include/klee/SolverImpl.h +++ b/include/klee/SolverImpl.h @@ -93,10 +93,17 @@ namespace klee { /// getOperationStatusCode - get the status of the last solver operation virtual SolverRunStatus getOperationStatusCode() = 0; - + /// getOperationStatusString - get string representation of the operation /// status code static const char* getOperationStatusString(SolverRunStatus statusCode); + + virtual char *getConstraintLog(const Query& query) { + // dummy + return(NULL); + } + + virtual void setCoreSolverTimeout(double timeout) {}; }; } diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index b13879df..2684e071 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -42,7 +42,11 @@ namespace klee { } void setTimeout(double t) { - stpSolver->setTimeout(t); + stpSolver->setCoreSolverTimeout(t); + } + + char *getConstraintLog(const Query& query) { + return solver->getConstraintLog(query); } bool evaluate(const ExecutionState&, ref, Solver::Validity &result); diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 5911bbf3..674d4627 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -85,6 +85,8 @@ public: hasSolution); } SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout); }; /** @returns the canonical version of the given query. The reference @@ -244,6 +246,14 @@ SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } +char *CachingSolver::getConstraintLog(const Query& query) { + return solver->impl->getConstraintLog(query); +} + +void CachingSolver::setCoreSolverTimeout(double timeout) { + solver->impl->setCoreSolverTimeout(timeout); +} + /// Solver *klee::createCachingSolver(Solver *_solver) { diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index b38df672..df7fffc5 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -83,6 +83,8 @@ public: std::vector< std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query& query); + void setCoreSolverTimeout(double timeout); }; /// @@ -350,6 +352,14 @@ SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } +char *CexCachingSolver::getConstraintLog(const Query& query) { + return solver->impl->getConstraintLog(query); +} + +void CexCachingSolver::setCoreSolverTimeout(double timeout) { + solver->impl->setCoreSolverTimeout(timeout); +} + /// Solver *klee::createCexCachingSolver(Solver *_solver) { diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index 7bc8058d..dc2c9fd4 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -138,3 +138,12 @@ StagedSolverImpl::computeInitialValues(const Query& query, SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() { return secondary->impl->getOperationStatusCode(); } + +char *StagedSolverImpl::getConstraintLog(const Query& query) { + return secondary->impl->getConstraintLog(query); +} + +void StagedSolverImpl::setCoreSolverTimeout(double timeout) { + secondary->impl->setCoreSolverTimeout(timeout); +} + diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index b3ef1e57..d9fc77dc 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -285,6 +285,8 @@ public: hasSolution); } SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout); }; bool IndependentSolver::computeValidity(const Query& query, @@ -318,6 +320,14 @@ SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } +char *IndependentSolver::getConstraintLog(const Query& query) { + return solver->impl->getConstraintLog(query); +} + +void IndependentSolver::setCoreSolverTimeout(double timeout) { + solver->impl->setCoreSolverTimeout(timeout); +} + Solver *klee::createIndependentSolver(Solver *s) { return new Solver(new IndependentSolver(s)); } diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 245ad3bf..e7187fc3 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -183,4 +183,11 @@ SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } +char *QueryLoggingSolver::getConstraintLog(const Query& query) { + return solver->impl->getConstraintLog(query); +} + +void QueryLoggingSolver::setCoreSolverTimeout(double timeout) { + solver->impl->setCoreSolverTimeout(timeout); +} diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 527d075b..2c7d80e8 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -70,7 +70,8 @@ public: std::vector< std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); - + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout); }; #endif /* KLEE_QUERYLOGGINGSOLVER_H */ diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index b3d1613d..3414cda2 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -101,6 +101,14 @@ Solver::~Solver() { delete impl; } +char *Solver::getConstraintLog(const Query& query) { + return impl->getConstraintLog(query); +} + +void Solver::setCoreSolverTimeout(double timeout) { + impl->setCoreSolverTimeout(timeout); +} + bool Solver::evaluate(const Query& query, Validity &result) { assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!"); @@ -307,6 +315,8 @@ public: std::vector< std::vector > &values, bool &hasSolution); SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query&); + void setCoreSolverTimeout(double timeout); }; bool ValidatingSolver::computeTruth(const Query& query, @@ -408,6 +418,14 @@ SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } +char *ValidatingSolver::getConstraintLog(const Query& query) { + return solver->impl->getConstraintLog(query); +} + +void ValidatingSolver::setCoreSolverTimeout(double timeout) { + solver->impl->setCoreSolverTimeout(timeout); +} + Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) { return new Solver(new ValidatingSolver(s, oracle)); } @@ -466,9 +484,9 @@ private: public: STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true); ~STPSolverImpl(); - + char *getConstraintLog(const Query&); - void setTimeout(double _timeout) { timeout = _timeout; } + void setCoreSolverTimeout(double _timeout) { timeout = _timeout; } bool computeTruth(const Query&, bool &isValid); bool computeValue(const Query&, ref &result); @@ -532,11 +550,11 @@ STPSolver::STPSolver(bool useForkedSTP, bool optimizeDivides) } char *STPSolver::getConstraintLog(const Query &query) { - return static_cast(impl)->getConstraintLog(query); + return impl->getConstraintLog(query); } -void STPSolver::setTimeout(double timeout) { - static_cast(impl)->setTimeout(timeout); +void STPSolver::setCoreSolverTimeout(double timeout) { + impl->setCoreSolverTimeout(timeout); } /***/ diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 47c4f07f..6c2a29e5 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -216,7 +216,7 @@ static bool EvaluateInputAST(const char *Filename, if (!UseDummySolver) { STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver); if (0 != MaxCoreSolverTime) { - stpSolver->setTimeout(MaxCoreSolverTime); + stpSolver->setCoreSolverTimeout(MaxCoreSolverTime); } STP = S = stpSolver; } -- cgit 1.4.1 From 4a426569a38760b9ecf34af46b4eeca76e21e8e6 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 18:25:16 +0100 Subject: TimingSolver and constructSolverChain() no longer coupled with pointers to STPSolver objects. Timeout is now set by the solver at the top of the solver chain rather than by STPSolver. --- include/klee/Common.h | 2 +- lib/Basic/ConstructSolverChain.cpp | 14 +++++++------- lib/Core/Executor.cpp | 9 +++++---- lib/Core/TimingSolver.h | 11 ++++------- tools/kleaver/main.cpp | 22 ++++++++-------------- 5 files changed, 25 insertions(+), 33 deletions(-) (limited to 'lib/Core') diff --git a/include/klee/Common.h b/include/klee/Common.h index 1418f1b6..7149708a 100644 --- a/include/klee/Common.h +++ b/include/klee/Common.h @@ -22,7 +22,7 @@ namespace klee { const char ALL_QUERIES_PC_FILE_NAME[]="all-queries.pc"; const char SOLVER_QUERIES_PC_FILE_NAME[]="solver-queries.pc"; - Solver *constructSolverChain(STPSolver *stpSolver, + Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, std::string queryPCLogPath, diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index 70c728df..c0d0ef61 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -16,13 +16,13 @@ namespace klee { - Solver *constructSolverChain(STPSolver *stpSolver, - std::string querySMT2LogPath, - std::string baseSolverQuerySMT2LogPath, - std::string queryPCLogPath, - std::string baseSolverQueryPCLogPath) + Solver *constructSolverChain(Solver *coreSolver, + std::string querySMT2LogPath, + std::string baseSolverQuerySMT2LogPath, + std::string queryPCLogPath, + std::string baseSolverQueryPCLogPath) { - Solver *solver = stpSolver; + Solver *solver = coreSolver; if (optionIsSet(queryLoggingOptions, SOLVER_PC)) { @@ -55,7 +55,7 @@ namespace klee solver = createIndependentSolver(solver); if (DebugValidateSolver) - solver = createValidatingSolver(solver, stpSolver); + solver = createValidatingSolver(solver, coreSolver); if (optionIsSet(queryLoggingOptions, ALL_PC)) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 309c5fd5..b57b1956 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -251,16 +251,17 @@ Executor::Executor(const InterpreterOptions &opts, coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 ? std::min(MaxCoreSolverTime,MaxInstructionTime) : std::max(MaxCoreSolverTime,MaxInstructionTime)) { + if (coreSolverTimeout) UseForkedCoreSolver = true; - STPSolver *stpSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); + Solver *coreSolver = new STPSolver(UseForkedCoreSolver, CoreSolverOptimizeDivides); Solver *solver = - constructSolverChain(stpSolver, + constructSolverChain(coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); - this->solver = new TimingSolver(solver, stpSolver); + this->solver = new TimingSolver(solver); memory = new MemoryManager(); } @@ -3280,7 +3281,7 @@ void Executor::getConstraintLog(const ExecutionState &state, case STP: { Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->stpSolver->getConstraintLog(query); + char *log = solver->getConstraintLog(query); res = std::string(log); free(log); } diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 2684e071..c98dd881 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -17,15 +17,13 @@ namespace klee { class ExecutionState; - class Solver; - class STPSolver; + class Solver; /// TimingSolver - A simple class which wraps a solver and handles /// tracking the statistics that we care about. class TimingSolver { public: Solver *solver; - STPSolver *stpSolver; bool simplifyExprs; public: @@ -34,15 +32,14 @@ namespace klee { /// \param _simplifyExprs - Whether expressions should be /// simplified (via the constraint manager interface) prior to /// querying. - TimingSolver(Solver *_solver, STPSolver *_stpSolver, - bool _simplifyExprs = true) - : solver(_solver), stpSolver(_stpSolver), simplifyExprs(_simplifyExprs) {} + TimingSolver(Solver *_solver, bool _simplifyExprs = true) + : solver(_solver), simplifyExprs(_simplifyExprs) {} ~TimingSolver() { delete solver; } void setTimeout(double t) { - stpSolver->setCoreSolverTimeout(t); + solver->setCoreSolverTimeout(t); } char *getConstraintLog(const Query& query) { diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 6c2a29e5..accc48e4 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -211,25 +211,19 @@ static bool EvaluateInputAST(const char *Filename, return false; // FIXME: Support choice of solver. - Solver *S = 0; - Solver *STP = 0; + Solver *coreSolver = UseDummySolver ? createDummySolver() : new STPSolver(UseForkedCoreSolver); + if (!UseDummySolver) { - STPSolver* stpSolver = new STPSolver(UseForkedCoreSolver); if (0 != MaxCoreSolverTime) { - stpSolver->setCoreSolverTimeout(MaxCoreSolverTime); + coreSolver->setCoreSolverTimeout(MaxCoreSolverTime); } - STP = S = stpSolver; - } - else { - STP = S = createDummySolver(); } - S= constructSolverChain((STPSolver*) STP, - getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), - getQueryLogPath(ALL_QUERIES_PC_FILE_NAME), - getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME)); - + Solver *S = constructSolverChain(coreSolver, + getQueryLogPath(ALL_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_SMT2_FILE_NAME), + getQueryLogPath(ALL_QUERIES_PC_FILE_NAME), + getQueryLogPath(SOLVER_QUERIES_PC_FILE_NAME)); unsigned Index = 0; for (std::vector::iterator it = Decls.begin(), -- cgit 1.4.1 From 6eae8c62e620c86ef5c95839e899d39e003c13eb Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Tue, 6 Aug 2013 19:08:41 +0100 Subject: ObjectState::concreteStore initialised. --- lib/Core/Memory.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'lib/Core') diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 7b3655f8..08c95d48 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -110,6 +110,7 @@ ObjectState::ObjectState(const MemoryObject *mo) const Array *array = new Array("tmp_arr" + llvm::utostr(++id), size); updates = UpdateList(array, 0); } + memset(concreteStore, 0, size); } @@ -126,6 +127,7 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array) readOnly(false) { mo->refCount++; makeSymbolic(); + memset(concreteStore, 0, size); } ObjectState::ObjectState(const ObjectState &os) -- cgit 1.4.1