Linking: actually replace code type information in expressions

The linker already accepted a number of type mismatches for function
declarations, but did not actually modify the goto functions to reflect these
type mismatches, just the type information in the symbol table was updated.

Author: tautschnig

regression/ansi-c/undeclared_function/undeclared_function1.desc

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

src/goto-programs/link_goto_model.cpp

@@ -58,7 +58,8 @@ static bool link_functions(
   goto_functionst &src_functions,
   const rename_symbolt &rename_symbol,
   const std::unordered_set<irep_idt> &weak_symbols,
-  const replace_symbolt &object_type_updates)
+  const replace_symbolt &object_type_updates,
+  const replace_symbolt &code_type_updates)
 {
   namespacet ns(dest_symbol_table);
   namespacet src_ns(src_symbol_table);
@@ -165,6 +166,19 @@ static bool link_functions(
       }
   }
 
+  if(!code_type_updates.empty())
+  {
+    // std::cerr << code_type_updates.get_expr_map().begin()->second.pretty() << std::endl;
+    Forall_goto_functions(dest_it, dest_functions)
+      Forall_goto_program_instructions(iit, dest_it->second.body)
+      {
+        code_type_updates(iit->code);
+
+        if(iit->has_condition())
+          code_type_updates(iit->guard);
+      }
+  }
+
   return false;
 }
 
@@ -196,7 +210,8 @@ void link_goto_model(
        src.goto_functions,
        linking.rename_symbol,
        weak_symbols,
-       linking.object_type_updates))
+       linking.object_type_updates,
+       linking.code_type_updates))
   {
     throw invalid_source_file_exceptiont("linking failed");
   }

src/linking/linking.cpp

@@ -743,6 +743,12 @@ void linkingt::duplicate_code_symbol(
         }
       }
     }
+
+    if(old_symbol.type == new_symbol.type)
+    {
+      code_type_updates.insert(
+        old_symbol.symbol_expr(), old_symbol.symbol_expr());
+    }
   }
 
   if(!new_symbol.value.is_nil())
@@ -757,6 +763,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
+      code_type_updates.erase(old_symbol.name);
+      code_type_updates.insert(
+        old_symbol.symbol_expr(), old_symbol.symbol_expr());
     }
     else if(to_code_type(old_symbol.type).get_inlined())
     {
@@ -1385,6 +1396,8 @@ void linkingt::copy_symbols()
     {
       object_type_updates(
         main_symbol_table.get_writeable_ref(named_symbol.first).value);
+      code_type_updates(
+        main_symbol_table.get_writeable_ref(named_symbol.first).value);
     }
   }
 }

src/linking/linking_class.h

@@ -42,6 +42,7 @@ class linkingt:public typecheckt
 
   rename_symbolt rename_symbol;
   casting_replace_symbolt object_type_updates;
+  unchecked_replace_symbolt code_type_updates;
 
 protected:
   bool needs_renaming_type(