Merge pull request #6535 from remi-delmas-3000/function-pointer-call-site-add-decl-dead

Add missing DECL and DEAD instructions in function pointer call site labelling

Author: remi-delmas-3000

src/goto-programs/goto_program.h

@@ -625,6 +625,22 @@ class goto_programt
 
   /// Insertion that preserves jumps to "target".
   /// The instruction is destroyed.
+  ///
+  /// Turns:
+  /// ```
+  /// ...->[a]->...
+  ///       ^
+  ///     target
+  /// ```
+  ///
+  /// Into:
+  /// ```
+  /// ...->[i]->[a]->...
+  ///       ^
+  ///     target
+  /// ```
+  ///
+  /// So that jumps to `a` now jump to the newly inserted `i`.
   void insert_before_swap(targett target, instructiont &instruction)
   {
     insert_before_swap(target);

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
       });
   }
 }