fix: Get rid of the testcases spamming mode (#187)

Author: misonijnik

include/klee/Core/TerminationTypes.h

@@ -98,7 +98,6 @@ enum Reason {
   CovCheck,
   NoMoreStates,
   ReachedTarget,
-  UnreachedTarget,
   ErrorOnWhichShouldExit,
   Interrupt,
   MaxDepth,

lib/Core/Executor.cpp

@@ -246,9 +246,6 @@ cl::opt<HaltExecution::Reason> 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.",

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",

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;