Merge pull request #6120 from tautschnig/concurrency-function-name

Concurrency: ensure function name is correct when starting threads

Author: tautschnig

src/goto-symex/goto_symex_state.h

@@ -182,6 +182,7 @@ class goto_symex_statet final : public goto_statet
   struct threadt
   {
     goto_programt::const_targett pc;
+    irep_idt function_id;
     guardt guard;
     call_stackt call_stack;
     std::map<irep_idt, unsigned> function_frame;

src/goto-symex/symex_main.cpp

@@ -290,6 +290,7 @@ switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
   // get new PC
   state.source.thread_nr = thread_nb;
   state.source.pc = state.threads[thread_nb].pc;
+  state.source.function_id = state.threads[thread_nb].function_id;
 
   state.guard = state.threads[thread_nb].guard;
   // A thread's initial state is certainly reachable:

src/goto-symex/symex_start_thread.cpp

@@ -45,6 +45,7 @@ void goto_symext::symex_start_thread(statet &state)
   // statet::threadt &cur_thread=state.threads[state.source.thread_nr];
   statet::threadt &new_thread=state.threads.back();
   new_thread.pc=thread_target;
+  new_thread.function_id = state.source.function_id;
   new_thread.guard=state.guard;
   new_thread.call_stack.push_back(state.call_stack().top());
   new_thread.call_stack.back().local_objects.clear();