Correct nondet init of function pointer arguments

regression/cbmc/pointer-function-origin-argument/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+typedef int (*other_function_type)(int n);
+
+void foo(other_function_type other_function)
+{
+  assert(other_function(4) > 5);
+}

regression/cbmc/pointer-function-origin-argument/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--function foo
+^EXIT=10$
+^SIGNAL=0$
+^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: FAILURE$
+VERIFICATION FAILED
+--
+^warning: ignoring

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -54,6 +54,47 @@ void symbol_factoryt::gen_nondet_init(
     const pointer_typet &pointer_type=to_pointer_type(type);
     const typet &subtype = pointer_type.subtype();
 
+    //TODO check if really is not target candidate
+    if(subtype.id() == ID_code)
+    {
+      symbolt function_symbol;
+      code_typet function_type = to_code_type(subtype);
+
+      for(size_t index = 0; index < function_type.parameters().size(); index++)
+      {
+        auto &param = function_type.parameters().at(index);
+        symbolt param_symbol;
+        param_symbol.type = param.type();
+        param_symbol.name = "param" + std::to_string(index);
+        param_symbol.base_name = param_symbol.name;
+        param_symbol.pretty_name = param_symbol.name;
+        param_symbol.mode = "C";
+        param_symbol.is_parameter = true;
+        //TODO check if not present
+        symbol_table.add(param_symbol);
+        param.set_identifier(param_symbol.name);
+        //TODO flags
+      }
+      function_symbol.type = function_type;
+      code_blockt function_body;
+      function_body.add(
+        code_returnt{side_effect_expr_nondett{function_type.return_type()}});
+      function_symbol.value = function_body;
+      //      function_symbol.name = CPROVER_PREFIX "_generated_function";
+      function_symbol.name = "my_generated_function";
+      function_symbol.base_name = function_symbol.name;
+      function_symbol.pretty_name = function_symbol.name;
+      function_symbol.mode = "C";
+      //TODO set flags
+      symbol_table.add(function_symbol);
+
+      // assignments.add(
+      //   code_assignt{expr, side_effect_expr_nondett{pointer_type, loc}});
+      assignments.add(
+        code_assignt{expr, address_of_exprt{function_symbol.symbol_expr()}});
+      return;
+    }
+
     if(subtype.id() == ID_struct_tag)
     {
       const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();

src/goto-programs/remove_function_pointers.cpp

@@ -416,6 +416,38 @@ void remove_function_pointerst::remove_function_pointer(
     t->source_location.set_property_class("pointer dereference");
     t->source_location.set_comment("invalid function pointer");
   }
+
+  const auto calling_from_entry = [&function_id, this]() -> bool {
+    const auto &cprover_start =
+      to_code_block(to_code(ns.lookup(CPROVER_PREFIX "_start").value));
+    for(const auto &statement_code : cprover_start.statements())
+    {
+      if(statement_code.get_statement() == ID_function_call)
+      {
+        const auto f_call = to_code_function_call(statement_code);
+        if(
+          f_call.function().id() == ID_symbol &&
+          to_symbol_expr(f_call.function()).get_identifier() == function_id)
+          return true;
+      }
+    }
+    return false;
+  };
+  const auto target_is_param = [&function_id, &pointer, this]() -> bool {
+    for(const auto &param :
+        to_code_type(ns.lookup(function_id).type).parameters())
+    {
+      if(param.get_identifier() == to_symbol_expr(pointer).get_identifier())
+        return true;
+    }
+    return false;
+  };
+
+  // do not cut this execution if the function pointer is the parameter of the
+  // entry point
+  if(functions.empty() && calling_from_entry() && target_is_param())
+    ;
+  //else
   new_code_gotos.add(goto_programt::make_assumption(false_exprt()));
 
   goto_programt new_code;