Added ExecutionState::dumpStack function for inspecting the status of the stack

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106798 91177308-0d34-0410-b5e6-96231b3b80d8

3 files changed, 35 insertions, 29 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index 09999110..c119edd3 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -134,6 +134,7 @@ public:
   }
 
   bool merge(const ExecutionState &b);
+  void dumpStack(std::ostream &out) const;
 };
 
 }
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 57f9bca9..4362b78f 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -22,6 +22,7 @@
 #include "llvm/Support/CommandLine.h"
 
 #include <iostream>
+#include <iomanip>
 #include <cassert>
 #include <map>
 #include <set>
@@ -302,3 +303,35 @@ bool ExecutionState::merge(const ExecutionState &b) {
 
   return true;
 }
+
+void ExecutionState::dumpStack(std::ostream &out) const {
+  unsigned idx = 0;
+  const KInstruction *target = prevPC;
+  for (ExecutionState::stack_ty::const_reverse_iterator
+         it = stack.rbegin(), ie = stack.rend();
+       it != ie; ++it) {
+    const StackFrame &sf = *it;
+    Function *f = sf.kf->function;
+    const InstructionInfo &ii = *target->info;
+    out << "\t#" << idx++ 
+        << " " << std::setw(8) << std::setfill('0') << ii.assemblyLine
+        << " in " << f->getNameStr() << " (";
+    // Yawn, we could go up and print varargs if we wanted to.
+    unsigned index = 0;
+    for (Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
+         ai != ae; ++ai) {
+      if (ai!=f->arg_begin()) out << ", ";
+
+      out << ai->getNameStr();
+      // XXX should go through function
+      ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; 
+      if (isa<ConstantExpr>(value))
+        out << "=" << value;
+    }
+    out << ")";
+    if (ii.file != "")
+      out << " at " << ii.file << ":" << ii.line;
+    out << "\n";
+    target = sf.caller;
+  }
+}
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index dc74b6cd..1da91f2a 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2554,35 +2554,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
       msg << "Line: " << ii.line << "\n";
     }
     msg << "Stack: \n";
-    unsigned idx = 0;
-    const KInstruction *target = state.prevPC;
-    for (ExecutionState::stack_ty::reverse_iterator
-           it = state.stack.rbegin(), ie = state.stack.rend();
-         it != ie; ++it) {
-      StackFrame &sf = *it;
-      Function *f = sf.kf->function;
-      const InstructionInfo &ii = *target->info;
-      msg << "\t#" << idx++ 
-          << " " << std::setw(8) << std::setfill('0') << ii.assemblyLine
-          << " in " << f->getNameStr() << " (";
-      // Yawn, we could go up and print varargs if we wanted to.
-      unsigned index = 0;
-      for (Function::arg_iterator ai = f->arg_begin(), ae = f->arg_end();
-           ai != ae; ++ai) {
-        if (ai!=f->arg_begin()) msg << ", ";
-
-        msg << ai->getNameStr();
-        // XXX should go through function
-        ref<Expr> value = sf.locals[sf.kf->getArgRegister(index++)].value; 
-        if (isa<ConstantExpr>(value))
-          msg << "=" << value;
-      }
-      msg << ")";
-      if (ii.file != "")
-        msg << " at " << ii.file << ":" << ii.line;
-      msg << "\n";
-      target = sf.caller;
-    }
+    state.dumpStack(msg);
 
     std::string info_str = info.str();
     if (info_str != "")