Skip to content

Commit 3b7e24b

Browse files
committed
Concurrency: ensure function name is correct when starting threads
goto-symex did not update the function identifier when switching threads, resulting in the last function of the previous thread being used up until the next function call.
1 parent d23ffc6 commit 3b7e24b

File tree

3 files changed

+3
-0
lines changed

3 files changed

+3
-0
lines changed

src/goto-symex/goto_symex_state.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -181,6 +181,7 @@ class goto_symex_statet final : public goto_statet
181181
struct threadt
182182
{
183183
goto_programt::const_targett pc;
184+
irep_idt function_id;
184185
guardt guard;
185186
call_stackt call_stack;
186187
std::map<irep_idt, unsigned> function_frame;

src/goto-symex/symex_main.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -292,6 +292,7 @@ switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
292292
// get new PC
293293
state.source.thread_nr = thread_nb;
294294
state.source.pc = state.threads[thread_nb].pc;
295+
state.source.function_id = state.threads[thread_nb].function_id;
295296

296297
state.guard = state.threads[thread_nb].guard;
297298
// A thread's initial state is certainly reachable:

src/goto-symex/symex_start_thread.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ void goto_symext::symex_start_thread(statet &state)
4545
// statet::threadt &cur_thread=state.threads[state.source.thread_nr];
4646
statet::threadt &new_thread=state.threads.back();
4747
new_thread.pc=thread_target;
48+
new_thread.function_id = state.source.function_id;
4849
new_thread.guard=state.guard;
4950
new_thread.call_stack.push_back(state.call_stack().top());
5051
new_thread.call_stack.back().local_objects.clear();

0 commit comments

Comments
 (0)