Merge pull request #6959 from tautschnig/bugfixes/function-pointer-arg-conversion

Function pointer removal: argument conversion must use byte extract

Author: tautschnig

regression/cbmc/Function_Pointer19/main.c

@@ -0,0 +1,51 @@
+#include <assert.h>
+
+struct PtrWrapperInner
+{
+  int *value;
+};
+
+struct PtrWrapper
+{
+  int *value;
+  struct PtrWrapperInner inner;
+};
+
+struct AltPtrWrapperInner
+{
+  int *value;
+};
+
+struct AltPtrWrapper
+{
+  unsigned int *value;
+  // A) Doesn't work
+  struct AltPtrWrapperInner inner;
+  // B) Works
+  // struct PtrWrapperInner inner;
+};
+
+void fn(struct PtrWrapper wrapper)
+{
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+}
+
+int main()
+{
+  int ret = 10;
+  int *ptr = &ret;
+
+  struct AltPtrWrapper alt;
+  alt.inner.value = ptr;
+  alt.value = ptr;
+
+  // Casting the structure itself works.
+  struct PtrWrapper wrapper = *(struct PtrWrapper *)&alt;
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+
+  // This only works if there is one level of casting.
+  int (*alias)(struct AltPtrWrapper) = (int (*)(struct AltPtrWrapper))fn;
+  alias(alt);
+}

regression/cbmc/Function_Pointer19/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Linking7/member-name-mismatch.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 module2.c
 ^EXIT=10$

regression/cbmc/Linking7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 module.c
 ^EXIT=10$

src/goto-programs/remove_function_pointers.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "remove_function_pointers.h"
 
+#include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
@@ -195,8 +197,10 @@ static void fix_argument_types(code_function_callt &function_call)
     {
       if(call_arguments[i].type() != function_parameters[i].type())
       {
-        call_arguments[i] =
-          typecast_exprt(call_arguments[i], function_parameters[i].type());
+        call_arguments[i] = make_byte_extract(
+          call_arguments[i],
+          from_integer(0, c_index_type()),
+          function_parameters[i].type());
       }
     }
   }
@@ -235,8 +239,10 @@ static void fix_return_type(
   exprt old_lhs=function_call.lhs();
   function_call.lhs()=tmp_symbol_expr;
 
-  dest.add(goto_programt::make_assignment(
-    code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
+  dest.add(goto_programt::make_assignment(code_assignt(
+    old_lhs,
+    make_byte_extract(
+      tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()))));
 }
 
 void remove_function_pointerst::remove_function_pointer(