Make recording of branches possible

symex_bmct may now re-implement merge_goto to observe each merge, just
like loop unwinding is reported.

Author: tautschnig

src/goto-symex/goto_symex.h

@@ -175,6 +175,10 @@ class goto_symext
   // gotos
   void merge_gotos(statet &state);
 
+  virtual void merge_goto(
+    const statet::goto_statet &goto_state,
+    statet &state);
+
   void merge_value_sets(
     const statet::goto_statet &goto_state,
     statet &dest);

src/goto-symex/goto_symex_state.h

@@ -189,6 +189,7 @@ class goto_symex_statet
     level2t::current_namest level2_current_names;
     value_sett value_set;
     guardt guard;
+    symex_targett::sourcet source;
     propagationt propagation;
     unsigned atomic_section_id;
 
@@ -197,6 +198,7 @@ class goto_symex_statet
       level2_current_names(s.level2.current_names),
       value_set(s.value_set),
       guard(s.guard),
+      source(s.source),
       propagation(s.propagation),
       atomic_section_id(s.atomic_section_id)
     {

src/goto-symex/symex_goto.cpp

@@ -121,15 +121,15 @@ void goto_symext::symex_goto(statet &state)
     state_pc=goto_target;
   }
 
-  state.source.pc=state_pc;
-
   // put into state-queue
   statet::goto_state_listt &goto_state_list=
     state.top().goto_state_map[new_state_pc];
 
   goto_state_list.push_back(statet::goto_statet(state));
   statet::goto_statet &new_state=goto_state_list.back();
 
+  state.source.pc=state_pc;
+
   // adjust guards
   if(new_guard.is_true())
   {
@@ -244,27 +244,42 @@ void goto_symext::merge_gotos(statet &state)
       list_it=state_list.rbegin();
       list_it!=state_list.rend();
       list_it++)
-  {
-    statet::goto_statet &goto_state=*list_it;
+    merge_goto(*list_it, state);
 
-    // check atomic section
-    if(state.atomic_section_id!=goto_state.atomic_section_id)
-      throw "atomic sections differ across branches";
+  // clean up to save some memory
+  frame.goto_state_map.erase(state_map_it);
+}
 
-    // do SSA phi functions
-    phi_function(goto_state, state);
+/*******************************************************************\
 
-    merge_value_sets(goto_state, state);
+Function: goto_symext::merge_goto
 
-    // adjust guard
-    state.guard|=goto_state.guard;
+  Inputs:
 
-    // adjust depth
-    state.depth=std::min(state.depth, goto_state.depth);
-  }
+ Outputs:
 
-  // clean up to save some memory
-  frame.goto_state_map.erase(state_map_it);
+ Purpose:
+
+\*******************************************************************/
+
+void goto_symext::merge_goto(
+  const statet::goto_statet &goto_state,
+  statet &state)
+{
+  // check atomic section
+  if(state.atomic_section_id!=goto_state.atomic_section_id)
+    throw "atomic sections differ across branches";
+
+  // do SSA phi functions
+  phi_function(goto_state, state);
+
+  merge_value_sets(goto_state, state);
+
+  // adjust guard
+  state.guard|=goto_state.guard;
+
+  // adjust depth
+  state.depth=std::min(state.depth, goto_state.depth);
 }
 
 /*******************************************************************\