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,23 @@ 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
+      if(config.ansi_c.mode == configt::ansi_ct::flavourt::VISUAL_STUDIO)
+      {
+        warning().source_location = symbol.value.find_source_location();
+        warning() << "`extern' symbol should not have an initializer" << eom;
+      }
+      else
+      {
+        error().source_location = symbol.value.find_source_location();
+        error() << "`extern' symbol should not have an initializer" << eom;
+        throw 0;
+      }
+    }
   }
   else if(!is_function && symbol.value.id()==ID_code)
   {

src/goto-instrument/dump_c.cpp

@@ -958,7 +958,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

@@ -214,6 +214,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 "goto_symext::address_arithmetic does not handle "+expr.id_string();
 

src/linking/linking.cpp

@@ -875,6 +875,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 &&
@@ -961,10 +966,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);
 
@@ -1043,6 +1048,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/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
 
@@ -49,14 +50,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()))
@@ -66,7 +69,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)
@@ -83,15 +86,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;