diff --git a/include/klee/Core/TerminationTypes.h b/include/klee/Core/TerminationTypes.h index 9dc67be69a..6563b9736c 100644 --- a/include/klee/Core/TerminationTypes.h +++ b/include/klee/Core/TerminationTypes.h @@ -98,7 +98,6 @@ enum Reason { CovCheck, NoMoreStates, ReachedTarget, - UnreachedTarget, ErrorOnWhichShouldExit, Interrupt, MaxDepth, diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c6a395731c..20652188c2 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -246,9 +246,6 @@ cl::opt DumpStatesOnHalt( cl::values( clEnumValN(HaltExecution::Reason::NotHalt, "none", "Do not dump test cases for all active states on exit."), - clEnumValN(HaltExecution::Reason::UnreachedTarget, "unreached", - "Dump test cases for all active states on exit if error not " - "reached."), clEnumValN(HaltExecution::Reason::Unspecified, "all", "Dump test cases for all active states on exit (default)")), cl::cat(TestGenCat)); @@ -4451,19 +4448,11 @@ void Executor::decreaseConfidenceFromStoppedStates( void Executor::doDumpStates() { auto &states = objectManager->getStates(); - if (DumpStatesOnHalt == HaltExecution::Reason::NotHalt || - (DumpStatesOnHalt == HaltExecution::Reason::UnreachedTarget && - haltExecution == HaltExecution::Reason::ReachedTarget) || - states.empty()) { + if (DumpStatesOnHalt == HaltExecution::Reason::NotHalt || states.empty()) { interpreterHandler->incPathsExplored(states.size()); return; } - if (FunctionCallReproduce != "" && - haltExecution != HaltExecution::Reason::ReachedTarget) { - haltExecution = HaltExecution::UnreachedTarget; - } - klee_message("halting execution, dumping remaining states"); for (const auto &state : objectManager->getStates()) { terminateStateEarly(*state, "Execution halting.", diff --git a/scripts/kleef b/scripts/kleef index a5a99fcc23..b1f2abb55a 100755 --- a/scripts/kleef +++ b/scripts/kleef @@ -81,7 +81,7 @@ def klee_options( "--function-call-reproduce=reach_error", # "--max-cycles=0", # "--tc-type=bug", - "--dump-states-on-halt=unreached", # Explicitly do not dump states + "--dump-states-on-halt=none", # Explicitly do not dump states "--exit-on-error-type=Assert", # Only generate test cases of type assert # "--dump-test-case-type=Assert", # Only dump test cases of type assert "--search=dfs", diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 48d1f85c06..29651bbf91 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -680,10 +680,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, unsigned id = ++m_numTotalTests; if (!WriteNone && (FunctionCallReproduce == "" || strcmp(suffix, "assert.err") == 0 || - strcmp(suffix, "reachable.err") == 0 || - (DumpStatesOnHalt == HaltExecution::Reason::UnreachedTarget && - m_interpreter->getHaltExecution() == - HaltExecution::Reason::UnreachedTarget))) { + strcmp(suffix, "reachable.err") == 0)) { KTest ktest; ktest.numArgs = m_argc; ktest.args = m_argv;