Merge pull request diffblue#2558 from tautschnig/linking-xen

Accept more mismatching function definition/declaration pairs

regression/ansi-c/linking1/main.c

@@ -0,0 +1,7 @@
+void f(int);
+
+int main(int argc, char *argv[])
+{
+  f(argc);
+  return 0;
+}

regression/ansi-c/linking1/module.c

@@ -0,0 +1,3 @@
+void f(float param)
+{
+}

regression/ansi-c/linking1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+module.c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$

regression/cbmc/Linking7/main.c

@@ -0,0 +1,19 @@
+struct S
+{
+  void *a;
+  void *b;
+};
+
+typedef void (*fptr)(struct S);
+
+extern void foo(struct S s);
+
+fptr A[] = { foo };
+
+extern void bar();
+
+int main()
+{
+  bar();
+  return 0;
+}

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

@@ -0,0 +1,11 @@
+KNOWNBUG
+main.c
+module2.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 1 of 2 failed
+--
+^warning: ignoring
+--
+This is either a bug in goto-symex or value_sett (where the invariant fails).

regression/cbmc/Linking7/module.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+struct S
+{
+  void *a;
+  void *b;
+};
+
+typedef void (*fptr)(struct S);
+
+extern fptr A[1];
+
+struct real_S
+{
+  int *a;
+  int *b;
+};
+
+void foo(struct real_S g)
+{
+  assert(*g.a == 42);
+  assert(*g.b == 41);
+}
+
+void bar()
+{
+  int x = 42;
+  struct real_S s;
+  s.a = &x;
+  s.b = &x;
+  A[0]((struct S){ s.a, s.b });
+}

regression/cbmc/Linking7/module2.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+struct S
+{
+  void *a;
+  void *b;
+};
+
+typedef void (*fptr)(struct S);
+
+extern fptr A[1];
+
+struct real_S
+{
+  int *a;
+  int *c;
+};
+
+void foo(struct real_S g)
+{
+  assert(*g.a == 42);
+  assert(*g.c == 41);
+}
+
+void bar()
+{
+  int x = 42;
+  struct real_S s;
+  s.a = &x;
+  s.c = &x;
+  A[0]((struct S){ s.a, s.c });
+}

regression/cbmc/Linking7/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+module.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 1 of 2 failed
+--
+^warning: ignoring

src/goto-programs/remove_function_pointers.cpp

@@ -13,18 +13,18 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
+#include <util/base_type.h>
+#include <util/c_types.h>
 #include <util/fresh_symbol.h>
+#include <util/invariant.h>
+#include <util/message.h>
+#include <util/pointer_offset_size.h>
 #include <util/replace_expr.h>
 #include <util/source_location.h>
 #include <util/std_expr.h>
 #include <util/type_eq.h>
-#include <util/message.h>
-#include <util/base_type.h>
 
 #include <analyses/does_remove_const.h>
-#include <util/invariant.h>
-
-#include <util/c_types.h>
 
 #include "remove_skip.h"
 #include "compute_called_functions.h"
@@ -135,8 +135,8 @@ bool remove_function_pointerst::arg_is_type_compatible(
     return false;
   }
 
-  // structs/unions need to match,
-  // which could be made more generous
+  return pointer_offset_bits(call_type, ns) ==
+         pointer_offset_bits(function_type, ns);
 
   return false;
 }

src/linking/linking.cpp

@@ -701,6 +701,17 @@ void linkingt::duplicate_code_symbol(
           if(!found)
             break;
         }
+        // different non-pointer arguments with implementation - the
+        // implementation is always right, even though such code may
+        // be severely broken
+        else if(pointer_offset_bits(t1, ns)==pointer_offset_bits(t2, ns) &&
+                old_symbol.value.is_nil()!=new_symbol.value.is_nil())
+        {
+          if(warn_msg.empty())
+            warn_msg="non-pointer parameter types differ between "
+                     "declaration and definition";
+          replace=new_symbol.value.is_not_nil();
+        }
         else
           break;