Add overloads of remove_virtual_functions that take a pre-computed class_hierarchyt

This allows driver programs to avoid pointless recomputation. In the process sort out the
function documentation, moving it to the implementation site per convention and documenting
parameters.

Author: smowton

src/goto-programs/remove_virtual_functions.cpp

@@ -737,6 +737,8 @@ void remove_virtual_functionst::operator()(goto_functionst &functions)
 
 /// Remove virtual function calls from all functions in the specified
 /// list and replace them with their most derived implementations
+/// \param symbol_table: symbol table associated with \p goto_functions
+/// \param goto_functions: functions from which to remove virtual function calls
 void remove_virtual_functions(
   symbol_table_baset &symbol_table,
   goto_functionst &goto_functions)
@@ -747,14 +749,47 @@ void remove_virtual_functions(
   rvf(goto_functions);
 }
 
+/// Remove virtual function calls from all functions in the specified
+/// list and replace them with their most derived implementations
+/// \param symbol_table: symbol table associated with \p goto_functions
+/// \param goto_functions: functions from which to remove virtual function calls
+/// \param class_hierarchy: class hierarchy derived from symbol_table
+///   This should already be populated (i.e. class_hierarchyt::operator() has
+///   already been called)
+void remove_virtual_functions(
+  symbol_table_baset &symbol_table,
+  goto_functionst &goto_functions,
+  const class_hierarchyt &class_hierarchy)
+{
+  remove_virtual_functionst rvf(symbol_table, class_hierarchy);
+  rvf(goto_functions);
+}
+
 /// Remove virtual function calls from the specified model
+/// \param goto_model: model from which to remove virtual functions
 void remove_virtual_functions(goto_modelt &goto_model)
 {
   remove_virtual_functions(
     goto_model.symbol_table, goto_model.goto_functions);
 }
 
+/// Remove virtual function calls from the specified model
+/// \param goto_model: model from which to remove virtual functions
+/// \param class_hierarchy: class hierarchy derived from model.symbol_table
+///   This should already be populated (i.e. class_hierarchyt::operator() has
+///   already been called)
+void remove_virtual_functions(
+  goto_modelt &goto_model,
+  const class_hierarchyt &class_hierarchy)
+{
+  remove_virtual_functions(
+    goto_model.symbol_table, goto_model.goto_functions, class_hierarchy);
+}
+
 /// Remove virtual function calls from the specified model function
+/// May change the location numbers in `function`.
+/// \param function: function from which virtual functions should be converted
+///   to explicit dispatch tables.
 void remove_virtual_functions(goto_model_functiont &function)
 {
   class_hierarchyt class_hierarchy;
@@ -764,6 +799,22 @@ void remove_virtual_functions(goto_model_functiont &function)
     function.get_function_id(), function.get_goto_function().body);
 }
 
+/// Remove virtual function calls from the specified model function
+/// May change the location numbers in `function`.
+/// \param function: function from which virtual functions should be converted
+///   to explicit dispatch tables.
+/// \param class_hierarchy: class hierarchy derived from function.symbol_table
+///   This should already be populated (i.e. class_hierarchyt::operator() has
+///   already been called)
+void remove_virtual_functions(
+  goto_model_functiont &function,
+  const class_hierarchyt &class_hierarchy)
+{
+  remove_virtual_functionst rvf(function.get_symbol_table(), class_hierarchy);
+  rvf.remove_virtual_functions(
+    function.get_function_id(), function.get_goto_function().body);
+}
+
 /// Replace virtual function call with a static function call
 /// Achieved by substituting a virtual function with its most derived
 /// implementation. If there's a type mismatch between implementation

src/goto-programs/remove_virtual_functions.h

@@ -26,19 +26,32 @@ class goto_model_functiont;
 class goto_modelt;
 class symbol_table_baset;
 
+// For all of the following the class-hierarchy and non-class-hierarchy
+// overloads are equivalent, but the class-hierarchy-taking one saves time if
+// you already have a class-hierarchy object available.
+
 void remove_virtual_functions(
   goto_modelt &goto_model);
 
+void remove_virtual_functions(
+  goto_modelt &goto_model,
+  const class_hierarchyt &class_hierarchy);
+
 void remove_virtual_functions(
   symbol_table_baset &symbol_table,
   goto_functionst &goto_functions);
 
-/// Remove virtual functions from one function.
-/// May change the location numbers in `function`.
-/// \param function: function from which virtual functions should be converted
-///   to explicit dispatch tables.
+void remove_virtual_functions(
+  symbol_table_baset &symbol_table,
+  goto_functionst &goto_functions,
+  const class_hierarchyt &class_hierarchy);
+
 void remove_virtual_functions(goto_model_functiont &function);
 
+void remove_virtual_functions(
+  goto_model_functiont &function,
+  const class_hierarchyt &class_hierarchy);
+
 /// Specifies remove_virtual_function's behaviour when the actual supplied
 /// parameter does not match any of the possible callee types
 enum class virtual_dispatch_fallback_actiont