Fix linking in case of function type conflict

regression/ansi-c/undeclared_function/fileB.c

@@ -1,4 +1,7 @@
-#include <stdlib.h>
+void *malloc(__CPROVER_size_t s)
+{
+  return (void *)0 + s;
+}
 
 int f()
 {

regression/ansi-c/undeclared_function/undeclared_function1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE gcc-only
 fileA.c
 fileB.c --validate-goto-model
 ^EXIT=0$

regression/cbmc/incomplete-structs/test.desc

@@ -0,0 +1,13 @@
+CORE
+typesmain.c
+types1.c types2.c types3.c
+reason for conflict at \*#this.u: number of members is different \(3/0\)
+reason for conflict at \*#this.u: number of members is different \(0/3\)
+struct U   \(incomplete\)
+warning: pointer parameter types differ between declaration and definition "bar"
+warning: pointer parameter types differ between declaration and definition "foo"
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/incomplete-structs/types1.c

@@ -0,0 +1,9 @@
+struct S
+{
+  int s;
+} s_object;
+
+int foobar()
+{
+  return s_object.s;
+}

regression/cbmc/incomplete-structs/types2.c

@@ -0,0 +1,16 @@
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+struct U
+{
+  struct S *s;
+  int j;
+};
+
+int bar(struct S *s)
+{
+  return s->u->j;
+}

regression/cbmc/incomplete-structs/types3.c

@@ -0,0 +1,17 @@
+struct T
+{
+  int i;
+};
+
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+int bar(struct S *);
+
+int foo(struct S *s)
+{
+  return bar(s) + s->t->i;
+}

regression/cbmc/incomplete-structs/typesmain.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+struct T
+{
+  int i;
+};
+
+struct U
+{
+  struct S *s;
+  int j;
+};
+
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+int foo(struct S *s);
+
+int main()
+{
+  struct T t = {10};
+  struct U u = {0, 32};
+  struct S s = {&t, &u};
+  int res = foo(&s);
+  assert(res == 42);
+}

regression/cbmc/return6/test.desc

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

regression/linking-goto-binaries/chain.sh

@@ -21,4 +21,4 @@ else
   $goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
 fi
 
-$cbmc "final.gb"
+$cbmc --validate-goto-model "final.gb"

regression/linking-goto-binaries/type_conflicts/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/linking-goto-binaries/type_conflicts/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/linking-goto-binaries/type_conflicts/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/linking-goto-binaries/type_conflicts/Linking7-return_type1.c

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+struct S
+{
+  int i;
+};
+
+struct S *function();
+
+int main()
+{
+  assert(function() != 0);
+}

regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c

@@ -0,0 +1,10 @@
+struct S
+{
+  int i;
+  int j; // extra member
+} some_var;
+
+struct S *function()
+{
+  return &some_var;
+}

regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc

@@ -0,0 +1,11 @@
+CORE
+Linking7-main.c
+Linking7-module2.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.c == 41: FAILURE
+^\*\* 1 of 3 failed
+--
+^warning: ignoring

regression/linking-goto-binaries/type_conflicts/return_type.desc

@@ -0,0 +1,10 @@
+CORE
+Linking7-return_type1.c
+Linking7-return_type2.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Note issue #3081

regression/linking-goto-binaries/type_conflicts/test.desc

@@ -0,0 +1,11 @@
+CORE
+Linking7-main.c
+Linking7-module.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 1 of 3 failed
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.b == 41: FAILURE
+--
+^warning: ignoring

src/goto-programs/link_goto_model.cpp

@@ -148,7 +148,7 @@ void finalize_linking(
   goto_modelt &dest,
   const replace_symbolt::expr_mapt &type_updates)
 {
-  unchecked_replace_symbolt object_type_updates;
+  casting_replace_symbolt object_type_updates;
   object_type_updates.get_expr_map().insert(
     type_updates.begin(), type_updates.end());
 
@@ -196,10 +196,30 @@ void finalize_linking(
     {
       for(auto &instruction : gf_entry.second.body.instructions)
       {
-        instruction.transform([&object_type_updates](exprt expr) {
-          object_type_updates(expr);
-          return expr;
-        });
+        if(instruction.is_function_call())
+        {
+          const bool changed =
+            !object_type_updates.replace(instruction.call_function());
+          if(changed && instruction.call_lhs().is_not_nil())
+          {
+            object_type_updates(instruction.call_lhs());
+            if(
+              instruction.call_lhs().type() !=
+              to_code_type(instruction.call_function().type()).return_type())
+            {
+              instruction.call_lhs() = typecast_exprt{
+                instruction.call_lhs(),
+                to_code_type(instruction.call_function().type()).return_type()};
+            }
+          }
+        }
+        else
+        {
+          instruction.transform([&object_type_updates](exprt expr) {
+            const bool changed = !object_type_updates.replace(expr);
+            return changed ? optionalt<exprt>{expr} : nullopt;
+          });
+        }
       }
     }
   }