diff --git a/CHANGELOG b/CHANGELOG
index 44ac745be0d..e497b1cadc2 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -8,6 +8,8 @@
 * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
 * GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
 * GOTO-INSTRUMENT: New option --remove-function-body
+* GOTO-INSTRUMENT: New option --use-all-headers, changed --use-system-headers to
+  --no-system-headers
 
 
 5.7
diff --git a/regression/goto-instrument/dump-vararg1/main.c b/regression/goto-instrument/dump-vararg1/main.c
new file mode 100644
index 00000000000..9ce2bce8d03
--- /dev/null
+++ b/regression/goto-instrument/dump-vararg1/main.c
@@ -0,0 +1,19 @@
+#include<stdarg.h>
+#include<stdlib.h>
+
+void bb_verror_msg(const char *s, va_list p, const char *strerr) {
+}
+
+void bb_error_msg(const char *s, ...)
+{
+    va_list p;
+    va_start(p, s);
+    bb_verror_msg(s, p, NULL);
+    va_end(p);
+}
+
+int main() {
+    bb_error_msg("FOOO");
+    return 0;
+}
+
diff --git a/regression/goto-instrument/dump-vararg1/test.desc b/regression/goto-instrument/dump-vararg1/test.desc
new file mode 100644
index 00000000000..d1a6d2f2d6f
--- /dev/null
+++ b/regression/goto-instrument/dump-vararg1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+va_list
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/typedef1/main.c b/regression/goto-instrument/typedef1/main.c
new file mode 100644
index 00000000000..8c80dc61e34
--- /dev/null
+++ b/regression/goto-instrument/typedef1/main.c
@@ -0,0 +1,69 @@
+typedef long int off_t;
+typedef signed char smallint;
+
+typedef struct chain_s {
+  struct node_s *first;
+  struct node_s *last;
+  const char *programname;
+} chain;
+
+typedef struct func_s {
+    struct chain_s body;
+} func;
+
+typedef struct node_s {
+  struct node_s *n;
+} node;
+
+typedef struct dumper_t_x {
+  node n;
+  off_t dump_skip;
+  signed int dump_length;
+  smallint dump_vflag;
+} dumper_t;
+
+typedef struct FS_x {
+  struct FS *nextfs;
+  signed int bcnt;
+} FS;
+
+dumper_t * alloc_dumper(void) {
+  return (void*) 0;
+}
+
+typedef unsigned int uint32_t;
+
+const uint32_t xx[2];
+
+typedef struct node_s2 {
+  uint32_t info;
+} node2;
+
+typedef struct {
+  int x;
+} anon_name;
+
+typedef struct node_s3 {
+  union {
+    struct node_s *n;
+    func *f;
+  } r;
+} node3;
+
+typedef int x_int;
+typedef int y_int;
+typedef x_int *p_int;
+
+int main() {
+  node n;
+  chain c;
+  dumper_t a;
+  dumper_t b[3];
+  node2* sn;
+  anon_name d;
+  node3* s3;
+  y_int y;
+  p_int p;
+  alloc_dumper();
+  return 0;
+}
diff --git a/regression/goto-instrument/typedef1/test.desc b/regression/goto-instrument/typedef1/test.desc
new file mode 100644
index 00000000000..8047eddf32b
--- /dev/null
+++ b/regression/goto-instrument/typedef1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test should be run via chain.sh, which will try to recompile the dumped C
+code. Missing/incomplete typedef output would cause a failure.
diff --git a/regression/goto-instrument/typedef2/main.c b/regression/goto-instrument/typedef2/main.c
new file mode 100644
index 00000000000..928abcfde9a
--- /dev/null
+++ b/regression/goto-instrument/typedef2/main.c
@@ -0,0 +1,16 @@
+typedef struct
+{
+	char bogus;
+} bb_mbstate_t;
+
+int bb_wcrtomb(char *s, char wc, bb_mbstate_t *ps);
+
+int bb_wcrtomb(char *s, char wc, bb_mbstate_t *ps)
+{
+	return 1;
+}
+
+int main() {
+	bb_wcrtomb("foo", 'Z', (void*)1);
+	return 0;
+}
diff --git a/regression/goto-instrument/typedef2/test.desc b/regression/goto-instrument/typedef2/test.desc
new file mode 100644
index 00000000000..8047eddf32b
--- /dev/null
+++ b/regression/goto-instrument/typedef2/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test should be run via chain.sh, which will try to recompile the dumped C
+code. Missing/incomplete typedef output would cause a failure.
diff --git a/regression/goto-instrument/typedef3/main.c b/regression/goto-instrument/typedef3/main.c
new file mode 100644
index 00000000000..4ca41b69451
--- /dev/null
+++ b/regression/goto-instrument/typedef3/main.c
@@ -0,0 +1,30 @@
+extern void* memset(void *, int, unsigned long);
+
+typedef void (*__sighandler_t) (int);
+
+typedef __sighandler_t sighandler_t;
+
+typedef struct siginfo {
+  int si_signo;
+} siginfo_t;
+
+struct sigaction {
+  union {
+    __sighandler_t _sa_handler;
+    void (*_sa_sigaction)(int, struct siginfo *, void *);
+  } _u;
+};
+
+#define sa_sigaction  _u._sa_sigaction
+#define sa_handler  _u._sa_handler
+
+static void askpass_timeout(signed int ignore) {
+  ;
+}
+
+int main() {
+  struct sigaction sa, oldsa;
+  memset(&sa, 0, sizeof(sa));
+  sa.sa_handler = askpass_timeout;
+  return 0;
+}
diff --git a/regression/goto-instrument/typedef3/test.desc b/regression/goto-instrument/typedef3/test.desc
new file mode 100644
index 00000000000..8047eddf32b
--- /dev/null
+++ b/regression/goto-instrument/typedef3/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test should be run via chain.sh, which will try to recompile the dumped C
+code. Missing/incomplete typedef output would cause a failure.
diff --git a/regression/goto-instrument/typedef4/main.c b/regression/goto-instrument/typedef4/main.c
new file mode 100644
index 00000000000..7290f9c9ba5
--- /dev/null
+++ b/regression/goto-instrument/typedef4/main.c
@@ -0,0 +1,23 @@
+#ifndef _WIN32
+
+#include <signal.h>
+#include <stdlib.h>
+
+void sig_block(int sig)
+{
+  sigset_t ss;
+  sigemptyset(&ss);
+  sigaddset(&ss, sig);
+  sigprocmask(SIG_BLOCK, &ss, NULL);
+}
+
+int main() {
+  sig_block(0);
+  return 0;
+}
+#else
+int main()
+{
+  return 0;
+}
+#endif
diff --git a/regression/goto-instrument/typedef4/test.desc b/regression/goto-instrument/typedef4/test.desc
new file mode 100644
index 00000000000..8047eddf32b
--- /dev/null
+++ b/regression/goto-instrument/typedef4/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--dump-c
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test should be run via chain.sh, which will try to recompile the dumped C
+code. Missing/incomplete typedef output would cause a failure.
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index dc0c469b64c..73a9f5cff09 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -558,6 +558,14 @@ std::string expr2ct::convert_rec(
 
     c_qualifierst ret_qualifiers;
     ret_qualifiers.read(code_type.return_type());
+    // _Noreturn should go with the return type
+    if(new_qualifiers.is_noreturn)
+    {
+      ret_qualifiers.is_noreturn=true;
+      new_qualifiers.is_noreturn=false;
+      q=new_qualifiers.as_string();
+    }
+
     const typet &return_type=code_type.return_type();
 
     // return type may be a function pointer or array
@@ -1833,10 +1841,12 @@ std::string expr2ct::convert_constant(
 
     if(dest!="" && isdigit(dest[dest.size()-1]))
     {
+      if(dest.find('.')==std::string::npos)
+        dest+=".0";
+
+      // ANSI-C: double is default; float/long-double require annotation
       if(src.type()==float_type())
         dest+='f';
-      else if(src.type()==double_type())
-        dest+=""; // ANSI-C: double is default
       else if(src.type()==long_double_type())
         dest+='l';
     }
@@ -3522,7 +3532,11 @@ std::string expr2ct::convert_with_precedence(
     return convert_function(src, "isinf", precedence=16);
 
   else if(src.id()==ID_bswap)
-    return convert_function(src, "bswap", precedence=16);
+    return convert_function(
+      src,
+      "__builtin_bswap"+
+      integer2string(pointer_offset_bits(src.op0().type(), ns)),
+      precedence=16);
 
   else if(src.id()==ID_isnormal)
     return convert_function(src, "isnormal", precedence=16);
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
index 3026dc3e6aa..6537445e88b 100644
--- a/src/clobber/clobber_parse_options.cpp
+++ b/src/clobber/clobber_parse_options.cpp
@@ -146,7 +146,7 @@ int clobber_parse_optionst::doit()
     if(!out)
       throw std::string("failed to create file simulator.c");
 
-    dump_c(goto_functions, true, ns, out);
+    dump_c(goto_functions, true, false, ns, out);
 
     status() << "instrumentation complete; compile and execute simulator.c"
              << eom;
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index f9184b86598..27a680a3901 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -714,6 +714,7 @@ void compilet::convert_symbols(goto_functionst &dest)
 
       if(s_it->second.type.id()==ID_code &&
          !s_it->second.is_macro &&
+         !s_it->second.is_type &&
           s_it->second.value.id()!="compiled" &&
           s_it->second.value.is_not_nil())
       {
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 443b2a79413..fa9ebf63359 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <cctype>
 
 #include <util/config.h>
+#include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/suffix.h>
 #include <util/find_symbols.h>
@@ -38,6 +39,7 @@ void dump_ct::operator()(std::ostream &os)
   std::stringstream func_decl_stream;
   std::stringstream compound_body_stream;
   std::stringstream global_var_stream;
+  std::stringstream global_decl_stream;
   std::stringstream func_body_stream;
   local_static_declst local_static_decls;
 
@@ -92,17 +94,20 @@ void dump_ct::operator()(std::ostream &os)
     symbolt &symbol=it->second;
     bool tag_added=false;
 
+    // TODO we could get rid of some of the ID_anonymous by looking up
+    // the origin symbol types in typedef_types and adjusting any other
+    // uses of ID_tag
     if((symbol.type.id()==ID_union || symbol.type.id()==ID_struct) &&
        symbol.type.get(ID_tag).empty())
     {
-      assert(symbol.is_type);
+      PRECONDITION(symbol.is_type);
       symbol.type.set(ID_tag, ID_anonymous);
       tag_added=true;
     }
     else if(symbol.type.id()==ID_c_enum &&
             symbol.type.find(ID_tag).get(ID_C_base_name).empty())
     {
-      assert(symbol.is_type);
+      PRECONDITION(symbol.is_type);
       symbol.type.add(ID_tag).set(ID_C_base_name, ID_anonymous);
       tag_added=true;
     }
@@ -141,14 +146,17 @@ void dump_ct::operator()(std::ostream &os)
         symbol.type.set(ID_tag, new_tag);
     }
 
-    // we don't want to dump in full all definitions
-    if(!tag_added && ignore(symbol))
+    // we don't want to dump in full all definitions; in particular
+    // do not dump anonymous types that are defined in system headers
+    if((!tag_added || symbol.is_type) && ignore(symbol))
       continue;
 
-    if(!symbols_sorted.insert(name_str).second)
-      assert(false);
+    bool inserted=symbols_sorted.insert(name_str).second;
+    CHECK_RETURN(inserted);
   }
 
+  gather_global_typedefs();
+
   // collect all declarations we might need, include local static variables
   bool skip_function_main=false;
   for(std::set<std::string>::const_iterator
@@ -167,13 +175,17 @@ void dump_ct::operator()(std::ostream &os)
         type_id==ID_incomplete_union ||
         type_id==ID_c_enum))
     {
-      os << "// " << symbol.name << '\n';
-      os << "// " << symbol.location << '\n';
-
-      if(type_id==ID_c_enum)
-        convert_compound_enum(symbol.type, os);
-      else
-        os << type_to_string(symbol_typet(symbol.name)) << ";\n\n";
+      if(!ignore(symbol))
+      {
+        global_decl_stream << "// " << symbol.name << '\n';
+        global_decl_stream << "// " << symbol.location << '\n';
+
+        if(type_id==ID_c_enum)
+          convert_compound_enum(symbol.type, global_decl_stream);
+        else
+          global_decl_stream << type_to_string(symbol_typet(symbol.name))
+                             << ";\n\n";
+      }
     }
     else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
       convert_global_variable(
@@ -201,7 +213,8 @@ void dump_ct::operator()(std::ostream &os)
   {
     const symbolt &symbol=ns.lookup(*it);
 
-    if(symbol.type.id()!=ID_code)
+    if(symbol.type.id()!=ID_code ||
+       symbol.is_type)
       continue;
 
     convert_function_declaration(
@@ -230,6 +243,8 @@ void dump_ct::operator()(std::ostream &os)
           compound_body_stream);
   }
 
+  // Dump the code to the target stream;
+  // the statements before to this point collect the code to dump!
   for(std::set<std::string>::const_iterator
       it=system_headers.begin();
       it!=system_headers.end();
@@ -261,6 +276,11 @@ void dump_ct::operator()(std::ostream &os)
        << "#endif\n\n";
   }
 
+  if(!global_decl_stream.str().empty())
+    os << global_decl_stream.str() << '\n';
+
+  dump_typedefs(os);
+
   if(!func_decl_stream.str().empty())
     os << func_decl_stream.str() << '\n';
   if(!compound_body_stream.str().empty())
@@ -295,7 +315,7 @@ void dump_ct::convert_compound(
   {
     const symbolt &symbol=
       ns.lookup(to_symbol_type(type).get_identifier());
-    assert(symbol.is_type);
+    DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
 
     if(!ignore(symbol))
       convert_compound(symbol.type, unresolved, recursive, os);
@@ -304,7 +324,7 @@ void dump_ct::convert_compound(
   {
     const symbolt &symbol=
       ns.lookup(to_c_enum_tag_type(type).get_identifier());
-    assert(symbol.is_type);
+    DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
 
     if(!ignore(symbol))
       convert_compound(symbol.type, unresolved, recursive, os);
@@ -349,11 +369,14 @@ void dump_ct::convert_compound(
   if(!converted_compound.insert(name).second)
     return;
 
+  // make sure typedef names used in the declaration are available
+  collect_typedefs(type, true);
+
   const irept &bases = type.find(ID_bases);
   std::stringstream base_decls;
   forall_irep(parent_it, bases.get_sub())
   {
-    assert(false);
+    UNREACHABLE;
     /*
     assert(parent_it->id() == ID_base);
     assert(parent_it->get(ID_type) == ID_symbol);
@@ -407,8 +430,13 @@ void dump_ct::convert_compound(
     while(non_array_type->id()==ID_array)
       non_array_type=&(ns.follow(non_array_type->subtype()));
 
-    if(recursive && non_array_type->id()!=ID_pointer)
-      convert_compound(comp.type(), comp.type(), recursive, os);
+    if(recursive)
+    {
+      if(non_array_type->id()!=ID_pointer)
+        convert_compound(comp.type(), comp.type(), recursive, os);
+      else
+        collect_typedefs(comp.type(), true);
+    }
 
     irep_idt comp_name=comp.get_name();
 
@@ -419,7 +447,7 @@ void dump_ct::convert_compound(
     // namespace
     std::string fake_unique_name="NO/SUCH/NS::"+id2string(comp_name);
     std::string s=make_decl(fake_unique_name, comp.type());
-    assert(s.find("NO/SUCH/NS")==std::string::npos);
+    POSTCONDITION(s.find("NO/SUCH/NS")==std::string::npos);
 
     if(comp_type.id()==ID_c_bit_field &&
        to_c_bit_field_type(comp_type).get_width()==0)
@@ -457,15 +485,31 @@ void dump_ct::convert_compound(
         struct_body << s;
     }
     else
-      assert(false);
+      UNREACHABLE;
 
     struct_body << ";\n";
   }
 
-  os << type_to_string(unresolved);
+  typet unresolved_clean=unresolved;
+  typedef_typest::const_iterator td_entry=
+    typedef_types.find(unresolved);
+  irep_idt typedef_str;
+  if(td_entry!=typedef_types.end())
+  {
+    unresolved_clean.remove(ID_C_typedef);
+    typedef_str=td_entry->second;
+    std::pair<typedef_mapt::iterator, bool> td_map_entry=
+      typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
+    PRECONDITION(!td_map_entry.second);
+    if(!td_map_entry.first->second.early)
+      td_map_entry.first->second.type_decl_str="";
+    os << "typedef ";
+  }
+
+  os << type_to_string(unresolved_clean);
   if(!base_decls.str().empty())
   {
-    assert(language->id()=="cpp");
+    PRECONDITION(language->id()=="cpp");
     os << ": " << base_decls.str();
   }
   os << '\n';
@@ -489,14 +533,16 @@ void dump_ct::convert_compound(
     os << " __attribute__ ((__transparent_union__))";
   if(type.get_bool(ID_C_packed))
     os << " __attribute__ ((__packed__))";
-  os << ";\n";
+  if(!typedef_str.empty())
+    os << " " << typedef_str;
+  os << ";\n\n";
 }
 
 void dump_ct::convert_compound_enum(
   const typet &type,
   std::ostream &os)
 {
-  assert(type.id()==ID_c_enum);
+  PRECONDITION(type.id()==ID_c_enum);
 
   const irept &tag=type.find(ID_tag);
   const irep_idt &name=tag.get(ID_C_base_name);
@@ -597,7 +643,10 @@ void dump_ct::init_system_library_map()
     "pthread_rwlock_unlock", "pthread_rwlock_wrlock",
     "pthread_rwlockattr_destroy", "pthread_rwlockattr_getpshared",
     "pthread_rwlockattr_init", "pthread_rwlockattr_setpshared",
-    "pthread_self", "pthread_setspecific"
+    "pthread_self", "pthread_setspecific",
+    /* non-public struct types */
+    "tag-__pthread_internal_list", "tag-__pthread_mutex_s",
+    "pthread_mutex_t"
   };
   ADD_TO_SYSTEM_LIBRARY(pthread_syms, "pthread.h");
 
@@ -622,7 +671,7 @@ void dump_ct::init_system_library_map()
     "mkstemp", "mktemp", "perror", "printf", "putc", "putchar",
     "puts", "putw", "putwc", "putwchar", "remove", "rewind", "scanf",
     "setbuf", "setbuffer", "setlinebuf", "setvbuf", "snprintf",
-    "sprintf", "sscanf", "strerror", "swprintf", "sys_errlist",
+    "sprintf", "sscanf", "swprintf", "sys_errlist",
     "sys_nerr", "tempnam", "tmpfile", "tmpnam", "ungetc", "ungetwc",
     "vasprintf", "vfprintf", "vfscanf", "vfwprintf", "vprintf",
     "vscanf", "vsnprintf", "vsprintf", "vsscanf", "vswprintf",
@@ -658,9 +707,9 @@ void dump_ct::init_system_library_map()
   const char* time_syms[]=
   {
     "asctime", "asctime_r", "ctime", "ctime_r", "difftime", "gmtime",
-    "gmtime_r", "localtime", "localtime_r", "mktime",
+    "gmtime_r", "localtime", "localtime_r", "mktime", "strftime",
     /* non-public struct types */
-    "tag-timespec", "tag-timeval"
+    "tag-timespec", "tag-timeval", "tag-tm"
   };
   ADD_TO_SYSTEM_LIBRARY(time_syms, "time.h");
 
@@ -681,21 +730,27 @@ void dump_ct::init_system_library_map()
   // sys/select.h
   const char* sys_select_syms[]=
   {
-    "select"
+    "select",
+    /* non-public struct types */
+    "fd_set"
   };
   ADD_TO_SYSTEM_LIBRARY(sys_select_syms, "sys/select.h");
 
   // sys/socket.h
   const char* sys_socket_syms[]=
   {
-    "accept", "bind", "connect"
+    "accept", "bind", "connect",
+    /* non-public struct types */
+    "tag-sockaddr"
   };
   ADD_TO_SYSTEM_LIBRARY(sys_socket_syms, "sys/socket.h");
 
   // sys/stat.h
   const char* sys_stat_syms[]=
   {
-    "fstat", "lstat", "stat"
+    "fstat", "lstat", "stat",
+    /* non-public struct types */
+    "tag-stat"
   };
   ADD_TO_SYSTEM_LIBRARY(sys_stat_syms, "sys/stat.h");
 
@@ -715,6 +770,38 @@ void dump_ct::init_system_library_map()
   ADD_TO_SYSTEM_LIBRARY(sys_wait_syms, "sys/wait.h");
 }
 
+/*******************************************************************\
+
+Function: dump_ct::ignore
+
+Inputs: type  input to check whether it should not be dumped
+
+Outputs: true, iff the type should not be printed
+
+Purpose: Ignore selected types as they are covered via system headers
+
+\*******************************************************************/
+
+bool dump_ct::ignore(const typet &type)
+{
+  symbolt symbol;
+  symbol.type=type;
+
+  return ignore(symbol);
+}
+
+/*******************************************************************\
+
+Function: dump_ct::ignore
+
+Inputs: type  input to check whether it should not be dumped
+
+Outputs: true, iff the symbol should not be printed
+
+Purpose: Ignore selected symbols as they are covered via system headers
+
+\*******************************************************************/
+
 bool dump_ct::ignore(const symbolt &symbol)
 {
   const std::string &name_str=id2string(symbol.name);
@@ -729,15 +816,13 @@ bool dump_ct::ignore(const symbolt &symbol)
      name_str=="envp_size'")
     return true;
 
+  if(has_suffix(name_str, "$object"))
+    return true;
+
   const std::string &file_str=id2string(symbol.location.get_file());
 
   // don't dump internal GCC builtins
-  if((file_str=="gcc_builtin_headers_alpha.h" ||
-      file_str=="gcc_builtin_headers_arm.h" ||
-      file_str=="gcc_builtin_headers_ia32.h" ||
-      file_str=="gcc_builtin_headers_mips.h" ||
-      file_str=="gcc_builtin_headers_power.h" ||
-      file_str=="gcc_builtin_headers_generic.h") &&
+  if(has_prefix(file_str, "gcc_builtin_headers_") &&
      has_prefix(name_str, "__builtin_"))
     return true;
 
@@ -749,9 +834,6 @@ bool dump_ct::ignore(const symbolt &symbol)
     return true;
   }
 
-  if(name_str.find("$link")!=std::string::npos)
-    return false;
-
   system_library_mapt::const_iterator it=
     system_library_map.find(symbol.name);
 
@@ -761,6 +843,19 @@ bool dump_ct::ignore(const symbolt &symbol)
     return true;
   }
 
+  if(use_all_headers &&
+     has_prefix(file_str, "/usr/include/"))
+  {
+    if(file_str.find("/bits/")==std::string::npos)
+    {
+      // Do not include transitive includes of system headers!
+      std::string::size_type prefix_len=std::string("/usr/include/").size();
+      system_headers.insert(file_str.substr(prefix_len));
+    }
+
+    return true;
+  }
+
   return false;
 }
 
@@ -789,6 +884,10 @@ void dump_ct::cleanup_decl(
 
   tmp.add_instruction(END_FUNCTION);
 
+  std::unordered_set<irep_idt, irep_id_hash> typedef_names;
+  for(const auto &td : typedef_map)
+    typedef_names.insert(td.first);
+
   code_blockt b;
   goto_program2codet p2s(
     irep_idt(),
@@ -797,13 +896,268 @@ void dump_ct::cleanup_decl(
     b,
     local_static,
     local_type_decls,
+    typedef_names,
     system_headers);
   p2s();
 
-  assert(b.operands().size()==1);
+  POSTCONDITION(b.operands().size()==1);
   decl.swap(b.op0());
 }
 
+/*******************************************************************\
+
+Function: dump_ct::collect_typedefs
+
+Inputs:
+    type  Type to inspect for ID_C_typedef entry
+    early Set to true to enforce that typedef is dumped before any
+          function declarations or struct definitions
+
+Outputs:
+
+Purpose: Find any typedef names contained in the input type and store
+         their declaration strings in typedef_map for eventual output.
+
+\*******************************************************************/
+
+void dump_ct::collect_typedefs(const typet &type, bool early)
+{
+  std::unordered_set<irep_idt, irep_id_hash> deps;
+  collect_typedefs_rec(type, early, deps);
+}
+
+/*******************************************************************\
+
+Function: dump_ct::collect_typedefs_rec
+
+Inputs:
+    type  Type to inspect for ID_C_typedef entry
+    early Set to true to enforce that typedef is dumped before any
+          function declarations or struct definitions
+    dependencies Typedefs used in the declaration of a given typedef
+
+Outputs:
+
+Purpose: Find any typedef names contained in the input type and store
+         their declaration strings in typedef_map for eventual output.
+
+\*******************************************************************/
+
+void dump_ct::collect_typedefs_rec(
+  const typet &type,
+  bool early,
+  std::unordered_set<irep_idt, irep_id_hash> &dependencies)
+{
+  if(ignore(type))
+    return;
+
+  std::unordered_set<irep_idt, irep_id_hash> local_deps;
+
+  if(type.id()==ID_code)
+  {
+    const code_typet &code_type=to_code_type(type);
+
+    collect_typedefs_rec(code_type.return_type(), early, local_deps);
+    for(const auto &param : code_type.parameters())
+      collect_typedefs_rec(param.type(), early, local_deps);
+  }
+  else if(type.id()==ID_pointer || type.id()==ID_array)
+  {
+    collect_typedefs_rec(type.subtype(), early, local_deps);
+  }
+  else if(type.id()==ID_symbol)
+  {
+    const symbolt &symbol=
+      ns.lookup(to_symbol_type(type).get_identifier());
+    collect_typedefs_rec(symbol.type, early, local_deps);
+  }
+
+  const irep_idt &typedef_str=type.get(ID_C_typedef);
+
+  if(!typedef_str.empty())
+  {
+    std::pair<typedef_mapt::iterator, bool> entry=
+      typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
+
+    if(entry.second ||
+       (early && entry.first->second.type_decl_str.empty()))
+    {
+      if(typedef_str=="__gnuc_va_list" || typedef_str == "va_list")
+      {
+        system_headers.insert("stdarg.h");
+        early=false;
+      }
+      else
+      {
+        typet t=type;
+        t.remove(ID_C_typedef);
+
+        std::ostringstream oss;
+        oss << "typedef " << make_decl(typedef_str, t) << ';';
+
+        entry.first->second.type_decl_str=oss.str();
+        entry.first->second.dependencies=local_deps;
+      }
+    }
+
+    if(early)
+    {
+      entry.first->second.early=true;
+
+      for(const auto &d : local_deps)
+      {
+        auto td_entry=typedef_map.find(d);
+        PRECONDITION(td_entry!=typedef_map.end());
+        td_entry->second.early=true;
+      }
+    }
+
+    dependencies.insert(typedef_str);
+  }
+
+  dependencies.insert(local_deps.begin(), local_deps.end());
+}
+
+/*******************************************************************\
+
+Function: dump_ct::gather_global_typedefs
+
+Inputs:
+
+Outputs:
+
+Purpose: find all global typdefs in the symbol table and store them
+         in typedef_types
+
+\*******************************************************************/
+
+void dump_ct::gather_global_typedefs()
+{
+  // sort the symbols first to ensure deterministic replacement in
+  // typedef_types below as there could be redundant declarations
+  // typedef int x;
+  // typedef int y;
+  std::map<std::string, symbolt> symbols_sorted;
+  for(const auto &symbol_entry : copied_symbol_table.symbols)
+    symbols_sorted.insert(
+      {id2string(symbol_entry.first), symbol_entry.second});
+
+  for(const auto &symbol_entry : symbols_sorted)
+  {
+    const symbolt &symbol=symbol_entry.second;
+
+    if(symbol.is_macro && symbol.is_type &&
+       symbol.location.get_function().empty())
+    {
+      const irep_idt &typedef_str=symbol.type.get(ID_C_typedef);
+      PRECONDITION(!typedef_str.empty());
+      typedef_types[symbol.type]=typedef_str;
+      if(ignore(symbol))
+        typedef_map.insert({typedef_str, typedef_infot(typedef_str)});
+      else
+        collect_typedefs(symbol.type, false);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: dump_ct::dump_typedefs
+
+Inputs:
+
+Outputs: os  output stream
+
+Purpose: print all typedefs that are not covered via
+         typedef struct xyz { ... } name;
+
+\*******************************************************************/
+
+void dump_ct::dump_typedefs(std::ostream &os) const
+{
+  // we need to compute a topological sort; we do so by picking all
+  // typedefs the dependencies of which have been emitted into to_insert
+  std::vector<typedef_infot> typedefs_sorted;
+  typedefs_sorted.reserve(typedef_map.size());
+
+  // elements in to_insert are lexicographically sorted and ready for
+  // output
+  std::map<std::string, typedef_infot> to_insert;
+
+  typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
+  id_sett typedefs_done;
+  std::unordered_map<irep_idt, id_sett, irep_id_hash>
+    forward_deps, reverse_deps;
+
+  for(const auto &td : typedef_map)
+    if(!td.second.type_decl_str.empty())
+    {
+      if(td.second.dependencies.empty())
+        // those can be dumped immediately
+        to_insert.insert({id2string(td.first), td.second});
+      else
+      {
+        // delay them until dependencies are dumped
+        forward_deps.insert({td.first, td.second.dependencies});
+        for(const auto &d : td.second.dependencies)
+          reverse_deps[d].insert(td.first);
+      }
+    }
+
+  while(!to_insert.empty())
+  {
+    // the topologically next element (lexicographically ranked first
+    // among all the dependencies of which have been dumped)
+    typedef_infot t=to_insert.begin()->second;
+    to_insert.erase(to_insert.begin());
+    // move to the output queue
+    typedefs_sorted.push_back(t);
+
+    // find any depending typedefs that are now valid, or at least
+    // reduce the remaining dependencies
+    auto r_it=reverse_deps.find(t.typedef_name);
+    if(r_it==reverse_deps.end())
+      continue;
+
+    // reduce remaining dependencies
+    id_sett &r_deps=r_it->second;
+    for(id_sett::iterator it=r_deps.begin(); it!=r_deps.end(); ) // no ++it
+    {
+      auto f_it=forward_deps.find(*it);
+      if(f_it==forward_deps.end()) // might be done already
+      {
+        it=r_deps.erase(it);
+        continue;
+      }
+
+      // update dependencies
+      id_sett &f_deps=f_it->second;
+      PRECONDITION(!f_deps.empty());
+      PRECONDITION(f_deps.find(t.typedef_name)!=f_deps.end());
+      f_deps.erase(t.typedef_name);
+
+      if(f_deps.empty()) // all depenencies done now!
+      {
+        const auto td_entry=typedef_map.find(*it);
+        PRECONDITION(td_entry!=typedef_map.end());
+        to_insert.insert({id2string(*it), td_entry->second});
+        forward_deps.erase(*it);
+        it=r_deps.erase(it);
+      }
+      else
+        ++it;
+    }
+  }
+
+  POSTCONDITION(forward_deps.empty());
+
+  for(const auto &td : typedefs_sorted)
+    os << td.type_decl_str << '\n';
+
+  if(!typedefs_sorted.empty())
+    os << '\n';
+}
+
 void dump_ct::convert_global_variable(
     const symbolt &symbol,
     std::ostream &os,
@@ -837,8 +1191,10 @@ void dump_ct::convert_global_variable(
         it=syms.begin();
         it!=syms.end();
         ++it)
-      if(!symbols_sorted.insert(id2string(*it)).second)
-        assert(false);
+    {
+      bool inserted=symbols_sorted.insert(id2string(*it)).second;
+      CHECK_RETURN(inserted);
+    }
 
     for(std::set<std::string>::const_iterator
         it=symbols_sorted.begin();
@@ -862,7 +1218,7 @@ void dump_ct::convert_global_variable(
 
     std::list<irep_idt> empty_static, empty_types;
     cleanup_decl(d, empty_static, empty_types);
-    assert(empty_static.empty());
+    CHECK_RETURN(empty_static.empty());
     os << expr_to_string(d) << '\n';
   }
 }
@@ -888,6 +1244,10 @@ void dump_ct::convert_function_declaration(
     code_blockt b;
     std::list<irep_idt> type_decls, local_static;
 
+    std::unordered_set<irep_idt, irep_id_hash> typedef_names;
+    for(const auto &td : typedef_map)
+      typedef_names.insert(td.first);
+
     goto_program2codet p2s(
       symbol.name,
       func_entry->second.body,
@@ -895,6 +1255,7 @@ void dump_ct::convert_function_declaration(
       b,
       local_static,
       type_decls,
+      typedef_names,
       system_headers);
     p2s();
 
@@ -933,6 +1294,10 @@ void dump_ct::convert_function_declaration(
     os_decl << "// " << symbol.location << '\n';
     os_decl << make_decl(symbol.name, symbol.type) << ";\n";
   }
+
+  // make sure typedef names used in the function declaration are
+  // available
+  collect_typedefs(symbol.type, true);
 }
 
 static bool find_block_position_rec(
@@ -1029,7 +1394,7 @@ void dump_ct::insert_local_static_decls(
   {
     local_static_declst::const_iterator d_it=
       local_static_decls.find(*it);
-    assert(d_it!=local_static_decls.end());
+    PRECONDITION(d_it!=local_static_decls.end());
 
     code_declt d=d_it->second;
     std::list<irep_idt> redundant;
@@ -1042,7 +1407,7 @@ void dump_ct::insert_local_static_decls(
     // within an if(false) { ... } block
     if(find_block_position_rec(*it, b, dest_ptr, before))
     {
-      assert(dest_ptr!=0);
+      CHECK_RETURN(dest_ptr!=0);
       dest_ptr->operands().insert(before, d);
     }
   }
@@ -1079,7 +1444,7 @@ void dump_ct::insert_local_type_decls(
     // has been removed by cleanup operations
     if(find_block_position_rec(*it, b, dest_ptr, before))
     {
-      assert(dest_ptr!=0);
+      CHECK_RETURN(dest_ptr!=0);
       dest_ptr->operands().insert(before, skip);
     }
   }
@@ -1103,7 +1468,7 @@ void dump_ct::cleanup_expr(exprt &expr)
     exprt::operandst old_ops;
     old_ops.swap(expr.operands());
 
-    assert(old_components.size()==old_ops.size());
+    PRECONDITION(old_components.size()==old_ops.size());
     exprt::operandst::iterator o_it=old_ops.begin();
     for(struct_union_typet::componentst::const_iterator
         it=old_components.begin();
@@ -1145,7 +1510,7 @@ void dump_ct::cleanup_expr(exprt &expr)
       const struct_union_typet::componentt &comp=
         u_type_f.get_component(u.get_component_name());
       const typet &u_op_type=comp.type();
-      assert(u_op_type.id()==ID_pointer);
+      PRECONDITION(u_op_type.id()==ID_pointer);
 
       typecast_exprt tc(u.op(), u_op_type);
       expr.swap(tc);
@@ -1253,8 +1618,9 @@ void dump_ct::cleanup_type(typet &type)
   if(type.id()==ID_array)
     cleanup_expr(to_array_type(type).size());
 
-  assert((type.id()!=ID_union && type.id()!=ID_struct) ||
-         !type.get(ID_tag).empty());
+  POSTCONDITION(
+    (type.id()!=ID_union && type.id()!=ID_struct) ||
+    !type.get(ID_tag).empty());
 }
 
 std::string dump_ct::type_to_string(const typet &type)
@@ -1278,19 +1644,23 @@ std::string dump_ct::expr_to_string(const exprt &expr)
 void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out)
 {
-  dump_ct goto2c(src, use_system_headers, ns, new_ansi_c_language);
+  dump_ct goto2c(
+    src, use_system_headers, use_all_headers, ns, new_ansi_c_language);
   out << goto2c;
 }
 
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out)
 {
-  dump_ct goto2cpp(src, use_system_headers, ns, new_cpp_language);
+  dump_ct goto2cpp(
+    src, use_system_headers, use_all_headers, ns, new_cpp_language);
   out << goto2cpp;
 }
diff --git a/src/goto-instrument/dump_c.h b/src/goto-instrument/dump_c.h
index 263165aec97..afac58b9007 100644
--- a/src/goto-instrument/dump_c.h
+++ b/src/goto-instrument/dump_c.h
@@ -17,12 +17,14 @@ Author: Daniel Kroening, kroening@kroening.com
 void dump_c(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out);
 
 void dump_cpp(
   const goto_functionst &src,
   const bool use_system_headers,
+  const bool use_all_headers,
   const namespacet &ns,
   std::ostream &out);
 
diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
index 32e9ce85bb5..255cb88677e 100644
--- a/src/goto-instrument/dump_c_class.h
+++ b/src/goto-instrument/dump_c_class.h
@@ -25,12 +25,14 @@ class dump_ct
   dump_ct(
     const goto_functionst &_goto_functions,
     const bool use_system_headers,
+    const bool use_all_headers,
     const namespacet &_ns,
     language_factoryt factory):
     goto_functions(_goto_functions),
     copied_symbol_table(_ns.get_symbol_table()),
     ns(copied_symbol_table),
-    language(factory())
+    language(factory()),
+    use_all_headers(use_all_headers)
   {
     if(use_system_headers)
       init_system_library_map();
@@ -48,6 +50,7 @@ class dump_ct
   symbol_tablet copied_symbol_table;
   const namespacet ns;
   languaget *language;
+  const bool use_all_headers;
 
   typedef std::unordered_set<irep_idt, irep_id_hash> convertedt;
   convertedt converted_compound, converted_global, converted_enum;
@@ -62,12 +65,32 @@ class dump_ct
     declared_enum_constants_mapt;
   declared_enum_constants_mapt declared_enum_constants;
 
+  struct typedef_infot
+  {
+    irep_idt typedef_name;
+    std::string type_decl_str;
+    bool early;
+    std::unordered_set<irep_idt, irep_id_hash> dependencies;
+
+    explicit typedef_infot(const irep_idt &name):
+      typedef_name(name),
+      type_decl_str(""),
+      early(false)
+    {
+    }
+  };
+  typedef std::map<irep_idt, typedef_infot> typedef_mapt;
+  typedef_mapt typedef_map;
+  typedef std::unordered_map<typet, irep_idt, irep_hash> typedef_typest;
+  typedef_typest typedef_types;
+
   void init_system_library_map();
 
   std::string type_to_string(const typet &type);
   std::string expr_to_string(const exprt &expr);
 
   bool ignore(const symbolt &symbol);
+  bool ignore(const typet &type);
 
   static std::string indent(const unsigned n)
   {
@@ -88,6 +111,14 @@ class dump_ct
     return d_str.substr(0, d_str.size()-1);
   }
 
+  void collect_typedefs(const typet &type, bool early);
+  void collect_typedefs_rec(
+    const typet &type,
+    bool early,
+    std::unordered_set<irep_idt, irep_id_hash> &dependencies);
+  void gather_global_typedefs();
+  void dump_typedefs(std::ostream &os) const;
+
   void convert_compound_declaration(
       const symbolt &symbol,
       std::ostream &os_body);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 622618a220f..b807b21dc9a 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -621,7 +621,8 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("dump-c") || cmdline.isset("dump-cpp"))
     {
       const bool is_cpp=cmdline.isset("dump-cpp");
-      const bool h=cmdline.isset("use-system-headers");
+      const bool h_libc=!cmdline.isset("no-system-headers");
+      const bool h_all=cmdline.isset("use-all-headers");
       namespacet ns(symbol_table);
 
       // restore RETURN instructions in case remove_returns had been
@@ -640,10 +641,11 @@ int goto_instrument_parse_optionst::doit()
           error() << "failed to write to `" << cmdline.args[1] << "'";
           return 10;
         }
-        (is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, out);
+        (is_cpp ? dump_cpp : dump_c)(goto_functions, h_libc, h_all, ns, out);
       }
       else
-        (is_cpp ? dump_cpp : dump_c)(goto_functions, h, ns, std::cout);
+        (is_cpp ? dump_cpp : dump_c)(
+          goto_functions, h_libc, h_all, ns, std::cout);
 
       return 0;
     }
@@ -1540,7 +1542,8 @@ void goto_instrument_parse_optionst::help()
     " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
     "\n"
     "Other options:\n"
-    " --use-system-headers         with --dump-c/--dump-cpp: generate C source with includes\n" // NOLINT(*)
+    " --no-system-headers          with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
+    " --use-all-headers            with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 7cd570607d9..e2c4bf4fbc0 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(all)" \
   "(document-claims-latex)(document-claims-html)" \
   "(document-properties-latex)(document-properties-html)" \
-  "(dump-c)(dump-cpp)(use-system-headers)(dot)(xml)" \
+  "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
   OPT_GOTO_CHECK \
   /* no-X-check are deprecated and ignored */ \
   "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 508c4fcaa3e..dac40c7b4ee 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -110,14 +110,23 @@ void goto_program2codet::scan_for_varargs()
   forall_goto_program_instructions(target, goto_program)
     if(target->is_assign())
     {
+      const exprt &l=to_code_assign(target->code).lhs();
       const exprt &r=to_code_assign(target->code).rhs();
 
+      // find va_arg_next
       if(r.id()==ID_side_effect &&
          to_side_effect_expr(r).get_statement()==ID_gcc_builtin_va_arg_next)
       {
         assert(r.has_operands());
         va_list_expr.insert(r.op0());
       }
+      // try our modelling of va_start
+      else if(l.type().id()==ID_pointer &&
+              l.type().get(ID_C_typedef)=="va_list" &&
+              l.id()==ID_symbol &&
+              r.id()==ID_typecast &&
+              to_typecast_expr(r).op().id()==ID_address_of)
+        va_list_expr.insert(l);
     }
 
   if(!va_list_expr.empty())
@@ -556,7 +565,7 @@ goto_programt::const_targett goto_program2codet::convert_goto(
   else if(!target->guard.is_true())
     return convert_goto_switch(target, upper_bound, dest);
   else if(!loop_last_stack.empty())
-    return convert_goto_break_continue(target, dest);
+    return convert_goto_break_continue(target, upper_bound, dest);
   else
     return convert_goto_goto(target, dest);
 }
@@ -794,7 +803,14 @@ bool goto_program2codet::set_block_end_points(
 
       // ignore dead instructions for the following checks
       if(n.dominators.empty())
+      {
+        // simplification may have figured out that a case is unreachable
+        // this is possibly getting too weird, abort to be safe
+        if(case_end==it->case_start)
+          return true;
+
         continue;
+      }
 
       // find the last instruction dominated by the case start
       if(n.dominators.find(it->case_start)==n.dominators.end())
@@ -1098,7 +1114,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
        upper_bound->location_number < end_if->location_number))
   {
     if(!loop_last_stack.empty())
-      return convert_goto_break_continue(target, dest);
+      return convert_goto_break_continue(target, upper_bound, dest);
     else
       return convert_goto_goto(target, dest);
   }
@@ -1131,6 +1147,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_if(
 
 goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
     goto_programt::const_targett target,
+    goto_programt::const_targett upper_bound,
     codet &dest)
 {
   assert(!loop_last_stack.empty());
@@ -1140,7 +1157,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue(
   // 1: ...
   goto_programt::const_targett next=target;
   for(++next;
-      next!=goto_program.instructions.end();
+      next!=upper_bound && next!=goto_program.instructions.end();
       ++next)
   {
     cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry=
@@ -1496,6 +1513,11 @@ void goto_program2codet::cleanup_code(
 
     add_local_types(code.op0().type());
 
+    const irep_idt &typedef_str=code.op0().type().get(ID_C_typedef);
+    if(!typedef_str.empty() &&
+       typedef_names.find(typedef_str)==typedef_names.end())
+      code.op0().type().remove(ID_C_typedef);
+
     return;
   }
   else if(code.get_statement()==ID_function_call)
@@ -1851,6 +1873,11 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
 
     add_local_types(t);
     expr=typecast_exprt(expr, t);
+
+    const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
+    if(!typedef_str.empty() &&
+       typedef_names.find(typedef_str)==typedef_names.end())
+      expr.type().remove(ID_C_typedef);
   }
   else if(expr.id()==ID_array ||
           expr.id()==ID_vector)
@@ -1863,6 +1890,11 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
 
     expr.make_typecast(t);
     add_local_types(t);
+
+    const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
+    if(!typedef_str.empty() &&
+       typedef_names.find(typedef_str)==typedef_names.end())
+      expr.type().remove(ID_C_typedef);
   }
   else if(expr.id()==ID_side_effect)
   {
@@ -1978,6 +2010,11 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     {
       add_local_types(expr.type());
 
+      const irep_idt &typedef_str=expr.type().get(ID_C_typedef);
+      if(!typedef_str.empty() &&
+         typedef_names.find(typedef_str)==typedef_names.end())
+        expr.type().remove(ID_C_typedef);
+
       assert(expr.type().id()!=ID_union &&
              expr.type().id()!=ID_struct);
     }
diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h
index f8aa1eed53f..3bf1ea7404f 100644
--- a/src/goto-instrument/goto_program2code.h
+++ b/src/goto-instrument/goto_program2code.h
@@ -52,6 +52,7 @@ class goto_program2codet
       code_blockt &_dest,
       id_listt &_local_static,
       id_listt &_type_names,
+      const id_sett &_typedef_names,
       std::set<std::string> &_system_headers):
     func_name(identifier),
     goto_program(_goto_program),
@@ -60,6 +61,7 @@ class goto_program2codet
     toplevel_block(_dest),
     local_static(_local_static),
     type_names(_type_names),
+    typedef_names(_typedef_names),
     system_headers(_system_headers)
   {
     assert(local_static.empty());
@@ -81,6 +83,7 @@ class goto_program2codet
   code_blockt &toplevel_block;
   id_listt &local_static;
   id_listt &type_names;
+  const id_sett &typedef_names;
   std::set<std::string> &system_headers;
   std::unordered_set<exprt, irep_hash> va_list_expr;
 
@@ -196,6 +199,7 @@ class goto_program2codet
 
   goto_programt::const_targett convert_goto_break_continue(
       goto_programt::const_targett target,
+      goto_programt::const_targett upper_bound,
       codet &dest);
 
   goto_programt::const_targett convert_goto_goto(
diff --git a/src/goto-programs/read_goto_binary.cpp b/src/goto-programs/read_goto_binary.cpp
index 717da589d2f..6eaede5fd97 100644
--- a/src/goto-programs/read_goto_binary.cpp
+++ b/src/goto-programs/read_goto_binary.cpp
@@ -302,7 +302,7 @@ static bool link_functions(
   rename_symbolt macro_application;
 
   forall_symbols(it, dest_symbol_table.symbols)
-    if(it->second.is_macro)
+    if(it->second.is_macro && !it->second.is_type)
     {
       const symbolt &symbol=it->second;
 
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
index 32e10d33627..e58d64855fe 100644
--- a/src/util/find_symbols.cpp
+++ b/src/util/find_symbols.cpp
@@ -124,6 +124,10 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
 
     forall_subtypes(it, src)
       find_symbols(kind, *it, dest);
+
+    const irep_idt &typedef_name=src.get(ID_C_typedef);
+    if(!typedef_name.empty())
+      dest.insert(typedef_name);
   }
 
   if(src.id()==ID_struct ||