Add symex-backtrace

Author: smowton

src/goto-symex/goto_symex_state.cpp

@@ -774,3 +774,21 @@ void goto_symex_statet::get_l1_name(exprt &expr) const
     Forall_operands(it, expr)
       get_l1_name(*it);
 }
+
+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

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