Function pointer removal: create fall-back function call

regression/cbmc/Function_Pointer18/test.desc

@@ -1,11 +1,13 @@
 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
+^\*\*\*\* WARNING: no body for function main::fptr_call
+^\*\*\*\* WARNING: no body for function main::fptr_call\$0
+\[f2.assertion.1\] line [0-9]+ assertion 0: FAILURE
+\[main.assertion.1\] line [0-9]+ assertion x == 1: FAILURE
 \[main.assertion.2\] line [0-9]+ assertion x == 2: SUCCESS
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
 --
 ^warning: ignoring

regression/cbmc/Function_Pointer20/main.c

@@ -0,0 +1,26 @@
+#include <assert.h>
+
+struct PtrWrapper
+{
+  char *value_c;
+};
+
+void fn(struct PtrWrapper wrapper)
+{
+  assert(wrapper.value_c == 'B');
+}
+
+void indirect(int (*fn_ptr)(char *), char *data)
+{
+  fn_ptr(data);
+  assert(0);
+}
+
+int main()
+{
+  struct PtrWrapper wrapper;
+  wrapper.value_c = 'A';
+
+  int (*alias)(char *) = (int (*)(char *))fn;
+  indirect(alias, &wrapper.value_c);
+}

regression/cbmc/Function_Pointer20/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^\*\*\*\* WARNING: no body for function indirect::fptr_call
+^\[indirect.assertion.1\] line 16 assertion 0: FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Function_Pointer_Init_No_Candidate/main.c

@@ -4,9 +4,7 @@ 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
-  // requesting `pointer-check` will then catch the fact that there is no valid
+  // requesting `pointer-check` will catch the fact that there is no valid
   //   candidate function to call resulting in an invalid function pointer
   //   failure
   assert(other_function(4) > 5);

regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --function foo --pointer-check
-^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$
+^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: FAILURE$
 ^\[foo.pointer_dereference.\d+\] line \d+ no candidates for dereferenced function pointer: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$

regression/goto-analyzer/value-set-function-pointers-simple/test.desc

@@ -10,7 +10,7 @@ main.c
 ^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\) :value-set-end
 ^main::1::fun2_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
 ^main::1::fun3_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
-^fun_global_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end
+^fun_global_show \(\) -> value-set-begin: TOP :value-set-end
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/goto-instrument/value-set-fi-fp-removal4/test.desc

@@ -5,6 +5,7 @@ test.c
 ^SIGNAL=0$
 ^file test.c line 20 function main: replacing function pointer by 2 possible targets$
 --
+--
 This test checks that the value-set-fi-based function pointer removal
 precisely identifies the function to call for a particular function pointer
 call.

regression/goto-instrument/value-set-fi-fp-removal5/test.desc

@@ -5,6 +5,7 @@ test.c
 ^SIGNAL=0$
 ^file test.c line 19 function main: replacing function pointer by 0 possible targets$
 --
+--
 This test checks that the value-set-fi-based function pointer removal
 precisely identifies the function to call for a particular function pointer
 call.

src/goto-instrument/value_set_fi_fp_removal.cpp

@@ -31,6 +31,7 @@ void value_set_fi_fp_removal(
   message.status() << "Instrumenting" << messaget::eom;
 
   // now replace aliases by addresses
+  std::list<irep_idt> fall_back_fns;
   for(auto &f : goto_model.goto_functions.function_map)
   {
     for(auto target = f.second.body.instructions.begin();
@@ -69,18 +70,26 @@ void value_set_fi_fp_removal(
 
           if(functions.size() > 0)
           {
-            remove_function_pointer(
+            fall_back_fns.push_back(remove_function_pointer(
               message_handler,
               goto_model.symbol_table,
               f.second.body,
               f.first,
               target,
               functions,
-              true);
+              true));
           }
         }
       }
     }
   }
-  goto_model.goto_functions.update();
+
+  for(const auto &id : fall_back_fns)
+  {
+    goto_model.goto_functions.function_map[id].set_parameter_identifiers(
+      to_code_type(ns.lookup(id).type));
+  }
+
+  if(!fall_back_fns.empty())
+    goto_model.goto_functions.update();
 }