diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-23 21:48:12 +0100 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-03-23 21:48:12 +0100 |
commit | 20eb0485850073fafdac07a630cededf8b99c536 (patch) | |
tree | 445080c0a8bfef0fcb473a5ad4a4eab93f94baca /lib/Solver | |
parent | 082e9d7bab796eda37624c026d8d006608625b90 (diff) | |
download | klee-20eb0485850073fafdac07a630cededf8b99c536.tar.gz |
Refactoring of conditional flush into own function.
@delcypher: Thanks a lot Dan!
Diffstat (limited to 'lib/Solver')
-rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 24 | ||||
-rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 1 |
2 files changed, 15 insertions, 10 deletions
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 6084e2e1..f93bec3c 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -39,6 +39,16 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, QueryLoggingSolver::~QueryLoggingSolver() { delete solver; } +void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { + logBuffer.flush(); + if (writeToFile) { + os << logBuffer.str(); + os.flush(); + } + // prepare the buffer for reuse + BufferString = ""; +} + void QueryLoggingSolver::startQuery(const Query &query, const char *typeName, const Query *falseQuery, const std::vector<const Array *> *objects) { @@ -52,11 +62,7 @@ void QueryLoggingSolver::startQuery(const Query &query, const char *typeName, printQuery(query, falseQuery, objects); if (DumpPartialQueryiesEarly) { - logBuffer.flush(); - os << logBuffer.str(); - os.flush(); - // prepare the buffer for reuse - BufferString = ""; + flushBufferConditionally(true); } startTime = getWallTime(); } @@ -74,7 +80,7 @@ void QueryLoggingSolver::finishQuery(bool success) { } void QueryLoggingSolver::flushBuffer() { - logBuffer.flush(); + bool writeToFile = false; if ((0 == minQueryTimeToLog) || (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) { @@ -86,13 +92,11 @@ void QueryLoggingSolver::flushBuffer() { (solver->impl->getOperationStatusCode()))) { // we do additional check here to log only timeouts in case // user specified negative value for minQueryTimeToLog param - os << logBuffer.str(); - os.flush(); + writeToFile = true; } } - // prepare the buffer for reuse - BufferString = ""; + flushBufferConditionally(writeToFile); } bool QueryLoggingSolver::computeTruth(const Query &query, bool &isValid) { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 3068f2ab..bb266c67 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -55,6 +55,7 @@ protected: virtual void printQuery(const Query &query, const Query *falseQuery = 0, const std::vector<const Array *> *objects = 0) = 0; + void flushBufferConditionally(bool writeToFile); public: QueryLoggingSolver(Solver *_solver, std::string path, |