Provide function name in goto_model_functiont

This is necessary because not all functions work with goto_programt::get_function_id,
e.g. those with empty bodies.

Author: smowton

src/goto-programs/goto_model.h

@@ -86,9 +86,11 @@ class goto_model_functiont
   goto_model_functiont(
     journalling_symbol_tablet &symbol_table,
     goto_functionst &goto_functions,
+    const irep_idt &function_id,
     goto_functionst::goto_functiont &goto_function):
   symbol_table(symbol_table),
   goto_functions(goto_functions),
+  function_id(function_id),
   goto_function(goto_function)
   {
   }
@@ -117,9 +119,17 @@ class goto_model_functiont
     return goto_function;
   }
 
+  /// Get function id
+  /// \return `goto_function`'s name (its key in `goto_functions`)
+  const irep_idt &get_function_id()
+  {
+    return function_id;
+  }
+
 private:
   journalling_symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
+  irep_idt function_id;
   goto_functionst::goto_functiont &goto_function;
 };
 

src/goto-programs/lazy_goto_functions_map.h

@@ -49,6 +49,7 @@ class lazy_goto_functions_mapt final
 
   typedef
     std::function<void(
+      const irep_idt &name,
       goto_functionst::goto_functiont &function,
       journalling_symbol_tablet &function_symbols)>
     post_process_functiont;
@@ -128,7 +129,7 @@ class lazy_goto_functions_mapt final
     if(processed_functions.count(name)==0)
     {
       // Run function-pass conversions
-      post_process_function(function, journalling_table);
+      post_process_function(name, function, journalling_table);
       // Assign procedure-local location numbers for now
       function.body.compute_location_numbers();
       processed_functions.insert(name);

src/goto-programs/lazy_goto_model.cpp

@@ -29,12 +29,14 @@ lazy_goto_modelt::lazy_goto_modelt(
       language_files,
       symbol_table,
       [this] (
+        const irep_idt &function_name,
         goto_functionst::goto_functiont &function,
         journalling_symbol_tablet &journalling_symbol_table) -> void
       {
         goto_model_functiont model_function(
           journalling_symbol_table,
           goto_model->goto_functions,
+          function_name,
           function);
         this->post_process_function(model_function, *this);
       },
@@ -54,12 +56,14 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
       language_files,
       symbol_table,
       [this] (
+        const irep_idt &function_name,
         goto_functionst::goto_functiont &function,
         journalling_symbol_tablet &journalling_symbol_table) -> void
       {
         goto_model_functiont model_function(
           journalling_symbol_table,
           goto_model->goto_functions,
+          function_name,
           function);
         this->post_process_function(model_function, *this);
       },