Merge pull request #4940 from xbauch/fix/function-pointer-init

Stop generating nondet pointees for function pointers

Author: tautschnig

regression/cbmc/Function_Pointer_Init_No_Candidate/main.c

@@ -0,0 +1,13 @@
+#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
+  // requesting `pointer-check` will then 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

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

regression/cbmc/Function_Pointer_Init_One_Candidate/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int identity(int n)
+{
+  return n;
+}
+
+typedef int (*other_function_type)(int n);
+
+void foo(other_function_type other_function)
+{
+  // the following assertion is reachable and should fail (the only candidate is identity)
+  assert(other_function(4) == 5);
+  // the following assertion should succeed
+  assert(other_function(4) == 4);
+}
+
+int main()
+{
+  foo(&identity);
+  return 0;
+}

regression/cbmc/Function_Pointer_Init_One_Candidate/test.desc

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

regression/cbmc/Function_Pointer_Init_Two_Candidates/main.c

@@ -0,0 +1,27 @@
+#include <assert.h>
+
+int identity(int n)
+{
+  return n;
+}
+int increment(int n)
+{
+  return n + 1;
+}
+
+typedef int (*other_function_type)(int n);
+
+void foo(other_function_type other_function)
+{
+  // the following assertion is reachable and should fail (because of the identity case)
+  assert(other_function(4) == 5);
+  // the following assertion should succeed (satisfied by both candidates)
+  assert(other_function(4) >= 4);
+}
+
+int main()
+{
+  foo(&identity);
+  foo(&increment);
+  return 0;
+}

regression/cbmc/Function_Pointer_Init_Two_Candidates/test.desc

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

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -54,6 +54,16 @@ void symbol_factoryt::gen_nondet_init(
     const pointer_typet &pointer_type=to_pointer_type(type);
     const typet &subtype = pointer_type.subtype();
 
+    if(subtype.id() == ID_code)
+    {
+      // Handle the pointer-to-code case separately:
+      // leave as nondet_ptr to allow `remove_function_pointers`
+      // to replace the pointer.
+      assignments.add(
+        code_assignt{expr, side_effect_expr_nondett{pointer_type, loc}});
+      return;
+    }
+
     if(subtype.id() == ID_struct_tag)
     {
       const irep_idt struct_tag = to_struct_tag_type(subtype).get_identifier();