Stop generating nondet pointees for function pointers

when building the entry point. Because that leads to declaring function-type
objects and then assigning values to them. Rather we should simply initialise
the function pointer with NONDET(fptr_type) and let the function-pointer removal
find the candidates.

Author: petr-bauch

regression/cbmc/Function_Pointer_Init/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+typedef int (*other_function_type)(int n);
+
+void foo(other_function_type other_function)
+{
+  // returning from the function call is unreachable -> the following assertion
+  // should succeed
+  assert(other_function(4) > 5);
+}

regression/cbmc/Function_Pointer_Init/test.desc

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

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -48,7 +48,7 @@ void symbol_factoryt::gen_nondet_init(
     return;
   }
 
-  if(type.id()==ID_pointer)
+  if(type.id() == ID_pointer && to_pointer_type(type).subtype().id() != ID_code)
   {
     // dereferenced type
     const pointer_typet &pointer_type=to_pointer_type(type);

src/goto-programs/remove_function_pointers.cpp

@@ -408,14 +408,12 @@ void remove_function_pointerst::remove_function_pointer(
       goto_programt::make_goto(call, equal_exprt(pointer, casted_address)));
   }
 
-  // fall-through
-  if(add_safety_assertion)
-  {
-    goto_programt::targett t =
-      new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
-    t->source_location.set_property_class("pointer dereference");
-    t->source_location.set_comment("invalid function pointer");
-  }
+  // fall-through: always on
+  goto_programt::targett t =
+    new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
+  t->source_location.set_property_class("pointer dereference");
+  t->source_location.set_comment("invalid function pointer");
+
   new_code_gotos.add(goto_programt::make_assumption(false_exprt()));
 
   goto_programt new_code;