Merge pull request #3527 from smowton/smowton/feature/symex-propagation-output

Symex propagation: add output function

Author: smowton

src/goto-symex/goto_symex_state.cpp

@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_exceptions.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
+#include <util/format.h>
+#include <util/format_expr.h>
 #include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
@@ -786,3 +788,14 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     }
   }
 }
+
+/// Print the constant propagation map in a human-friendly format.
+/// This is primarily for use from the debugger; please don't delete me just
+/// because there aren't any current callers.
+void goto_symex_statet::output_propagation_map(std::ostream &out)
+{
+  for(const auto &name_value : propagation)
+  {
+    out << name_value.first << " <- " << format(name_value.second) << "\n";
+  }
+}

src/goto-symex/goto_symex_state.h

@@ -67,6 +67,7 @@ class goto_symex_statet final
 
   // Map L1 names to (L2) constants
   std::map<irep_idt, exprt> propagation;
+  void output_propagation_map(std::ostream &);
 
   enum levelt { L0=0, L1=1, L2=2 };