[fix] Fix tests

misonijnik · Nov 22, 2022 · d8a07ff · d8a07ff
1 parent 8ed9e49
commit d8a07ff
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 7 deletions.
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -554,8 +554,9 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
 
 
   time::Span maxTime{MaxTime};
-  klee_message("Initialization overhead: %ds", opts.InitializationOverhead);
-  maxTime -= time::seconds(opts.InitializationOverhead);
+  if (opts.InitializationOverhead != 0) {
+    maxTime -= time::seconds(opts.InitializationOverhead);
+  }
   if (maxTime)
     timers.add(std::make_unique<Timer>(maxTime, [&] {
       klee_message("HaltTimer invoked");
@@ -4070,12 +4071,14 @@ void Executor::run(std::vector<ExecutionState *> initialStates) {
       haltExecution = true;
   }
 
-  bool canReachNew1 = decreaseConfidenceFromStoppedStates(pausedStates);
-  bool canReachNew2 = decreaseConfidenceFromStoppedStates(states);
+  if (guidanceKind == GuidanceKind::ErrorGuidance) {
+    bool canReachNew1 = decreaseConfidenceFromStoppedStates(pausedStates);
+    bool canReachNew2 = decreaseConfidenceFromStoppedStates(states);
 
-  for (auto &startBlockAndWhiteList : targets) {
-    targetedExecutionManager.reportFalsePositives(startBlockAndWhiteList.second,
-                                                  canReachNew1 || canReachNew2);
+    for (auto &startBlockAndWhiteList : targets) {
+      targetedExecutionManager.reportFalsePositives(startBlockAndWhiteList.second,
+                                                    canReachNew1 || canReachNew2);
+    }
   }
 
   delete searcher;

diff --git a/lib/Runner/run_klee.cpp b/lib/Runner/run_klee.cpp
@@ -2095,6 +2095,10 @@ int run_klee(int argc, char **argv, char **envp) {
     Interpreter::InterpreterOptions IOpts;
     IOpts.MakeConcreteSymbolic = MakeConcreteSymbolic;
     IOpts.InitializationOverhead = (lastTime - startTime).toSeconds();
+    klee_message("Initialization overhead: %ds", IOpts.InitializationOverhead);
+    if (ExecutionMode != Interpreter::GuidanceKind::ErrorGuidance) {
+      IOpts.InitializationOverhead = 0;
+    }
     std::unique_ptr<KleeHandler> handler =
         std::make_unique<KleeHandler>(pArgc, pArgv);
     std::unique_ptr<Interpreter> interpreter(