Set function member of each goto instruction in goto program passes

Author: peterschrammel

src/goto-programs/goto_convert_functions.cpp

@@ -213,9 +213,8 @@ void goto_convert_functionst::convert_function(
   // add "end of function"
   f.body.destructive_append(tmp_end_function);
 
-  // do function tags
-  Forall_goto_program_instructions(i_it, f.body)
-    i_it->function=identifier;
+  // do function tags (they are empty at this point)
+  f.update_instructions_function(identifier);
 
   f.body.update();
 

src/goto-programs/goto_functions_template.h

@@ -62,6 +62,14 @@ class goto_function_templatet
     parameter_identifiers.clear();
   }
 
+  /// update the function member in each instruction
+  /// \param function_id: the `function_id` used for assigning empty function
+  ///   members
+  void update_instructions_function(const irep_idt &function_id)
+  {
+    body.update_instructions_function(function_id);
+  }
+
   void swap(goto_function_templatet &other)
   {
     body.swap(other.body);
@@ -149,12 +157,23 @@ class goto_functions_templatet
   void compute_target_numbers();
   void compute_incoming_edges();
 
+  /// update the function member in each instruction by setting it to
+  /// the goto function's identifier
+  void update_instructions_function()
+  {
+    for(auto &func : function_map)
+    {
+      func.second.update_instructions_function(func.first);
+    }
+  }
+
   void update()
   {
     compute_incoming_edges();
     compute_target_numbers();
     compute_location_numbers();
     compute_loop_numbers();
+    update_instructions_function();
   }
 
   static inline irep_idt entry_point()

src/goto-programs/goto_model.h

@@ -103,6 +103,13 @@ class goto_model_functiont
     goto_functions.compute_location_numbers(goto_function.body);
   }
 
+  /// Updates the empty function member of each instruction by setting them
+  /// to `function_id`
+  void update_instructions_function()
+  {
+    goto_function.update_instructions_function(function_id);
+  }
+
   /// Get symbol table
   /// \return journalling symbol table that (a) wraps the global symbol table,
   ///   and (b) has recorded all symbol mutations (insertions, updates and

src/goto-programs/goto_program_template.h

@@ -521,6 +521,22 @@ class goto_program_templatet
     }
   }
 
+  /// Sets the `function` member of each instruction if not yet set
+  /// Note that a goto program need not be a goto function and therefore,
+  /// we cannot do this in update(), but only at the level of
+  /// of goto_functionst where goto programs are guaranteed to be
+  /// named functions.
+  void update_instructions_function(const irep_idt &function_id)
+  {
+    for(auto &instruction : instructions)
+    {
+      if(instruction.function.empty())
+      {
+        instruction.function = function_id;
+      }
+    }
+  }
+
   /// Compute location numbers
   void compute_location_numbers()
   {

src/jbmc/jbmc_parse_options.cpp

@@ -708,6 +708,9 @@ void jbmc_parse_optionst::process_goto_function(
         symbol_table.lookup_ref(new_symbol_name),
         symbol_table);
     }
+
+    // update the function member in each instruction
+    function.update_instructions_function();
   }
 
   catch(const char *e)