diff --git a/regression/ansi-c/gcc_builtins6/main.c b/regression/ansi-c/gcc_builtins6/main.c
new file mode 100644
index 00000000000..706dd6196be
--- /dev/null
+++ b/regression/ansi-c/gcc_builtins6/main.c
@@ -0,0 +1,23 @@
+#include <stddef.h>
+
+struct S
+{
+  int x;
+  union {
+    int y;
+    struct S2
+    {
+      int z;
+    } s[1];
+  } u[2];
+};
+
+int main()
+{
+  int A[offsetof(struct S, u[0].y)==sizeof(int)?1:-1];
+#if defined(__GNUC__) && !defined(__clang__)
+  int B[offsetof(struct S, u->y)==sizeof(int)?1:-1];
+  int C[offsetof(struct S, u->s[0].z)==sizeof(int)?1:-1];
+#endif
+  return 0;
+}
diff --git a/regression/ansi-c/gcc_builtins6/test.desc b/regression/ansi-c/gcc_builtins6/test.desc
new file mode 100644
index 00000000000..466da18b2b5
--- /dev/null
+++ b/regression/ansi-c/gcc_builtins6/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/cbmc/Linking6/main.c b/regression/cbmc/Linking6/main.c
new file mode 100644
index 00000000000..ff1234d5cd4
--- /dev/null
+++ b/regression/cbmc/Linking6/main.c
@@ -0,0 +1,23 @@
+#include <stdio.h>
+
+void set();
+
+char buffer[10];
+
+void init() {
+  int i;
+  for (i = 0; i < 10; i++) {buffer[i] = 0;}
+}
+
+void print() {
+  printf("buffer = %s\n",buffer);
+}
+
+void main () {
+  init();
+  set();
+  print();
+}
+
+
+
diff --git a/regression/cbmc/Linking6/module.c b/regression/cbmc/Linking6/module.c
new file mode 100644
index 00000000000..a4353324f3d
--- /dev/null
+++ b/regression/cbmc/Linking6/module.c
@@ -0,0 +1,9 @@
+#include <stdlib.h>
+
+extern char buffer[];
+
+static size_t _debug_tempBufferHead = ((size_t)(&buffer));
+
+void set() {
+  *(char *)_debug_tempBufferHead = 'a';
+}
diff --git a/regression/cbmc/Linking6/test.desc b/regression/cbmc/Linking6/test.desc
new file mode 100644
index 00000000000..67f1dd7303f
--- /dev/null
+++ b/regression/cbmc/Linking6/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+module.c --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/constructor1/main.c b/regression/cbmc/constructor1/main.c
new file mode 100644
index 00000000000..868b7f4d268
--- /dev/null
+++ b/regression/cbmc/constructor1/main.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+#ifdef __GNUC__
+int x;
+
+static __attribute__((constructor)) void format_init(void);
+
+static __attribute__((constructor))
+void format_init(void)
+{
+  x=42;
+  return;
+}
+#endif
+
+int main()
+{
+#ifdef __GNUC__
+  assert(x==42);
+#endif
+  return 0;
+}
diff --git a/regression/cbmc/constructor1/test.desc b/regression/cbmc/constructor1/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/constructor1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/hex_string1/main.c b/regression/cbmc/hex_string1/main.c
new file mode 100644
index 00000000000..77b163df8b4
--- /dev/null
+++ b/regression/cbmc/hex_string1/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+#define static_assert(x) ((struct { char some[(x)?1:-1]; }*)0)
+
+int main()
+{
+  static_assert('\xe8'==(char)0xe8);
+  static_assert(sizeof("abc")==4);
+  static_assert(sizeof("\u0201")==3);
+  static_assert(sizeof("\xe8")==2);
+  static_assert(sizeof("\u0201\xe8")==4);
+
+  if("\xe8"[0]!=(char)0xe8)
+    assert(0);
+  return 0;
+}
diff --git a/regression/cbmc/hex_string1/test.desc b/regression/cbmc/hex_string1/test.desc
new file mode 100644
index 00000000000..12fc8ce06e1
--- /dev/null
+++ b/regression/cbmc/hex_string1/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 62ff07f127e..77debbb0ce9 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -272,6 +272,15 @@ void ansi_c_convert_typet::write(typet &type)
       throw 0;
     }
 
+    // asm blocks (cf. regression/ansi-c/asm1) - ignore the asm
+    if(other.size()==2)
+    {
+      if(other.front().id()==ID_asm && other.back().id()==ID_empty)
+        other.pop_front();
+      else if(other.front().id()==ID_empty && other.back().id()==ID_asm)
+        other.pop_back();
+    }
+
     if(other.size()!=1)
     {
       error().source_location=source_location;
diff --git a/src/ansi-c/c_storage_spec.h b/src/ansi-c/c_storage_spec.h
index d735e578426..81da615ebc7 100644
--- a/src/ansi-c/c_storage_spec.h
+++ b/src/ansi-c/c_storage_spec.h
@@ -76,7 +76,13 @@ class c_storage_spect
     is_register     |=other.is_register;
     is_inline       |=other.is_inline;
     is_thread_local |=other.is_thread_local;
-    // attributes belong to the declarator, don't replace them
+    is_weak         |=other.is_weak;
+    if(alias.empty())
+      alias=other.alias;
+    if(asm_label.empty())
+      asm_label=other.asm_label;
+    if(section.empty())
+      section=other.section;
 
     return *this;
   }
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index 8597eef3852..b170a11a67a 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -210,27 +210,6 @@ void c_typecheck_baset::typecheck_new_symbol(symbolt &symbol)
   }
   else
   {
-    if(symbol.type.id()==ID_array &&
-       to_array_type(symbol.type).size().is_nil() &&
-       !symbol.is_type)
-    {
-      // Insert a new type symbol for the array.
-      // We do this because we want a convenient way
-      // of adjusting the size of the type later on.
-
-      type_symbolt new_symbol(symbol.type);
-      new_symbol.name=id2string(symbol.name)+"$type";
-      new_symbol.base_name=id2string(symbol.base_name)+"$type";
-      new_symbol.location=symbol.location;
-      new_symbol.mode=symbol.mode;
-      new_symbol.module=symbol.module;
-
-      symbol.type=symbol_typet(new_symbol.name);
-
-      symbolt *new_sp;
-      symbol_table.move(new_symbol, new_sp);
-    }
-
     // check the initializer
     do_initializer(symbol);
   }
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index dfbac98940c..24ca6dbed3d 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -901,7 +901,9 @@ void c_typecheck_baset::typecheck_return(codet &code)
 {
   if(code.operands().empty())
   {
-    if(follow(return_type).id()!=ID_empty)
+    if(follow(return_type).id()!=ID_empty &&
+       return_type.id()!=ID_constructor &&
+       return_type.id()!=ID_destructor)
     {
       // gcc doesn't actually complain, it just warns!
       // We'll put a zero here, which is dubious.
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index d209b5a04fb..84bc81aac49 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -459,6 +459,11 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
           expr.id()==ID_gcc_asm_clobbered_register)
   {
   }
+  else if(expr.id()==ID_lshr || expr.id()==ID_ashr ||
+          expr.id()==ID_assign_lshr || expr.id()==ID_assign_ashr)
+  {
+    // already type checked
+  }
   else
   {
     err_location(expr);
diff --git a/src/ansi-c/gcc_builtin_headers_generic.h b/src/ansi-c/gcc_builtin_headers_generic.h
index 09c97df89a6..17d997b8deb 100644
--- a/src/ansi-c/gcc_builtin_headers_generic.h
+++ b/src/ansi-c/gcc_builtin_headers_generic.h
@@ -86,7 +86,7 @@ void __sync_lock_release();
 // other
 int __builtin_choose_expr(_Bool, ...);
 int __builtin_classify_type();
-int __builtin_constant_p();
+int __builtin_constant_p(int);
 void __builtin_trap(void);
 void __builtin_unreachable(void);
 
diff --git a/src/ansi-c/literals/convert_string_literal.cpp b/src/ansi-c/literals/convert_string_literal.cpp
index ebf166b222b..d47d907d0e1 100644
--- a/src/ansi-c/literals/convert_string_literal.cpp
+++ b/src/ansi-c/literals/convert_string_literal.cpp
@@ -47,7 +47,7 @@ std::basic_string<unsigned int> convert_one_string_literal(
 
     // pad into wide string
     value.resize(utf8_value.size());
-    for(unsigned i=0; i<utf8_value.size(); i++)
+    for(std::size_t i=0; i<utf8_value.size(); i++)
       value[i]=utf8_value[i];
 
     return value;
@@ -64,16 +64,14 @@ std::basic_string<unsigned int> convert_one_string_literal(
     assert(src[0]=='"');
     assert(src[src.size()-1]=='"');
 
-    std::basic_string<unsigned int> value=
-      unescape_wide_string(std::string(src, 1, src.size()-2));
-
-    // turn into utf-8
-    std::string utf8_value=utf32_to_utf8(value);
+    std::string char_value=
+      unescape_string(std::string(src, 1, src.size()-2));
 
     // pad into wide string
-    value.resize(utf8_value.size());
-    for(unsigned i=0; i<utf8_value.size(); i++)
-      value[i]=utf8_value[i];
+    std::basic_string<unsigned int> value;
+    value.resize(char_value.size());
+    for(std::size_t i=0; i<char_value.size(); i++)
+      value[i]=char_value[i];
 
     return value;
   }
@@ -101,7 +99,7 @@ exprt convert_string_literal(const std::string &src)
 
   char wide=0;
 
-  for(unsigned i=0; i<src.size(); i++)
+  for(std::size_t i=0; i<src.size(); i++)
   {
     char ch=src[i];
 
@@ -115,27 +113,24 @@ exprt convert_string_literal(const std::string &src)
       wide=ch;
 
     // find start of sequence
-    unsigned j=i;
-    while(j<src.size() && src[j]!='"') j++;
+    std::size_t j=src.find('"', i);
+    if(j==std::string::npos)
+      throw "invalid string constant `"+src+"'";
 
     // find end of sequence, considering escaping
-    j++;
-    while(j<src.size() && src[j]!='"')
-    {
-      if(src[j]=='\\')
-        j+=2;
-      else
-        j++;
-    }
-
-    if(j<src.size())
-    {
-      std::string tmp_src=std::string(src, i, j-i+1);
-      std::basic_string<unsigned int> tmp_value=
-        convert_one_string_literal(tmp_src);
-      value.append(tmp_value);
-      i=j;
-    }
+    for(++j; j<src.size() && src[j]!='"'; ++j)
+      if(src[j]=='\\') // skip next character
+        ++j;
+
+    assert(j<=src.size());
+    if(j==src.size())
+      throw "non-terminated string constant `"+src+"'";
+
+    std::string tmp_src=std::string(src, i, j-i+1);
+    std::basic_string<unsigned int> tmp_value=
+      convert_one_string_literal(tmp_src);
+    value.append(tmp_value);
+    i=j;
   }
 
   if(wide!=0)
@@ -161,7 +156,7 @@ exprt convert_string_literal(const std::string &src)
     result.type().set(ID_size, from_integer(value.size(), index_type()));
 
     result.operands().resize(value.size());
-    for(unsigned i=0; i<value.size(); i++)
+    for(std::size_t i=0; i<value.size(); i++)
       result.operands()[i]=from_integer(value[i], subtype);
 
     return result;
@@ -172,7 +167,7 @@ exprt convert_string_literal(const std::string &src)
 
     char_value.resize(value.size());
 
-    for(unsigned i=0; i<value.size(); i++)
+    for(std::size_t i=0; i<value.size(); i++)
     {
       // Loss of data here if value[i]>255.
       // gcc issues a warning in this case.
diff --git a/src/ansi-c/literals/unescape_string.cpp b/src/ansi-c/literals/unescape_string.cpp
index 6ecfadc703d..ab0232b9b3a 100644
--- a/src/ansi-c/literals/unescape_string.cpp
+++ b/src/ansi-c/literals/unescape_string.cpp
@@ -8,13 +8,14 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 #include <cctype>
-#include <cstdio>
+
+#include <util/unicode.h>
 
 #include "unescape_string.h"
 
 /*******************************************************************\
 
-Function: unescape_string
+Function: append_universal_char
 
   Inputs:
 
@@ -24,119 +25,40 @@ Function: unescape_string
 
 \*******************************************************************/
 
-std::string unescape_string(const std::string &src)
+static void append_universal_char(
+  unsigned int value,
+  std::string &dest)
 {
-  std::string dest;
-  dest.reserve(src.size());
-
-  for(unsigned i=0; i<src.size(); i++)
-  {
-    char ch=src[i];
-
-    if(ch=='\\') // escape?
-    {
-      // go to next character
-      i++;
-      assert(i<src.size()); // backslash can't be last character
-
-      ch=src[i];
-      switch(ch)
-      {
-      case '\\': dest+=ch; break;
-      case 'n': dest+='\n'; break; /* NL (0x0a) */
-      case 't': dest+='\t'; break; /* HT (0x09) */
-      case 'v': dest+='\v'; break; /* VT (0x0b) */
-      case 'b': dest+='\b'; break; /* BS (0x08) */
-      case 'r': dest+='\r'; break; /* CR (0x0d) */
-      case 'f': dest+='\f'; break; /* FF (0x0c) */
-      case 'a': dest+='\a'; break; /* BEL (0x07) */
-      case '"': dest+='"'; break;
-      case '\'': dest+='\''; break;
-
-      case 'u': // universal character
-      case 'U': // universal character
-        i++;
-
-        {
-          std::string hex;
+  std::basic_string<unsigned int> value_str(1, value);
 
-          const unsigned digits=(ch=='u')?4:8;
-          hex.reserve(digits);
-
-          for(unsigned count=digits;
-              count!=0 && i<src.size();
-              i++, count--)
-            hex+=src[i];
-
-          // go back
-          i--;
-
-          unsigned int result=hex_to_unsigned(hex.c_str(), hex.size());
+  // turn into utf-8
+  std::string utf8_value=utf32_to_utf8(value_str);
 
-          // Universal characters in non-wide strings don't
-          // really work; gcc just issues a warning.
-          ch=result;
-        }
-
-        dest+=ch;
-        break;
-
-      case 'x': // hex
-        i++;
-
-        {
-          std::string hex;
-
-          while(i<src.size() && isxdigit(src[i]))
-          {
-            hex+=src[i];
-            i++;
-          }
-
-          // go back
-          i--;
+  dest.append(utf8_value);
+}
 
-          ch=hex_to_unsigned(hex.c_str(), hex.size());
-        }
+/*******************************************************************\
 
-        dest+=ch;
-        break;
+Function: append_universal_char
 
-      default:
-        if(isdigit(ch)) // octal
-        {
-          std::string octal;
+  Inputs:
 
-          while(i<src.size() && isdigit(src[i]))
-          {
-            octal+=src[i];
-            i++;
-          }
+ Outputs:
 
-          // go back
-          i--;
+ Purpose:
 
-          ch=octal_to_unsigned(octal.c_str(), octal.size());
-          dest+=ch;
-        }
-        else
-        {
-          // Unknown escape sequence.
-          // Both GCC and CL turn \% into %.
-          dest.push_back(ch);
-        }
-      }
-    }
-    else
-      dest+=ch;
-  }
+\*******************************************************************/
 
-  return dest;
+static void append_universal_char(
+  unsigned int value,
+  std::basic_string<unsigned int> &dest)
+{
+  dest.push_back(value);
 }
 
 /*******************************************************************\
 
-Function: unescape_wide_string
+Function: unescape_string_templ
 
   Inputs:
 
@@ -146,19 +68,20 @@ Function: unescape_wide_string
 
 \*******************************************************************/
 
-std::basic_string<unsigned int> unescape_wide_string(
-  const std::string &src)
+template<typename T>
+std::basic_string<T> unescape_string_templ(const std::string &src)
 {
-  std::basic_string<unsigned int> dest;
+  std::basic_string<T> dest;
 
   dest.reserve(src.size()); // about that long, but may be shorter
 
   for(unsigned i=0; i<src.size(); i++)
   {
-    unsigned int ch=(unsigned char)src[i];
+    T ch=(unsigned char)src[i];
 
     if(ch=='\\') // escape?
     {
+      // go to next character
       i++;
       assert(i<src.size()); // backslash can't be last character
 
@@ -183,21 +106,22 @@ std::basic_string<unsigned int> unescape_wide_string(
         {
           std::string hex;
 
-          unsigned count=(ch=='u')?4:8;
-          hex.reserve(count);
+          const unsigned digits=(ch=='u')?4:8;
+          hex.reserve(digits);
 
-          for(; count!=0 && i<src.size(); i++, count--)
+          for(unsigned count=digits;
+              count!=0 && i<src.size();
+              i++, count--)
             hex+=src[i];
 
           // go back
           i--;
 
-          unsigned int result;
-          sscanf(hex.c_str(), "%x", &result);
-          ch=result;
+          unsigned int result=hex_to_unsigned(hex.c_str(), hex.size());
+
+          append_universal_char(result, dest);
         }
 
-        dest.push_back(ch);
         break;
 
       case 'x': // hex
@@ -205,6 +129,7 @@ std::basic_string<unsigned int> unescape_wide_string(
 
         {
           std::string hex;
+
           while(i<src.size() && isxdigit(src[i]))
           {
             hex+=src[i];
@@ -214,11 +139,13 @@ std::basic_string<unsigned int> unescape_wide_string(
           // go back
           i--;
 
-          unsigned int result;
-          sscanf(hex.c_str(), "%x", &result);
-          ch=result;
+          ch=hex_to_unsigned(hex.c_str(), hex.size());
         }
 
+        // if T isn't sufficiently wide to hold unsigned values
+        // the following might truncate; but then
+        // universal characters in non-wide strings don't
+        // really work; gcc just issues a warning.
         dest.push_back(ch);
         break;
 
@@ -236,9 +163,7 @@ std::basic_string<unsigned int> unescape_wide_string(
           // go back
           i--;
 
-          unsigned int result;
-          sscanf(octal.c_str(), "%o", &result);
-          ch=result;
+          ch=octal_to_unsigned(octal.c_str(), octal.size());
           dest.push_back(ch);
         }
         else
@@ -258,6 +183,41 @@ std::basic_string<unsigned int> unescape_wide_string(
 
 /*******************************************************************\
 
+Function: unescape_string
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::string unescape_string(const std::string &src)
+{
+  return unescape_string_templ<char>(src);
+}
+
+/*******************************************************************\
+
+Function: unescape_wide_string
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+std::basic_string<unsigned int> unescape_wide_string(
+  const std::string &src)
+{
+  return unescape_string_templ<unsigned int>(src);
+}
+
+/*******************************************************************\
+
 Function: hex_to_unsigned
 
   Inputs:
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 3529ef5cff0..0819265fe70 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -22,6 +22,8 @@ extern char *yyansi_ctext;
 
 #include "parser_static.inc"
 
+#include "literals/convert_integer_literal.h"
+
 #include "ansi_c_y.tab.h"
 
 // statements have right recursion, deep nesting of statements thus
@@ -425,6 +427,17 @@ offsetof_member_designator:
           mto($2, $3);
           mto($$, $2);
         }
+        | offsetof_member_designator TOK_ARROW member_name
+        {
+          $$=$1;
+          set($2, ID_index);
+          exprt tmp=convert_integer_literal("0");
+          stack($2).move_to_operands(tmp);
+          mto($$, $2);
+          set($2, ID_member);
+          stack($2).set(ID_component_name, stack($3).get(ID_C_base_name));
+          mto($$, $2);
+        }
         ;
           
 quantifier_expression:
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
index f375cd4dbf6..3df64f14da6 100644
--- a/src/cpp/cpp_typecheck_code.cpp
+++ b/src/cpp/cpp_typecheck_code.cpp
@@ -45,6 +45,10 @@ void cpp_typecheckt::typecheck_code(codet &code)
           statement==ID_msc_if_not_exists)
   {
   }
+  else if(statement==ID_decl_block)
+  {
+    // type checked already
+  }
   else
     c_typecheck_baset::typecheck_code(code);
 }
diff --git a/src/cpp/cpp_typecheck_type.cpp b/src/cpp/cpp_typecheck_type.cpp
index 3672acfc0d2..5151492be5c 100644
--- a/src/cpp/cpp_typecheck_type.cpp
+++ b/src/cpp/cpp_typecheck_type.cpp
@@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
 \*******************************************************************/
 
 #include <util/source_location.h>
+#include <util/simplify_expr.h>
 
 #include <ansi-c/c_qualifiers.h>
 
@@ -126,7 +127,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
     exprt &size_expr=to_array_type(type).size();
 
     if(size_expr.is_not_nil())
+    {
       typecheck_expr(size_expr);
+      simplify(size_expr, *this);
+    }
 
     typecheck_type(type.subtype());
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index ee48efee628..f8e17ec8736 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -335,7 +335,9 @@ void goto_convertt::do_scanf(
 
               copy(array_copy_statement, OTHER, dest);
               #else
-              exprt lhs=dereference_exprt(ptr, type.subtype());
+              exprt lhs=
+                index_exprt(
+                  dereference_exprt(ptr, type), from_integer(0, index_type()));
               exprt rhs=side_effect_expr_nondett(type.subtype());
               code_assignt assign(lhs, rhs);
               assign.add_source_location()=function.source_location();
@@ -1528,8 +1530,18 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    const irep_idt description=
-      "assertion "+id2string(get_string_constant(arguments[3]));
+    irep_idt description;
+    try
+    {
+      description="assertion "+id2string(get_string_constant(arguments[3]));
+    }
+    catch(int)
+    {
+      // we might be building newlib, where __assert_func is passed
+      // a pointer-typed symbol; the warning will still have been
+      // printed
+      description="assertion";
+    }
 
     goto_programt::targett t=dest.add_instruction(ASSERT);
     t->guard=false_exprt();
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index dba23c3039f..a00ccf0a452 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -215,17 +215,19 @@ void goto_convertt::finish_gotos(goto_programt &dest)
 
       if(!stack_is_prefix)
       {
-        warning() << "Encountered goto (" << goto_label <<
-          ") that enters one or more lexical blocks;" <<
-          "omitting constructors and destructors." << eom;
+          debug().source_location=i.code.find_source_location();
+          debug() << "encountered goto `" << goto_label
+                  << "' that enters one or more lexical blocks; "
+                  << "omitting constructors and destructors" << eom;
       }
       else
       {
         auto unwind_to_size=label_stack.size();
         if(unwind_to_size<goto_stack.size())
         {
-          status() << "Adding goto-destructor code on jump to " <<
-            goto_label << eom;
+          debug().source_location=i.code.find_source_location();
+          debug() << "adding goto-destructor code on jump to `"
+                  << goto_label << "'" << eom;
           goto_programt destructor_code;
           unwind_destructor_stack(
             i.code.add_source_location(),
diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp
index 8aaa4183da3..ccb227a7d9f 100644
--- a/src/goto-programs/read_goto_binary.cpp
+++ b/src/goto-programs/read_goto_binary.cpp
@@ -289,7 +289,8 @@ static bool link_functions(
   const symbol_tablet &src_symbol_table,
   goto_functionst &src_functions,
   const rename_symbolt &rename_symbol,
-  const std::unordered_set<irep_idt, irep_id_hash> &weak_symbols)
+  const std::unordered_set<irep_idt, irep_id_hash> &weak_symbols,
+  const replace_symbolt &object_type_updates)
 {
   namespacet ns(dest_symbol_table);
   namespacet src_ns(src_symbol_table);
@@ -381,6 +382,16 @@ static bool link_functions(
     Forall_goto_functions(dest_it, dest_functions)
       rename_symbols_in_function(dest_it->second, macro_application);
 
+  if(!object_type_updates.expr_map.empty())
+  {
+    Forall_goto_functions(dest_it, dest_functions)
+      Forall_goto_program_instructions(iit, dest_it->second.body)
+      {
+        object_type_updates(iit->code);
+        object_type_updates(iit->guard);
+      }
+  }
+
   return false;
 }
 
@@ -427,9 +438,14 @@ bool read_object_and_link(
   if(linking.typecheck_main())
     return true;
 
-  if(link_functions(symbol_table, functions,
-                    temp_model.symbol_table, temp_model.goto_functions,
-                    linking.rename_symbol, weak_symbols))
+  if(link_functions(
+      symbol_table,
+      functions,
+      temp_model.symbol_table,
+      temp_model.goto_functions,
+      linking.rename_symbol,
+      weak_symbols,
+      linking.object_type_updates))
     return true;
 
   return false;
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 173d5b2cf4c..46ed3fe4a23 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -593,10 +593,16 @@ void linkingt::duplicate_code_symbol(
     }
     // handle (incomplete) function prototypes
     else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
-            ((old_t.parameters().empty() && old_t.has_ellipsis()) ||
-             (new_t.parameters().empty() && new_t.has_ellipsis())))
+            ((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())
+      if(old_t.parameters().empty() &&
+         old_t.has_ellipsis() &&
+         old_symbol.value.is_nil())
       {
         old_symbol.type=new_symbol.type;
         old_symbol.location=new_symbol.location;
@@ -830,6 +836,7 @@ void linkingt::duplicate_code_symbol(
       old_symbol.value=new_symbol.value;
       old_symbol.type=new_symbol.type; // for parameter identifiers
       old_symbol.is_weak=new_symbol.is_weak;
+      old_symbol.location=new_symbol.location;
       old_symbol.is_macro=new_symbol.is_macro;
     }
     else if(to_code_type(old_symbol.type).get_inlined())
@@ -1093,6 +1100,8 @@ void linkingt::duplicate_object_symbol(
     }
     else if(set_to_new)
       old_symbol.type=new_symbol.type;
+
+    object_type_updates.insert(old_symbol.name, old_symbol.symbol_expr());
   }
 
   // care about initializers
@@ -1501,6 +1510,15 @@ void linkingt::copy_symbols()
     else
       duplicate_non_type_symbol(old_symbol, new_symbol);
   }
+
+  // Apply type updates to initializers
+  Forall_symbols(s_it, main_symbol_table.symbols)
+  {
+    if(!s_it->second.is_type &&
+       !s_it->second.is_macro &&
+       s_it->second.value.is_not_nil())
+      object_type_updates(s_it->second.value);
+  }
 }
 
 /*******************************************************************\
diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h
index dba9481f3ab..9cc410c9fbc 100644
--- a/src/linking/linking_class.h
+++ b/src/linking/linking_class.h
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/namespace.h>
 #include <util/rename_symbol.h>
+#include <util/replace_symbol.h>
 #include <util/typecheck.h>
 #include <util/std_expr.h>
 
@@ -31,6 +32,7 @@ class linkingt:public typecheckt
   virtual void typecheck();
 
   rename_symbolt rename_symbol;
+  replace_symbolt object_type_updates;
 
 protected:
   typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index 507df13bac3..266a88fd13f 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -156,7 +156,6 @@ bool static_lifetime_init(
 
   // call designated "initialization" functions
 
-  #if 0
   for(const std::string &id : symbols)
   {
     const symbolt &symbol=ns.lookup(id);
@@ -170,7 +169,6 @@ bool static_lifetime_init(
       dest.move_to_operands(function_call);
     }
   }
-  #endif
 
   return false;
 }