Function pointer parameter to function pointer argument

Add mapping from function pointer argument names to
local variable names of the harness so users can specify
properties of arguments in terms of the names of the
arguments rather than having to rely on internal
implementation details of the function harness.

Author: NlightNFotis

regression/goto-harness/function_pointer_nullable/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.c
---harness-type call-function --function entry_point --function-pointer-can-be-null __goto_harness::f_but_may_be_null
+--harness-type call-function --function entry_point --function-pointer-can-be-null entry_point::f_but_may_be_null
 ^EXIT=10$
 ^SIGNAL=0$
 \[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0: SUCCESS

src/goto-harness/function_call_harness_generator.cpp

@@ -81,6 +81,16 @@ struct function_call_harness_generatort::implt
   void call_function(
     const code_function_callt::argumentst &arguments,
     code_blockt &function_body);
+  /// For function parameters that are pointers to functions we want to
+  /// be able to specify whether or not they can be NULL. To disambiguate
+  /// this specification from that for a global variable of the same name,
+  /// we prepend the name of the function to the parameter name. However,
+  /// what is actually being initialised in the implementation is not the
+  /// parameter itself, but a correspond function argument (local variable
+  /// of the harness function). We need a mapping from function parameter
+  /// name to function argument names, and this is what this function does.
+  std::unordered_set<irep_idt>
+  map_function_parameters_to_function_argument_names();
 };
 
 function_call_harness_generatort::function_call_harness_generatort(
@@ -218,6 +228,8 @@ void function_call_harness_generatort::implt::generate(
     recursive_initialization_config.variables_that_hold_array_sizes.insert(
       pair.second);
   }
+  recursive_initialization_config.potential_null_function_pointers =
+    map_function_parameters_to_function_argument_names();
   recursive_initialization_config.pointers_to_treat_as_cstrings =
     function_arguments_to_treat_as_cstrings;
   recursive_initialization = util_make_unique<recursive_initializationt>(
@@ -335,6 +347,43 @@ void function_call_harness_generatort::validate_options(
         "--" FUNCTION_HARNESS_GENERATOR_TREAT_POINTERS_EQUAL_OPT};
     }
   }
+
+  const namespacet ns{goto_model.symbol_table};
+
+  // Make sure all function pointers that the user asks are nullable are
+  // present in the symbol table.
+  for(const auto &nullable :
+      p_impl->recursive_initialization_config.potential_null_function_pointers)
+  {
+    const auto &function_pointer_symbol_pointer =
+      goto_model.symbol_table.lookup(nullable);
+
+    if(function_pointer_symbol_pointer == nullptr)
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "nullable function pointer `" + id2string(nullable) +
+          "' not found in symbol table",
+        "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT};
+    }
+
+    const auto &function_pointer_type =
+      ns.follow(function_pointer_symbol_pointer->type);
+
+    if(!can_cast_type<pointer_typet>(function_pointer_type))
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "`" + id2string(nullable) + "' is not a pointer",
+        "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT};
+    }
+
+    if(!can_cast_type<code_typet>(
+         to_pointer_type(function_pointer_type).subtype()))
+    {
+      throw invalid_command_line_argument_exceptiont{
+        "`" + id2string(nullable) + "' is not pointing to a function",
+        "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT};
+    }
+  }
 }
 
 const symbolt &
@@ -468,3 +517,25 @@ void function_call_harness_generatort::implt::call_function(
 
   function_body.add(std::move(function_call));
 }
+
+std::unordered_set<irep_idt> function_call_harness_generatort::implt::
+  map_function_parameters_to_function_argument_names()
+{
+  std::unordered_set<irep_idt> nullables;
+  for(const auto &nullable :
+      recursive_initialization_config.potential_null_function_pointers)
+  {
+    const auto &nullable_name = id2string(nullable);
+    const auto &function_prefix = id2string(function) + "::";
+    if(has_prefix(nullable_name, function_prefix))
+    {
+      nullables.insert(
+        "__goto_harness::" + nullable_name.substr(function_prefix.size()));
+    }
+    else
+    {
+      nullables.insert(nullable_name);
+    }
+  }
+  return nullables;
+}