Default fall-through for function pointer removal

When the pointer points to neither of the candidates we shouldn't just call the
first one (which does happen if the user does not request pointer-check). This
PR inserts an ASSUME (false) which makes all subsequent assertions
unreachable (and thus reported as not being violated).

A small regression test is included.

Author: petr-bauch

regression/cbmc/Function_Pointer18/main.c

@@ -0,0 +1,34 @@
+// f is set to 0 -> does not point to either f1 or f2
+#include <assert.h>
+
+typedef int (*f_ptr)(int);
+
+extern f_ptr f;
+
+int f1(int j);
+int f2(int i);
+
+int f1(int j)
+{
+  f = &f2;
+  return 1;
+}
+int f2(int i)
+{
+  assert(0);
+  return 2;
+}
+
+f_ptr f = 0;
+
+int main()
+{
+  int x = 0;
+
+  x = f(x);
+  assert(x == 1);
+  x = f(x);
+  assert(x == 2);
+
+  return 0;
+}

regression/cbmc/Function_Pointer18/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+\[f2.assertion.1\] line [0-9]+ assertion 0: SUCCESS
+\[main.assertion.1\] line [0-9]+ assertion x == 1: SUCCESS
+\[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-programs/remove_function_pointers.cpp

@@ -416,6 +416,7 @@ void remove_function_pointerst::remove_function_pointer(
     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;