diff options
| -rw-r--r-- | include/klee/Core/Interpreter.h | 3 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 5 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 26 |
3 files changed, 22 insertions, 12 deletions
diff --git a/include/klee/Core/Interpreter.h b/include/klee/Core/Interpreter.h index 541881a9..f14e3d88 100644 --- a/include/klee/Core/Interpreter.h +++ b/include/klee/Core/Interpreter.h @@ -40,7 +40,8 @@ public: virtual std::string getOutputFilename(const std::string &filename) = 0; virtual std::unique_ptr<llvm::raw_fd_ostream> openOutputFile(const std::string &filename) = 0; - virtual void incPathsExplored() = 0; + virtual void incPathsCompleted() = 0; + virtual void incPathsExplored(std::uint32_t num = 1) = 0; virtual void processTestCase(const ExecutionState &state, const char *err, diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2f806aad..fb83c883 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3436,8 +3436,10 @@ bool Executor::checkMemoryUsage() { } void Executor::doDumpStates() { - if (!DumpStatesOnHalt || states.empty()) + if (!DumpStatesOnHalt || states.empty()) { + interpreterHandler->incPathsExplored(states.size()); return; + } klee_message("halting execution, dumping remaining states"); for (const auto &state : states) @@ -3638,6 +3640,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) { if (!OnlyOutputStatesCoveringNew || state.coveredNew || (AlwaysOutputSeeds && seedMap.count(&state))) interpreterHandler->processTestCase(state, 0, 0); + interpreterHandler->incPathsCompleted(); terminateState(state); } diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 8d9a7c16..f340e743 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -308,7 +308,8 @@ private: unsigned m_numTotalTests; // Number of tests received from the interpreter unsigned m_numGeneratedTests; // Number of tests successfully generated - unsigned m_pathsExplored; // number of paths explored so far + unsigned m_pathsCompleted; // number of completed paths + unsigned m_pathsExplored; // number of partially explored and completed paths // used for writing .ktest files int m_argc; @@ -321,8 +322,11 @@ public: llvm::raw_ostream &getInfoStream() const { return *m_infoFile; } /// Returns the number of test cases successfully generated so far unsigned getNumTestCases() { return m_numGeneratedTests; } + unsigned getNumPathsCompleted() { return m_pathsCompleted; } unsigned getNumPathsExplored() { return m_pathsExplored; } - void incPathsExplored() { m_pathsExplored++; } + void incPathsCompleted() { ++m_pathsCompleted; } + void incPathsExplored(std::uint32_t num = 1) { + m_pathsExplored += num; } void setInterpreter(Interpreter *i); @@ -348,7 +352,7 @@ public: KleeHandler::KleeHandler(int argc, char **argv) : m_interpreter(0), m_pathWriter(0), m_symPathWriter(0), m_outputDirectory(), m_numTotalTests(0), m_numGeneratedTests(0), - m_pathsExplored(0), m_argc(argc), m_argv(argv) { + m_pathsCompleted(0), m_pathsExplored(0), m_argc(argc), m_argv(argv) { // create output directory (OutputDir or "klee-out-<i>") bool dir_given = OutputDir != ""; @@ -1583,13 +1587,15 @@ int main(int argc, char **argv, char **envp) { << "KLEE: done: query cex = " << queryCounterexamples << "\n"; std::stringstream stats; - stats << "\n"; - stats << "KLEE: done: total instructions = " - << instructions << "\n"; - stats << "KLEE: done: completed paths = " - << handler->getNumPathsExplored() << "\n"; - stats << "KLEE: done: generated tests = " - << handler->getNumTestCases() << "\n"; + stats << '\n' + << "KLEE: done: total instructions = " << instructions << '\n' + << "KLEE: done: completed paths = " << handler->getNumPathsCompleted() + << '\n' + << "KLEE: done: partially completed paths = " + << handler->getNumPathsExplored() - handler->getNumPathsCompleted() + << '\n' + << "KLEE: done: generated tests = " << handler->getNumTestCases() + << '\n'; bool useColors = llvm::errs().is_displayed(); if (useColors) |