Function pointer restrictions: simplify interface

Rather than requiring users to (necessarily!) make at least two calls,
just process what users actually have available (a goto model and some
command line options).

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1029,12 +1029,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     {
       label_function_pointer_call_sites(goto_model);
 
-      const auto function_pointer_restrictions =
-        function_pointer_restrictionst::from_options(
-          options, goto_model, log.get_message_handler());
-
-      restrict_function_pointers(
-        ui_message_handler, goto_model, function_pointer_restrictions);
+      restrict_function_pointers(ui_message_handler, goto_model, options);
     }
   }
 

src/goto-programs/restrict_function_pointers.cpp

@@ -169,8 +169,13 @@ void function_pointer_restrictionst::typecheck_function_pointer_restrictions(
 void restrict_function_pointers(
   message_handlert &message_handler,
   goto_modelt &goto_model,
-  const function_pointer_restrictionst &restrictions)
+  const optionst &options)
 {
+  const auto restrictions = function_pointer_restrictionst::from_options(
+    options, goto_model, message_handler);
+  if(restrictions.restrictions.empty())
+    return;
+
   for(auto &function_item : goto_model.goto_functions.function_map)
   {
     goto_functiont &goto_function = function_item.second;

src/goto-programs/restrict_function_pointers.h

@@ -164,6 +164,6 @@ class function_pointer_restrictionst
 void restrict_function_pointers(
   message_handlert &message_handler,
   goto_modelt &goto_model,
-  const function_pointer_restrictionst &restrictions);
+  const optionst &options);
 
 #endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H