Merge pull request #4646 from xbauch/fix/function-pointer-removal-invalid

Default fall-through for function pointer removal

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;