@@ -15,13 +15,14 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
1515 for (auto &goto_function : goto_model.goto_functions .function_map )
1616 {
1717 std::size_t function_pointer_call_counter = 0 ;
18+
1819 for_each_instruction_if (
1920 goto_function.second ,
2021 [](const goto_programt::targett it) {
2122 return it->is_function_call () && can_cast_expr<dereference_exprt>(
2223 it->get_function_call ().function ());
2324 },
24- [&](goto_programt::targett it) {
25+ [&](goto_programt::targett & it) {
2526 auto const &function_call = it->get_function_call ();
2627 auto const &function_pointer_dereference =
2728 to_dereference_expr (function_call.function ());
@@ -52,13 +53,22 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
5253
5354 // add assignment to the new function pointer variable, followed by a
5455 // call of the new variable
55- auto const assign_instruction = goto_programt::make_assignment (
56+ auto assign_instruction = goto_programt::make_assignment (
5657 code_assignt{new_function_pointer,
5758 function_pointer_dereference.pointer ()},
5859 source_location);
59- goto_function.second .body .insert_before (it, assign_instruction);
60- to_code_function_call (it->code ).function () =
60+
61+ goto_function.second .body .insert_before_swap (it, assign_instruction);
62+ const auto next = std::next (it);
63+ to_code_function_call (next->code ).function () =
6164 dereference_exprt{new_function_pointer};
65+ // we need to increment the iterator once more (in addition to the
66+ // increment already done by for_each_goto_function_if()). This is
67+ // because insert_before_swap() inserts a new instruction after the
68+ // instruction pointed to by it (and then swaps the contents with the
69+ // previous instruction). We need to increment the iterator as we also
70+ // need to skip over this newly inserted instruction.
71+ it++;
6272 });
6373 }
6474}
0 commit comments