Dumps Refined

Research-Tools-PAVT · Jan 5, 2021 · 470f1b0 · 470f1b0
1 parent 927bcac
commit 470f1b0
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 6 deletions.
diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h
@@ -43,8 +43,8 @@ class ConstraintSet {
   // REVISIT
   inline std::stringstream &printConstraintSetTY(std::stringstream &sso) {
     for (const ref<Expr> &conditions : constraints) {
-      sso << "\t\t";
-      sso << conditions << "\n";
+      sso << "->";
+      sso << conditions;
     }
     return sso;
   }

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
@@ -1148,7 +1148,6 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
     }
 
     processTree->attach(current.ptreeNode, falseState, trueState);
-    dumpPTree();
 
     if (pathWriter) {
       // Need to update the pathOS.id field of falseState, otherwise the same id
@@ -1179,21 +1178,21 @@ Executor::StatePair Executor::fork(ExecutionState &current, ref<Expr> condition,
 
     // COMMENT : Print the State level constraints.
     if (printSExpr) {
+      dumpPTree();
       std::stringstream sso("");
       *conditionsDump
           << "\tCurrent State Id : " << current.getID()
           << ",\n\tTrue KLEE Id : " << trueState->getID()
           << ",\n\tTrue Generate ID : " << stateExecutionStackID++
           << ",\n\ttrueQuery : \n\t\t[\n"
-          << (trueState->constraints.printConstraintSetTY(sso)).str()
-          << "\t\t],\n";
+          << (trueState->constraints.printConstraintSetTY(sso)).str() << "],\n";
       sso.str(std::string());
       *conditionsDump
           << "\tFalse KLEE Id : " << falseState->getID()
           << ",\n\tFalse Generate ID : " << stateExecutionStackID++
           << ",\n\tfalseQuery : \n\t\t[\n"
           << (falseState->constraints.printConstraintSetTY(sso)).str()
-          << "\t\t]\n}\n";
+          << "]\n}\n";
     }
     return StatePair(trueState, falseState);
   }