Linking: replace conflicting pointer types when one declaration is extern

Author: tautschnig

regression/cbmc/Linking8/a.c

@@ -0,0 +1,11 @@
+#include <stdlib.h>
+
+void foo();
+
+int main()
+{
+  extern void *p;
+  p = malloc(sizeof(int));
+  foo();
+  return 0;
+}

regression/cbmc/Linking8/b.c

@@ -0,0 +1,6 @@
+int *p;
+
+void foo()
+{
+  *p = 42;
+}

regression/cbmc/Linking8/test.desc

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

src/ansi-c/c_typecheck_base.cpp

@@ -67,6 +67,15 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
     // and have static lifetime
     new_name=root_name;
     symbol.is_static_lifetime=true;
+
+    if(symbol.value.is_not_nil())
+    {
+      // According to the C standard this should be an error, but at least some
+      // versions of Visual Studio insist to use this in their C library, and
+      // GCC just warns as well.
+      warning().source_location = symbol.value.find_source_location();
+      warning() << "`extern' symbol should not have an initializer" << eom;
+    }
   }
   else if(!is_function && symbol.value.id()==ID_code)
   {

src/goto-symex/symex_dereference.cpp

@@ -216,6 +216,23 @@ exprt goto_symext::address_arithmetic(
     else
       result=address_of_exprt(result);
   }
+  else if(expr.id() == ID_typecast)
+  {
+    const typecast_exprt &tc_expr = to_typecast_expr(expr);
+
+    result = address_arithmetic(tc_expr.op(), state, guard, keep_array);
+
+    // treat &array as &array[0]
+    const typet &expr_type = ns.follow(expr.type());
+    typet dest_type_subtype;
+
+    if(expr_type.id() == ID_array && !keep_array)
+      dest_type_subtype = expr_type.subtype();
+    else
+      dest_type_subtype = expr_type;
+
+    result = typecast_exprt(result, pointer_type(dest_type_subtype));
+  }
   else
     throw unsupported_operation_exceptiont(
       "goto_symext::address_arithmetic does not handle " + expr.id_string());

src/linking/linking.cpp

@@ -24,6 +24,21 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "linking_class.h"
 
+bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
+{
+  expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
+
+  if(it == expr_map.end())
+    return true;
+
+  const exprt &e = it->second;
+
+  typet type = s.type();
+  static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
+
+  return false;
+}
+
 std::string linkingt::expr_to_string(
   const namespacet &ns,
   const irep_idt &identifier,
@@ -864,6 +879,11 @@ bool linkingt::adjust_object_type_rec(
       "conflicting pointer types for variable");
     #endif
 
+    if(info.old_symbol.is_extern && !info.new_symbol.is_extern)
+    {
+      info.set_to_new = true; // store new type
+    }
+
     return false;
   }
   else if(t1.id()==ID_array &&
@@ -950,10 +970,10 @@ void linkingt::duplicate_object_symbol(
   symbolt &new_symbol)
 {
   // both are variables
+  bool set_to_new = false;
 
   if(!base_type_eq(old_symbol.type, new_symbol.type, ns))
   {
-    bool set_to_new=false;
     bool failed=
       adjust_object_type(old_symbol, new_symbol, set_to_new);
 
@@ -1033,6 +1053,14 @@ void linkingt::duplicate_object_symbol(
       }
     }
   }
+  else if(
+    set_to_new && !old_symbol.value.is_nil() &&
+    !old_symbol.value.get_bool(ID_C_zero_initializer))
+  {
+    // the type has been updated, now make sure that the initialising assignment
+    // will have matching types
+    old_symbol.value.make_typecast(old_symbol.type);
+  }
 }
 
 void linkingt::duplicate_non_type_symbol(

src/linking/linking_class.h

@@ -18,6 +18,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/typecheck.h>
 #include <util/std_expr.h>
 
+class casting_replace_symbolt : public replace_symbolt
+{
+private:
+  bool replace_symbol_expr(symbol_exprt &dest) const override;
+};
+
 class linkingt:public typecheckt
 {
 public:
@@ -35,7 +41,7 @@ class linkingt:public typecheckt
   virtual void typecheck();
 
   rename_symbolt rename_symbol;
-  unchecked_replace_symbolt object_type_updates;
+  casting_replace_symbolt object_type_updates;
 
 protected:
   bool needs_renaming_type(