Make symex_transition static

This does not use any field and is not overriden.

Author: romainbrenguier

src/goto-symex/goto_symex.h

@@ -238,19 +238,6 @@ class goto_symext
 
   const irep_idt guard_identifier;
 
-  // symex
-  virtual void symex_transition(
-    statet &,
-    goto_programt::const_targett to,
-    bool is_backwards_goto);
-
-  virtual void symex_transition(statet &state)
-  {
-    goto_programt::const_targett next=state.source.pc;
-    ++next;
-    symex_transition(state, next, false);
-  }
-
   virtual void symex_goto(statet &);
   virtual void symex_start_thread(statet &);
   virtual void symex_atomic_begin(statet &);
@@ -465,4 +452,11 @@ class goto_symext
   }
 };
 
+void symex_transition(goto_symext::statet &state);
+
+void symex_transition(
+  goto_symext::statet &,
+  goto_programt::const_targett to,
+  bool is_backwards_goto);
+
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/symex_main.cpp

@@ -22,8 +22,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/dirty.h>
 
-void goto_symext::symex_transition(
-  statet &state,
+void symex_transition(
+  goto_symext::statet &state,
   goto_programt::const_targett to,
   bool is_backwards_goto)
 {
@@ -34,7 +34,7 @@ void goto_symext::symex_transition(
     // 1. the transition from state.source.pc to "to" is not a backwards goto
     // or
     // 2. we are arriving from an outer loop
-    statet::framet &frame=state.top();
+    goto_symext::statet::framet &frame = state.top();
     const goto_programt::instructiont &instruction=*to;
     for(const auto &i_e : instruction.incoming_edges)
       if(i_e->is_goto() && i_e->is_backwards_goto() &&
@@ -46,6 +46,13 @@ void goto_symext::symex_transition(
   state.source.pc=to;
 }
 
+void symex_transition(goto_symext::statet &state)
+{
+  goto_programt::const_targett next = state.source.pc;
+  ++next;
+  symex_transition(state, next, false);
+}
+
 void goto_symext::vcc(
   const exprt &vcc_expr,
   const std::string &msg,