Add symex-backtrace

Author: smowton

src/goto-symex/goto_symex_state.cpp

@@ -856,3 +856,22 @@ void goto_symex_statet::switch_to_thread(unsigned t)
 
   guard=threads[t].guard;
 }
+
+void goto_symex_statet::print_backtrace(std::ostream &out)
+{
+  out << source.pc->function << " " << source.pc->location_number << "\n";
+
+  for(
+    auto stackit = threads[source.thread_nr].call_stack.rbegin(),
+      stackend = threads[source.thread_nr].call_stack.rend();
+    stackit != stackend;
+    ++stackit)
+  {
+    const auto &frame = *stackit;
+    if(frame.calling_location.is_set)
+    {
+      out << frame.calling_location.pc->function << " "
+          << frame.calling_location.pc->location_number << "\n";
+    }
+  }
+}

src/goto-symex/goto_symex_state.h

@@ -340,6 +340,8 @@ class goto_symex_statet final
   void pop_frame() { call_stack().pop_back(); }
   const framet &previous_frame() { return *(--(--call_stack().end())); }
 
+  void print_backtrace(std::ostream &);
+
   // threads
   unsigned atomic_section_id;
   typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;