diff --git a/regression/ansi-c/undeclared_function/fileB.c b/regression/ansi-c/undeclared_function/fileB.c
index 08bdda49110..5ac12a5caa1 100644
--- a/regression/ansi-c/undeclared_function/fileB.c
+++ b/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()
 {
diff --git a/regression/ansi-c/undeclared_function/undeclared_function1.desc b/regression/ansi-c/undeclared_function/undeclared_function1.desc
index d002ebcf531..a1d43feedbd 100644
--- a/regression/ansi-c/undeclared_function/undeclared_function1.desc
+++ b/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$
diff --git a/regression/cbmc/incomplete-structs/test.desc b/regression/cbmc/incomplete-structs/test.desc
new file mode 100644
index 00000000000..47de5a75263
--- /dev/null
+++ b/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
diff --git a/regression/cbmc/incomplete-structs/types1.c b/regression/cbmc/incomplete-structs/types1.c
new file mode 100644
index 00000000000..43dec03a9e4
--- /dev/null
+++ b/regression/cbmc/incomplete-structs/types1.c
@@ -0,0 +1,9 @@
+struct S
+{
+  int s;
+} s_object;
+
+int foobar()
+{
+  return s_object.s;
+}
diff --git a/regression/cbmc/incomplete-structs/types2.c b/regression/cbmc/incomplete-structs/types2.c
new file mode 100644
index 00000000000..77cb91d53cd
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/incomplete-structs/types3.c b/regression/cbmc/incomplete-structs/types3.c
new file mode 100644
index 00000000000..d3e0617b180
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/incomplete-structs/typesmain.c b/regression/cbmc/incomplete-structs/typesmain.c
new file mode 100644
index 00000000000..13e80a03bb2
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc/return6/test.desc b/regression/cbmc/return6/test.desc
index 2fc10d239b2..bf09360fa4c 100644
--- a/regression/cbmc/return6/test.desc
+++ b/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$
diff --git a/regression/linking-goto-binaries/chain.sh b/regression/linking-goto-binaries/chain.sh
index efe0cdf23a9..d74593341a0 100755
--- a/regression/linking-goto-binaries/chain.sh
+++ b/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"
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-main.c b/regression/linking-goto-binaries/type_conflicts/Linking7-main.c
new file mode 100644
index 00000000000..5233bb3b3ff
--- /dev/null
+++ b/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;
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-module.c b/regression/linking-goto-binaries/type_conflicts/Linking7-module.c
new file mode 100644
index 00000000000..8a790b3f49d
--- /dev/null
+++ b/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});
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-module2.c b/regression/linking-goto-binaries/type_conflicts/Linking7-module2.c
new file mode 100644
index 00000000000..bf7f87eaf8f
--- /dev/null
+++ 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});
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c
new file mode 100644
index 00000000000..eb05a3e45c8
--- /dev/null
+++ b/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);
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c
new file mode 100644
index 00000000000..598484e7095
--- /dev/null
+++ b/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;
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc b/regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc
new file mode 100644
index 00000000000..317b01d93d1
--- /dev/null
+++ b/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
diff --git a/regression/linking-goto-binaries/type_conflicts/return_type.desc b/regression/linking-goto-binaries/type_conflicts/return_type.desc
new file mode 100644
index 00000000000..2854da5c7c6
--- /dev/null
+++ b/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
diff --git a/regression/linking-goto-binaries/type_conflicts/test.desc b/regression/linking-goto-binaries/type_conflicts/test.desc
new file mode 100644
index 00000000000..938fac85344
--- /dev/null
+++ b/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
diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp
index 75141785e53..f3207e6a5fa 100644
--- a/src/goto-programs/link_goto_model.cpp
+++ b/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;
+          });
+        }
       }
     }
   }
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 0b175ddc522..c365be90f2e 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -10,9 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// ANSI-C Linking
 
 #include "linking.h"
-
-#include <deque>
-#include <unordered_set>
+#include "linking_class.h"
 
 #include <util/c_types.h>
 #include <util/find_symbols.h>
@@ -20,11 +18,77 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
 #include <util/symbol_table.h>
 
 #include <langapi/language_util.h>
 
-#include "linking_class.h"
+#include <deque>
+
+bool casting_replace_symbolt::replace(exprt &dest) const
+{
+  bool result = true; // unchanged
+
+  // first look at type
+
+  const exprt &const_dest(dest);
+  if(have_to_replace(const_dest.type()))
+    if(!replace_symbolt::replace(dest.type()))
+      result = false;
+
+  // now do expression itself
+
+  if(!have_to_replace(dest))
+    return result;
+
+  if(dest.id() == ID_side_effect)
+  {
+    if(auto call = expr_try_dynamic_cast<side_effect_expr_function_callt>(dest))
+    {
+      if(!have_to_replace(call->function()))
+        return replace_symbolt::replace(dest);
+
+      exprt before = dest;
+      code_typet type = to_code_type(call->function().type());
+
+      result &= replace_symbolt::replace(call->function());
+
+      // maybe add type casts here?
+      for(auto &arg : call->arguments())
+        result &= replace_symbolt::replace(arg);
+
+      if(
+        type.return_type() !=
+        to_code_type(call->function().type()).return_type())
+      {
+        call->type() = to_code_type(call->function().type()).return_type();
+        dest = typecast_exprt(*call, type.return_type());
+        result = true;
+      }
+
+      return result;
+    }
+  }
+  else if(dest.id() == ID_address_of)
+  {
+    pointer_typet ptr_type = to_pointer_type(dest.type());
+
+    result &= replace_symbolt::replace(dest);
+
+    address_of_exprt address_of = to_address_of_expr(dest);
+    if(address_of.object().type() != ptr_type.base_type())
+    {
+      to_pointer_type(address_of.type()).base_type() =
+        address_of.object().type();
+      dest = typecast_exprt{address_of, std::move(ptr_type)};
+      result = true;
+    }
+
+    return result;
+  }
+
+  return replace_symbolt::replace(dest);
+}
 
 bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 {
@@ -35,7 +99,7 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 
   const exprt &e = it->second;
 
-  if(e.type().id() != ID_array)
+  if(e.type().id() != ID_array && e.type().id() != ID_code)
   {
     typet type = s.type();
     static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
@@ -126,7 +190,7 @@ std::string linkingt::type_to_string_verbose(
   return type_to_string(symbol.name, type);
 }
 
-void linkingt::detailed_conflict_report_rec(
+bool linkingt::detailed_conflict_report_rec(
   const symbolt &old_symbol,
   const symbolt &new_symbol,
   const typet &type1,
@@ -134,9 +198,11 @@ void linkingt::detailed_conflict_report_rec(
   unsigned depth,
   exprt &conflict_path)
 {
-  #ifdef DEBUG
+  bool conclusive = false;
+
+#ifdef DEBUG
   debug() << "<BEGIN DEPTH " << depth << ">" << eom;
-  #endif
+#endif
 
   std::string msg;
 
@@ -144,7 +210,10 @@ void linkingt::detailed_conflict_report_rec(
   const typet &t2=follow_tags_symbols(ns, type2);
 
   if(t1.id()!=t2.id())
+  {
     msg="type classes differ";
+    conclusive = true;
+  }
   else if(t1.id()==ID_pointer ||
           t1.id()==ID_array)
   {
@@ -155,7 +224,7 @@ void linkingt::detailed_conflict_report_rec(
       if(conflict_path.type().id() == ID_pointer)
         conflict_path = dereference_exprt(conflict_path);
 
-      detailed_conflict_report_rec(
+      conclusive = detailed_conflict_report_rec(
         old_symbol,
         new_symbol,
         to_type_with_subtype(t1).subtype(),
@@ -184,6 +253,7 @@ void linkingt::detailed_conflict_report_rec(
       msg="number of members is different (";
       msg+=std::to_string(components1.size())+'/';
       msg+=std::to_string(components2.size())+')';
+      conclusive = true;
     }
     else
     {
@@ -197,7 +267,7 @@ void linkingt::detailed_conflict_report_rec(
           msg="names of member "+std::to_string(i)+" differ (";
           msg+=id2string(components1[i].get_name())+'/';
           msg+=id2string(components2[i].get_name())+')';
-          break;
+          conclusive = true;
         }
         else if(subtype1 != subtype2)
         {
@@ -210,6 +280,7 @@ void linkingt::detailed_conflict_report_rec(
                 e.id()==ID_index)
           {
             parent_types.insert(e.type());
+            parent_types.insert(follow_tags_symbols(ns, e.type()));
             if(e.id() == ID_dereference)
               e = to_dereference_expr(e).pointer();
             else if(e.id() == ID_member)
@@ -220,44 +291,32 @@ void linkingt::detailed_conflict_report_rec(
               UNREACHABLE;
           }
 
-          conflict_path=conflict_path_before;
-          conflict_path.type()=t1;
-          conflict_path=
-            member_exprt(conflict_path, components1[i]);
-
-          if(depth>0 &&
-             parent_types.find(t1)==parent_types.end())
-            detailed_conflict_report_rec(
-              old_symbol,
-              new_symbol,
-              subtype1,
-              subtype2,
-              depth-1,
-              conflict_path);
-          else
+          if(parent_types.find(subtype1) == parent_types.end())
           {
-            msg="type of member "+
-                id2string(components1[i].get_name())+
-                " differs";
-            if(depth>0)
+            conflict_path = conflict_path_before;
+            conflict_path.type() = t1;
+            conflict_path = member_exprt(conflict_path, components1[i]);
+
+            if(depth > 0)
             {
-              std::string msg_bak;
-              msg_bak.swap(msg);
-              symbol_exprt c = symbol_exprt::typeless(ID_C_this);
-              detailed_conflict_report_rec(
+              conclusive = detailed_conflict_report_rec(
                 old_symbol,
                 new_symbol,
                 subtype1,
                 subtype2,
-                depth-1,
-                c);
-              msg.swap(msg_bak);
+                depth - 1,
+                conflict_path);
             }
           }
-
-          if(parent_types.find(t1)==parent_types.end())
-            break;
+          else
+          {
+            msg = "type of member " + id2string(components1[i].get_name()) +
+                  " differs (recursive)";
+          }
         }
+
+        if(conclusive)
+          break;
       }
     }
   }
@@ -280,12 +339,14 @@ void linkingt::detailed_conflict_report_rec(
       msg +=
         type_to_string(new_symbol.name, to_c_enum_type(t2).underlying_type()) +
         ')';
+      conclusive = true;
     }
     else if(members1.size()!=members2.size())
     {
       msg="number of enum members is different (";
       msg+=std::to_string(members1.size())+'/';
       msg+=std::to_string(members2.size())+')';
+      conclusive = true;
     }
     else
     {
@@ -296,15 +357,18 @@ void linkingt::detailed_conflict_report_rec(
           msg="names of member "+std::to_string(i)+" differ (";
           msg+=id2string(members1[i].get_base_name())+'/';
           msg+=id2string(members2[i].get_base_name())+')';
-          break;
+          conclusive = true;
         }
         else if(members1[i].get_value()!=members2[i].get_value())
         {
           msg="values of member "+std::to_string(i)+" differ (";
           msg+=id2string(members1[i].get_value())+'/';
           msg+=id2string(members2[i].get_value())+')';
-          break;
+          conclusive = true;
         }
+
+        if(conclusive)
+          break;
       }
     }
 
@@ -328,21 +392,25 @@ void linkingt::detailed_conflict_report_rec(
       msg="parameter counts differ (";
       msg+=std::to_string(parameters1.size())+'/';
       msg+=std::to_string(parameters2.size())+')';
+      conclusive = true;
     }
     else if(return_type1 != return_type2)
     {
+      conflict_path.type() = array_typet{void_type(), nil_exprt{}};
       conflict_path=
         index_exprt(conflict_path,
                     constant_exprt(std::to_string(-1), integer_typet()));
 
       if(depth>0)
-        detailed_conflict_report_rec(
+      {
+        conclusive = detailed_conflict_report_rec(
           old_symbol,
           new_symbol,
           return_type1,
           return_type2,
-          depth-1,
+          depth - 1,
           conflict_path);
+      }
       else
         msg="return types differ";
     }
@@ -355,30 +423,37 @@ void linkingt::detailed_conflict_report_rec(
 
         if(subtype1 != subtype2)
         {
+          conflict_path.type() = array_typet{void_type(), nil_exprt{}};
           conflict_path=
             index_exprt(conflict_path,
                         constant_exprt(std::to_string(i), integer_typet()));
 
           if(depth>0)
-            detailed_conflict_report_rec(
+          {
+            conclusive = detailed_conflict_report_rec(
               old_symbol,
               new_symbol,
               subtype1,
               subtype2,
-              depth-1,
+              depth - 1,
               conflict_path);
+          }
           else
             msg="parameter types differ";
+        }
 
+        if(conclusive)
           break;
-        }
       }
     }
   }
   else
+  {
     msg="conflict on POD";
+    conclusive = true;
+  }
 
-  if(!msg.empty())
+  if(conclusive && !msg.empty())
   {
     error() << '\n';
     error() << "reason for conflict at "
@@ -392,6 +467,8 @@ void linkingt::detailed_conflict_report_rec(
   #ifdef DEBUG
   debug() << "<END DEPTH " << depth << ">" << eom;
   #endif
+
+  return conclusive;
 }
 
 void linkingt::link_error(
@@ -477,19 +554,9 @@ void linkingt::duplicate_code_symbol(
     const code_typet &old_t=to_code_type(old_symbol.type);
     const code_typet &new_t=to_code_type(new_symbol.type);
 
-    // if one of them was an implicit declaration then only conflicts on the
-    // return type are an error as we would end up with assignments with
-    // mismatching types; as we currently do not patch these by inserting type
-    // casts we need to fail hard
     if(old_symbol.type.get_bool(ID_C_incomplete) && old_symbol.value.is_nil())
     {
-      if(old_t.return_type() == new_t.return_type())
-        link_warning(old_symbol, new_symbol, "implicit function declaration");
-      else
-        link_error(
-          old_symbol,
-          new_symbol,
-          "implicit function declaration");
+      link_warning(old_symbol, new_symbol, "implicit function declaration");
 
       old_symbol.type=new_symbol.type;
       old_symbol.location=new_symbol.location;
@@ -498,24 +565,16 @@ void linkingt::duplicate_code_symbol(
     else if(
       new_symbol.type.get_bool(ID_C_incomplete) && new_symbol.value.is_nil())
     {
-      if(old_t.return_type() == new_t.return_type())
-        link_warning(
-          old_symbol,
-          new_symbol,
-          "ignoring conflicting implicit function declaration");
-      else
-        link_error(
-          old_symbol,
-          new_symbol,
-          "implicit function declaration");
+      link_warning(
+        old_symbol,
+        new_symbol,
+        "ignoring conflicting implicit function declaration");
     }
     // handle (incomplete) function prototypes
-    else if(
-      old_t.return_type() == new_t.return_type() &&
-      ((old_t.parameters().empty() && old_t.has_ellipsis() &&
-        old_symbol.value.is_nil()) ||
-       (new_t.parameters().empty() && new_t.has_ellipsis() &&
-        new_symbol.value.is_nil())))
+    else if(((old_t.parameters().empty() && old_t.has_ellipsis() &&
+              old_symbol.value.is_nil()) ||
+             (new_t.parameters().empty() && new_t.has_ellipsis() &&
+              new_symbol.value.is_nil())))
     {
       if(old_t.parameters().empty() &&
          old_t.has_ellipsis() &&
@@ -565,9 +624,7 @@ void linkingt::duplicate_code_symbol(
     }
     // conflicting declarations without a definition, matching return
     // types
-    else if(
-      old_t.return_type() == new_t.return_type() && old_symbol.value.is_nil() &&
-      new_symbol.value.is_nil())
+    else if(old_symbol.value.is_nil() && new_symbol.value.is_nil())
     {
       link_warning(
         old_symbol,
@@ -607,8 +664,11 @@ void linkingt::duplicate_code_symbol(
       conflictst conflicts;
 
       if(old_t.return_type() != new_t.return_type())
-        conflicts.push_back(
-          std::make_pair(old_t.return_type(), new_t.return_type()));
+      {
+        link_warning(old_symbol, new_symbol, "conflicting return types");
+
+        conflicts.emplace_back(old_t.return_type(), new_t.return_type());
+      }
 
       code_typet::parameterst::const_iterator
         n_it=new_t.parameters().begin(),
@@ -658,21 +718,11 @@ void linkingt::duplicate_code_symbol(
         const typet &t1=follow_tags_symbols(ns, conflicts.front().first);
         const typet &t2=follow_tags_symbols(ns, conflicts.front().second);
 
-        // void vs. non-void return type may be acceptable if the
-        // return value is never used
-        if((t1.id()==ID_empty || t2.id()==ID_empty) &&
-           (old_symbol.value.is_nil() || new_symbol.value.is_nil()))
-        {
-          if(warn_msg.empty())
-            warn_msg="void/non-void return type conflict on function";
-          replace=
-            new_symbol.value.is_not_nil() ||
-            (old_symbol.value.is_nil() && t2.id()==ID_empty);
-        }
         // different pointer arguments without implementation may work
-        else if((t1.id()==ID_pointer || t2.id()==ID_pointer) &&
-                pointer_offset_bits(t1, ns)==pointer_offset_bits(t2, ns) &&
-                old_symbol.value.is_nil() && new_symbol.value.is_nil())
+        if(
+          (t1.id() == ID_pointer || t2.id() == ID_pointer) &&
+          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="different pointer types in extern function";
@@ -685,8 +735,16 @@ void linkingt::duplicate_code_symbol(
                 old_symbol.value.is_nil()!=new_symbol.value.is_nil())
         {
           if(warn_msg.empty())
+          {
             warn_msg="pointer parameter types differ between "
                      "declaration and definition";
+            detailed_conflict_report(
+              old_symbol,
+              new_symbol,
+              conflicts.front().first,
+              conflicts.front().second);
+          }
+
           replace=new_symbol.value.is_not_nil();
         }
         // transparent union with (or entirely without) implementation is
@@ -767,6 +825,9 @@ void linkingt::duplicate_code_symbol(
         }
       }
     }
+
+    object_type_updates.insert(
+      old_symbol.symbol_expr(), old_symbol.symbol_expr());
   }
 
   if(!new_symbol.value.is_nil())
@@ -781,6 +842,11 @@ void linkingt::duplicate_code_symbol(
       old_symbol.is_weak=new_symbol.is_weak;
       old_symbol.location=new_symbol.location;
       old_symbol.is_macro=new_symbol.is_macro;
+
+      // replace any previous update
+      object_type_updates.erase(old_symbol.name);
+      object_type_updates.insert(
+        old_symbol.symbol_expr(), old_symbol.symbol_expr());
     }
     else if(to_code_type(old_symbol.type).get_inlined())
     {
diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h
index c445fb1dc94..9fbb9c9b6b5 100644
--- a/src/linking/linking_class.h
+++ b/src/linking/linking_class.h
@@ -19,8 +19,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/symbol.h>
 #include <util/typecheck.h>
 
+#include <unordered_set>
+
 class casting_replace_symbolt : public replace_symbolt
 {
+public:
+  bool replace(exprt &dest) const override;
+
 private:
   bool replace_symbol_expr(symbol_exprt &dest) const override;
 };
@@ -131,7 +136,10 @@ class linkingt:public typecheckt
     return type_to_string_verbose(symbol, symbol.type);
   }
 
-  void detailed_conflict_report_rec(
+  /// Returns true iff the conflict report on a particular branch of the tree of
+  /// types was a definitive result, and not contingent on conflicts within a
+  /// tag type.
+  bool detailed_conflict_report_rec(
     const symbolt &old_symbol,
     const symbolt &new_symbol,
     const typet &type1,