File tree 3 files changed +19
-18
lines changed
3 files changed +19
-18
lines changed Original file line number Diff line number Diff line change @@ -840,19 +840,3 @@ void goto_symex_statet::get_l1_name(exprt &expr) const
840
840
Forall_operands (it, expr)
841
841
get_l1_name (*it);
842
842
}
843
-
844
- void goto_symex_statet::switch_to_thread (unsigned t)
845
- {
846
- PRECONDITION (source.thread_nr < threads.size ());
847
- PRECONDITION (t < threads.size ());
848
-
849
- // save PC
850
- threads[source.thread_nr ].pc =source.pc ;
851
- threads[source.thread_nr ].atomic_section_id =atomic_section_id;
852
-
853
- // get new PC
854
- source.thread_nr =t;
855
- source.pc =threads[t].pc ;
856
-
857
- guard=threads[t].guard ;
858
- }
Original file line number Diff line number Diff line change @@ -377,7 +377,6 @@ class goto_symex_statet final
377
377
void populate_dirty_for_function (
378
378
const irep_idt &id, const goto_functiont &);
379
379
380
- void switch_to_thread (unsigned t);
381
380
bool record_events;
382
381
incremental_dirtyt dirty;
383
382
Original file line number Diff line number Diff line change @@ -154,6 +154,24 @@ void goto_symext::initialize_entry_point(
154
154
symex_transition (state, state.source .pc , false );
155
155
}
156
156
157
+ static void
158
+ switch_to_thread (goto_symex_statet &state, const unsigned int thread_nb)
159
+ {
160
+ PRECONDITION (state.source .thread_nr < state.threads .size ());
161
+ PRECONDITION (thread_nb < state.threads .size ());
162
+
163
+ // save PC
164
+ state.threads [state.source .thread_nr ].pc = state.source .pc ;
165
+ state.threads [state.source .thread_nr ].atomic_section_id =
166
+ state.atomic_section_id ;
167
+
168
+ // get new PC
169
+ state.source .thread_nr = thread_nb;
170
+ state.source .pc = state.threads [thread_nb].pc ;
171
+
172
+ state.guard = state.threads [thread_nb].guard ;
173
+ }
174
+
157
175
void goto_symext::symex_threaded_step (
158
176
statet &state, const get_goto_functiont &get_goto_function)
159
177
{
@@ -173,7 +191,7 @@ void goto_symext::symex_threaded_step(
173
191
#if 0
174
192
std::cout << "********* Now executing thread " << t << '\n';
175
193
#endif
176
- state. switch_to_thread (t);
194
+ switch_to_thread (state, t);
177
195
symex_transition (state, state.source .pc , false );
178
196
}
179
197
}
You can’t perform that action at this time.
0 commit comments