Merge pull request #3468 from smowton/smowton/feature/symex-backtrace

Add symex-backtrace

Author: smowton

src/goto-symex/goto_symex_state.cpp

@@ -774,3 +774,26 @@ void goto_symex_statet::get_l1_name(exprt &expr) const
     Forall_operands(it, expr)
       get_l1_name(*it);
 }
+
+/// Dumps the current state of symex, printing the function name and location
+/// number for each stack frame in the currently active thread.
+/// This is for use from the debugger or in debug code; please don't delete it
+/// just because it isn't called at present.
+/// \param out: stream to write to
+void goto_symex_statet::print_backtrace(std::ostream &out) const
+{
+  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

@@ -230,6 +230,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 &) const;
+
   // threads
   unsigned atomic_section_id;
   typedef std::pair<unsigned, std::list<guardt> > a_s_r_entryt;