Merge pull request #3446 from romainbrenguier/refactor/switch-to-thread

Make switch_to_thread static

Author: tautschnig

src/goto-symex/goto_symex_state.cpp

@@ -777,19 +777,3 @@ void goto_symex_statet::get_l1_name(exprt &expr) const
     Forall_operands(it, expr)
       get_l1_name(*it);
 }
-
-void goto_symex_statet::switch_to_thread(unsigned t)
-{
-  PRECONDITION(source.thread_nr < threads.size());
-  PRECONDITION(t < threads.size());
-
-  // save PC
-  threads[source.thread_nr].pc=source.pc;
-  threads[source.thread_nr].atomic_section_id=atomic_section_id;
-
-  // get new PC
-  source.thread_nr=t;
-  source.pc=threads[t].pc;
-
-  guard=threads[t].guard;
-}

src/goto-symex/goto_symex_state.h

@@ -283,7 +283,6 @@ class goto_symex_statet final
   void populate_dirty_for_function(
     const irep_idt &id, const goto_functiont &);
 
-  void switch_to_thread(unsigned t);
   bool record_events;
   incremental_dirtyt dirty;
 

src/goto-symex/symex_main.cpp

@@ -154,6 +154,24 @@ void goto_symext::initialize_entry_point(
   symex_transition(state, state.source.pc, false);
 }
 
+static void
+switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
+{
+  PRECONDITION(state.source.thread_nr < state.threads.size());
+  PRECONDITION(thread_nb < state.threads.size());
+
+  // save PC
+  state.threads[state.source.thread_nr].pc = state.source.pc;
+  state.threads[state.source.thread_nr].atomic_section_id =
+    state.atomic_section_id;
+
+  // get new PC
+  state.source.thread_nr = thread_nb;
+  state.source.pc = state.threads[thread_nb].pc;
+
+  state.guard = state.threads[thread_nb].guard;
+}
+
 void goto_symext::symex_threaded_step(
   statet &state, const get_goto_functiont &get_goto_function)
 {
@@ -173,7 +191,7 @@ void goto_symext::symex_threaded_step(
 #if 0
     std::cout << "********* Now executing thread " << t << '\n';
 #endif
-    state.switch_to_thread(t);
+    switch_to_thread(state, t);
     symex_transition(state, state.source.pc, false);
   }
 }