Linking: replace conflicting pointer types when one declaration is extern

Author: tautschnig

regression/cbmc/Linking7/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/Linking7/b.c

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

regression/cbmc/Linking7/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,13 @@ 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())
+    {
+      error().source_location=symbol.value.find_source_location();
+      error() << "extern symbols cannot have an initializer" << eom;
+      throw 0;
+    }
   }
   else if(!is_function && symbol.value.id()==ID_code)
   {

src/goto-instrument/dump_c.cpp

@@ -962,7 +962,7 @@ void dump_ct::cleanup_harness(code_blockt &b)
   }
 
   b.swap(decls);
-  replace(b);
+  replace.replace(b, true, true);
 }
 
 void dump_ct::convert_function_declaration(

src/goto-instrument/model_argc_argv.cpp

@@ -128,7 +128,7 @@ bool model_argc_argv(
       replace_symbolt replace;
       replace.insert("ARGC", ns.lookup("argc'").symbol_expr());
       replace.insert("ARGV", ns.lookup("argv'").symbol_expr());
-      replace(value);
+      replace.replace(value, true, true);
     }
     else if(
       has_prefix(

src/goto-symex/symex_dereference.cpp

@@ -218,6 +218,24 @@ exprt goto_symext::address_arithmetic(
     else
       result=address_of_exprt(result);
   }
+  else if(expr.id()==ID_typecast)
+  {
+    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 "goto_symext::address_arithmetic does not handle "+expr.id_string();
 

src/linking/linking.cpp

@@ -850,6 +850,9 @@ 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 &&

src/util/replace_symbol.cpp

@@ -29,7 +29,8 @@ void replace_symbolt::insert(
 
 bool replace_symbolt::replace(
   exprt &dest,
-  const bool replace_with_const) const
+  const bool replace_with_const,
+  const bool ignore_type_change) const
 {
   bool result=true; // unchanged
 
@@ -48,14 +49,16 @@ bool replace_symbolt::replace(
   {
     member_exprt &me=to_member_expr(dest);
 
-    if(!replace(me.struct_op(), replace_with_const)) // Could give non l-value.
+    // Could yield non l-value.
+    if(!replace(me.struct_op(), replace_with_const, ignore_type_change))
       result=false;
   }
   else if(dest.id()==ID_index)
   {
     index_exprt &ie=to_index_expr(dest);
 
-    if(!replace(ie.array(), replace_with_const)) // Could give non l-value.
+    // Could yield non l-value.
+    if(!replace(ie.array(), replace_with_const, ignore_type_change))
       result=false;
 
     if(!replace(ie.index()))
@@ -65,7 +68,7 @@ bool replace_symbolt::replace(
   {
     address_of_exprt &aoe=to_address_of_expr(dest);
 
-    if(!replace(aoe.object(), false))
+    if(!replace(aoe.object(), false, ignore_type_change))
       result=false;
   }
   else if(dest.id()==ID_symbol)
@@ -82,15 +85,22 @@ bool replace_symbolt::replace(
       if(!replace_with_const && e.is_constant())  // Would give non l-value.
         return true;
 
-      dest=e;
+      if(ignore_type_change || dest.type()==e.type())
+        dest=e;
+      else
+      {
+        typet type=dest.type();
+        dest=e;
+        dest.make_typecast(type);
+      }
 
       return false;
     }
   }
   else
   {
     Forall_operands(it, dest)
-      if(!replace(*it))
+      if(!replace(*it, true, ignore_type_change))
         result=false;
   }
 

src/util/replace_symbol.h

@@ -51,10 +51,13 @@ class replace_symbolt
   /// \param dest The expression in which to do the replacement
   /// \param replace_with_const If false then it disables the rewrites that
   /// could result in something that is not an l-value.
+  /// \param ignore_type_change If true, do not introduce type casts when the
+  /// replacement would cause expression types to change.
   ///
   virtual bool replace(
     exprt &dest,
-    const bool replace_with_const=true) const;
+    const bool replace_with_const=true,
+    const bool ignore_type_change=false) const;
 
   virtual bool replace(typet &dest) const;