Add DECL and DEAD instructions when labelling function pointer call sites.

Previously, function pointer call site labelling introduced ASSIGNS and CALL instructions
to a fresh function pointer variable in the goto program without adding corresponding
DECL and DEAD instructions which made them look like global variables when they really
are local to the function.

Author: Remi Delmas

src/goto-programs/label_function_pointer_call_sites.cpp

@@ -52,24 +52,32 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
           goto_model.symbol_table.lookup_ref(call_site_symbol_name)
             .symbol_expr();
 
-        // add assignment to the new function pointer variable, followed by a
-        // call of the new variable
+        // add a DECL instruction for the function pointer variable
+        auto decl_instruction =
+          goto_programt::make_decl(new_function_pointer, source_location);
+
+        goto_function.second.body.insert_before_swap(it, decl_instruction);
+        ++it;
+
+        // add assignment to the new variable
         auto assign_instruction = goto_programt::make_assignment(
           code_assignt{new_function_pointer,
                        function_pointer_dereference.pointer()},
           source_location);
 
         goto_function.second.body.insert_before_swap(it, assign_instruction);
-        const auto next = std::next(it);
-        to_code_function_call(next->code_nonconst()).function() =
-          dereference_exprt{new_function_pointer};
-        // we need to increment the iterator once more (in addition to the
-        // increment already done by for_each_goto_function_if()). This is
-        // because insert_before_swap() inserts a new instruction after the
-        // instruction pointed to by it (and then swaps the contents with the
-        // previous instruction). We need to increment the iterator as we also
-        // need to skip over this newly inserted instruction.
-        it++;
+        ++it;
+
+        // transform original call into a call to the new variable
+        it->call_function() = dereference_exprt{new_function_pointer};
+        ++it;
+
+        // add a DEAD instruction for the new variable
+        auto dead_instruction =
+          goto_programt::make_dead(new_function_pointer, source_location);
+        goto_function.second.body.insert_before_swap(it, dead_instruction);
+        // the iterator now points to the DEAD instruction and will be
+        // incremented by the outer loop
       });
   }
 }