diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
index 8fde8c57c4d..f8781ffd921 100644
--- a/src/ansi-c/ansi_c_convert_type.cpp
+++ b/src/ansi-c/ansi_c_convert_type.cpp
@@ -253,7 +253,9 @@ Function: ansi_c_convert_typet::write
 
 void ansi_c_convert_typet::write(typet &type)
 {
+  irep_idt _typedef = type.get(ID_typedef);
   type.clear();
+  type.set(ID_typedef,_typedef);
 
   // first, do "other"
 
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
index f9dea43c02b..80074545b79 100644
--- a/src/ansi-c/ansi_c_declaration.cpp
+++ b/src/ansi-c/ansi_c_declaration.cpp
@@ -139,6 +139,17 @@ typet ansi_c_declarationt::full_type(
 
   *p=type();
 
+  // retain typedef for dump-c
+  if(get_is_typedef())
+    result.set(ID_typedef,declarator.get_name());
+  // If this declaration was declared with a typedef'd type, we record it in the
+  // type of the expression.
+  irep_idt typedef_type=declarator.get(ID_typedef);
+  if(typedef_type!="")
+  {
+    result.set(ID_typedef, typedef_type);
+  }
+
   return result;
 }
 
diff --git a/src/ansi-c/ansi_c_parser.cpp b/src/ansi-c/ansi_c_parser.cpp
index 88787d4b519..8f3720546a9 100644
--- a/src/ansi-c/ansi_c_parser.cpp
+++ b/src/ansi-c/ansi_c_parser.cpp
@@ -136,6 +136,16 @@ void ansi_c_parsert::add_declarator(
   irept &declarator)
 {
   assert(declarator.is_not_nil());
+
+  irep_idt typedefd_name="";
+  if(declarator.id()==ID_symbol)
+  {
+    if(declaration.type().id()==ID_symbol)
+    {
+      typedefd_name=declaration.type().get(ID_identifier);
+    }
+  }
+
   ansi_c_declarationt &ansi_c_declaration=
     to_ansi_c_declaration(declaration);
 
@@ -197,6 +207,11 @@ void ansi_c_parsert::add_declarator(
     identifier.prefixed_name=prefixed_name;
   }
 
+  if(typedefd_name!="")
+  {
+    new_declarator.set(ID_typedef, typedefd_name);
+  }
+
   ansi_c_declaration.declarators().push_back(new_declarator);
 }
 
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
index be7c58cc197..917d3e8adfd 100644
--- a/src/ansi-c/c_typecheck_base.cpp
+++ b/src/ansi-c/c_typecheck_base.cpp
@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "type2name.h"
 #include "c_storage_spec.h"
 
+#include <iostream>
+
 /*******************************************************************\
 
 Function: c_typecheck_baset::to_string
@@ -96,6 +98,9 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
   bool is_function=symbol.type.id()==ID_code;
 
   const typet &final_type=follow(symbol.type);
+//  std::cout << "BASENAME: " << symbol.base_name << std::endl;
+//  std::cout << "TYPE: " << symbol.type.pretty() << std::endl;
+//  std::cout << "FINAL: " << final_type.pretty() << std::endl;
 
   // set a few flags
   symbol.is_lvalue=!symbol.is_type && !symbol.is_macro;
@@ -127,13 +132,23 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
      (final_type.id()==ID_struct ||
       final_type.id()==ID_incomplete_struct))
   {
-    symbol.pretty_name="struct "+id2string(symbol.base_name);
+    if(symbol.type.find(ID_typedef).is_not_nil())
+      symbol.pretty_name=symbol.type.get(ID_typedef);
+    else
+      symbol.pretty_name="struct "+id2string(symbol.base_name);
   }
   else if(symbol.is_type &&
           (final_type.id()==ID_union ||
            final_type.id()==ID_incomplete_union))
   {
-    symbol.pretty_name="union "+id2string(symbol.base_name);
+    if(symbol.type.find(ID_typedef).is_not_nil())
+    {
+      symbol.pretty_name=symbol.type.get(ID_typedef);
+      symbol_table.symbols.find(symbol.type.get(ID_identifier))->second.pretty_name=symbol.type.get(ID_typedef);
+      symbol_table.symbols.find(symbol.type.get(ID_identifier))->second.type.set(ID_typedef,symbol.pretty_name);
+    }
+    else
+      symbol.pretty_name="union "+id2string(symbol.base_name);
   }
   else if(symbol.is_type &&
           (final_type.id()==ID_c_enum ||
@@ -149,6 +164,7 @@ void c_typecheck_baset::typecheck_symbol(symbolt &symbol)
   // see if we have it already
   symbol_tablet::symbolst::iterator old_it=symbol_table.symbols.find(symbol.name);
 
+
   if(old_it==symbol_table.symbols.end())
   {
     // just put into symbol_table
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 3002bd5c7d5..84502e2c4f3 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -23,6 +23,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "type2name.h"
 #include "ansi_c_convert_type.h"
 
+#include <iostream>
+
 /*******************************************************************\
 
 Function: c_typecheck_baset::typecheck_type
@@ -52,12 +54,14 @@ void c_typecheck_baset::typecheck_type(typet &type)
     c_qualifiers+=c_qualifierst(type.subtype());
     bool packed=type.get_bool(ID_C_packed);
     exprt alignment=static_cast<const exprt &>(type.find(ID_C_alignment));
+    irept _typedef=type.find(ID_typedef);
 
     type.swap(type.subtype());
 
     c_qualifiers.write(type);
     if(packed) type.set(ID_C_packed, true);
     if(alignment.is_not_nil()) type.add(ID_C_alignment, alignment);
+    if(_typedef.is_not_nil()) type.add(ID_typedef, _typedef);
 
     return; // done
   }
@@ -726,11 +730,15 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
     // Anonymous? Must come with body.
     assert(have_body);
 
+//    std::cout << "__TYPE: " << type.pretty() << std::endl;
+
     // produce symbol
     symbolt compound_symbol;
     compound_symbol.is_type=true;
     compound_symbol.type=type;
     compound_symbol.location=type.source_location();
+    if(compound_symbol.type.find(ID_typedef).is_not_nil())
+      compound_symbol.pretty_name=compound_symbol.type.get(ID_typedef);
 
     typecheck_compound_body(to_struct_union_type(compound_symbol.type));
 
@@ -739,6 +747,9 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
     compound_symbol.name="tag-#anon#"+typestr;
     identifier=compound_symbol.name;
 
+//  std::cout << "TYPEDEF: " << compound_symbol.type.get_string(ID_typedef) << std::endl;
+//  std::cout << "BASENAME: " << id2string(compound_symbol.base_name) << std::endl;
+
     // We might already have the same anonymous union/struct,
     // and this is simply ok. Note that the C standard treats
     // these as different types.
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 78ced9c86a3..d24c7edfd17 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -360,7 +360,12 @@ std::string expr2ct::convert_rec(
   {
     const struct_typet &struct_type=to_struct_type(src);
 
-    std::string dest=q+"struct";
+    std::string dest=q;
+
+    if(src.find(ID_typedef).is_not_nil())
+      dest+="typedef struct";
+    else
+      dest+="struct";
 
     const irep_idt &tag=struct_type.get_tag();
     if(tag!="") dest+=" "+id2string(tag);
@@ -378,7 +383,10 @@ std::string expr2ct::convert_rec(
 
     dest+=" }";
 
-    dest+=d;
+    if(src.find(ID_typedef).is_not_nil())
+      dest+=src.get_string(ID_typedef);
+    else
+      dest+=d;
 
     return dest;
   }
@@ -396,7 +404,12 @@ std::string expr2ct::convert_rec(
   {
     const union_typet &union_type=to_union_type(src);
 
-    std::string dest=q+"union";
+    std::string dest=q;
+
+    if(src.find(ID_typedef).is_not_nil())
+      dest+="typedef union";
+    else
+      dest+="union";
 
     const irep_idt &tag=union_type.get_tag();
     if(tag!="") dest+=" "+id2string(tag);
@@ -414,7 +427,10 @@ std::string expr2ct::convert_rec(
 
     dest+=" }";
 
-    dest+=d;
+    if(src.find(ID_typedef).is_not_nil())
+      dest+=src.get_string(ID_typedef);
+    else
+      dest+=d;
 
     return dest;
   }
@@ -538,29 +554,47 @@ std::string expr2ct::convert_rec(
   }
   else if(src.id()==ID_symbol)
   {
-    const typet &followed=ns.follow(src);
+    symbol_typet symbolic_type=to_symbol_type(src);
+    const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
 
-    if(followed.id()==ID_struct)
+    // Providing we have a valid identifer, we can just use that rather than
+    // trying to find the concrete type
+    if(typedef_identifer!="")
     {
-      std::string dest=q+"struct";
-      const irep_idt &tag=to_struct_type(followed).get_tag();
-      if(tag!="") dest+=" "+id2string(tag);
-      dest+=d;
-      return dest;
+      return q+id2string(typedef_identifer)+d;
     }
-    else if(followed.id()==ID_union)
+    else
     {
-      std::string dest=q+"union";
-      const irep_idt &tag=to_union_type(followed).get_tag();
-      if(tag!="") dest+=" "+id2string(tag);
-      dest+=d;
-      return dest;
+      const typet &followed=ns.follow(src);
+
+      if(followed.id()==ID_struct)
+      {
+      if(followed.find(ID_typedef).is_not_nil())
+        return followed.get_string(ID_typedef)+d;
+        std::string dest=q+"struct";
+        const irep_idt &tag=to_struct_type(followed).get_tag();
+        if(tag!="") dest+=" "+id2string(tag);
+        dest+=d;
+        return dest;
+      }
+      else if(followed.id()==ID_union)
+      {
+      if(followed.find(ID_typedef).is_not_nil())
+        return followed.get_string(ID_typedef)+d;
+        std::string dest=q+"union";
+        const irep_idt &tag=to_union_type(followed).get_tag();
+        if(tag!="") dest+=" "+id2string(tag);
+        dest+=d;
+        return dest;
+      }
+      else
+        return convert_rec(followed, new_qualifiers, declarator);
     }
-    else
-      return convert_rec(followed, new_qualifiers, declarator);
   }
   else if(src.id()==ID_struct_tag)
   {
+    if(src.find(ID_typedef).is_not_nil())
+      return src.get_string(ID_typedef)+d;
     const struct_tag_typet &struct_tag_type=
       to_struct_tag_type(src);
 
@@ -573,6 +607,8 @@ std::string expr2ct::convert_rec(
   }
   else if(src.id()==ID_union_tag)
   {
+    if(src.find(ID_typedef).is_not_nil())
+      return src.get_string(ID_typedef)+d;
     const union_tag_typet &union_tag_type=
       to_union_tag_type(src);
 
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 1d6d7cc712e..0ca8beb74ef 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -161,6 +161,9 @@ void dump_ct::operator()(std::ostream &os)
         symbol.type.set(ID_tag, new_tag);
     }
 
+    if(ignore(symbol))
+      ignored_symbol_rec(symbol);
+
     // we don't want to dump in full all definitions
     if(!tag_added && ignore(symbol))
       continue;
@@ -177,6 +180,10 @@ void dump_ct::operator()(std::ostream &os)
       ++it)
   {
     const symbolt &symbol=ns.lookup(*it);
+
+    if(ignore(symbol))
+      continue;
+
     const irep_idt &type_id=symbol.type.id();
 
     if(symbol.is_type &&
@@ -192,6 +199,10 @@ void dump_ct::operator()(std::ostream &os)
 
       if(type_id==ID_c_enum)
         convert_compound_enum(symbol.type, os);
+      else if(symbol.type.find(ID_typedef).is_not_nil())
+      {
+        //skip
+      }
       else
         os << type_to_string(symbol_typet(symbol.name)) << ";\n\n";
     }
@@ -221,6 +232,9 @@ void dump_ct::operator()(std::ostream &os)
   {
     const symbolt &symbol=ns.lookup(*it);
 
+    if(ignore(symbol))
+      continue;
+
     if(symbol.type.id()!=ID_code) continue;
 
     convert_function_declaration(
@@ -239,6 +253,9 @@ void dump_ct::operator()(std::ostream &os)
   {
     const symbolt &symbol=ns.lookup(*it);
 
+    if(ignore(symbol))
+      continue;
+
     if(symbol.is_type &&
         (symbol.type.id()==ID_struct ||
          symbol.type.id()==ID_incomplete_struct ||
@@ -517,7 +534,12 @@ void dump_ct::convert_compound(
     struct_body << ";" << std::endl;
   }
 
-  os << type_to_string(unresolved);
+
+  if(type.find(ID_typedef).is_not_nil())
+    os << "typedef "+id2string(type.id());
+  else
+    os << type_to_string(unresolved);
+
   if(!base_decls.str().empty())
   {
     assert(language->id()=="cpp");
@@ -544,6 +566,8 @@ void dump_ct::convert_compound(
     os << " __attribute__ ((__transparent_union__))";
   if(type.get_bool(ID_C_packed))
     os << " __attribute__ ((__packed__))";
+  if(type.find(ID_typedef).is_not_nil())
+    os << " " << type.get_string(ID_typedef);
   os << ";";
   os << std::endl;
   os << std::endl;
@@ -673,10 +697,18 @@ 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",
+    "pthread_mutex_t", "pthread_attr_t", "pthread_cond_t",
+    "tag-__pthread_internal_list", "tag-__pthread_mutex_s"
   };
   ADD_TO_SYSTEM_LIBRARY(pthread_syms, "pthread.h");
 
+  // sys/resource.h
+  const char* sys_resource_syms[]={
+    "getrusage", "tag-rusage"
+  };
+  ADD_TO_SYSTEM_LIBRARY(sys_resource_syms, "sys/resource.h");
+
   // setjmp.h
   const char* setjmp_syms[]={
     "_longjmp", "_setjmp", "longjmp", "longjmperror", "setjmp",
@@ -722,7 +754,7 @@ void dump_ct::init_system_library_map()
   const char* string_syms[]={
     "strcat", "strncat", "strchr", "strrchr", "strcmp", "strncmp",
     "strcpy", "strncpy", "strerror", "strlen", "strpbrk", "strspn",
-    "strcspn", "strstr", "strtok"
+    "strcspn", "strstr", "strtok", "memcpy", "memset"
   };
   ADD_TO_SYSTEM_LIBRARY(string_syms, "string.h");
 
@@ -735,6 +767,12 @@ void dump_ct::init_system_library_map()
   };
   ADD_TO_SYSTEM_LIBRARY(time_syms, "time.h");
 
+  // sys/time.h
+  const char* sys_time_syms[]={
+    "gettimeofday", "tag-timezone"
+  };
+  ADD_TO_SYSTEM_LIBRARY(sys_time_syms, "sys/time.h");
+
   // unistd.h
   const char* unistd_syms[]={
     "_exit", "access", "alarm", "chdir", "chown", "close", "dup",
@@ -782,6 +820,41 @@ void dump_ct::init_system_library_map()
 
 /*******************************************************************\
 
+Function: dump_ct::ignored_symbol_rec
+
+Inputs:
+
+Outputs:
+
+Purpose: recursively marks symbols that shall be ignored
+
+\*******************************************************************/
+
+void dump_ct::ignored_symbol_rec(const symbolt &symbol)
+{
+  ignored_symbols.insert(id2string(symbol.name));
+
+  if(!(symbol.is_type &&
+       (symbol.type.id()==ID_union ||
+        symbol.type.id()==ID_struct)))
+    return;
+
+  const struct_union_typet &type=
+    to_struct_union_type(ns.follow(symbol.type));
+
+  for(struct_union_typet::componentst::const_iterator
+      it=type.components().begin();
+      it!=type.components().end();
+      it++)
+  {
+    const struct_typet::componentt &comp=*it;
+    if(comp.type().id()==ID_symbol)
+      ignored_symbol_rec(ns.lookup(to_symbol_type(comp.type()).get_identifier()));
+  }
+}
+
+/*******************************************************************\
+
 Function: dump_ct::ignore
 
 Inputs:
@@ -796,6 +869,9 @@ bool dump_ct::ignore(const symbolt &symbol)
 {
   const std::string &name_str=id2string(symbol.name);
 
+  if(ignored_symbols.find(name_str)!=ignored_symbols.end())
+    return true;
+
   if(has_prefix(name_str, CPROVER_PREFIX) ||
      name_str=="__func__" ||
      name_str=="__FUNCTION__" ||
@@ -827,10 +903,13 @@ bool dump_ct::ignore(const symbolt &symbol)
   }
 
   if(name_str.find("$link")!=std::string::npos)
-    return false;
+    return true;
 
-  system_library_mapt::const_iterator it=
-    system_library_map.find(symbol.name);
+  system_library_mapt::const_iterator it;
+  if(symbol.is_type && symbol.type.find(ID_typedef).is_not_nil())
+    it=system_library_map.find(symbol.type.get_string(ID_typedef));
+  else
+    it=system_library_map.find(symbol.name);
 
   if(it!=system_library_map.end())
   {
@@ -1446,6 +1525,10 @@ std::string dump_ct::type_to_string(const typet &type)
   std::string ret;
   typet t=type;
   cleanup_type(t);
+/*  if((t.id()==ID_union || t.id()==ID_struct) &&
+     t.find(ID_typedef).is_not_nil())
+    return id2string(t.get(ID_typedef));
+*/
   language->from_type(t, ret, ns);
   return ret;
 }
diff --git a/src/goto-instrument/dump_c_class.h b/src/goto-instrument/dump_c_class.h
index a84841ca9b9..3fba1c1b346 100644
--- a/src/goto-instrument/dump_c_class.h
+++ b/src/goto-instrument/dump_c_class.h
@@ -64,6 +64,8 @@ class dump_ct
   std::string type_to_string(const typet &type);
   std::string expr_to_string(const exprt &expr);
 
+  std::set<std::string> ignored_symbols;
+  void ignored_symbol_rec(const symbolt &symbol);
   bool ignore(const symbolt &symbol);
 
   static std::string indent(const unsigned n)
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index edcc18a3792..b9d4963d788 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -1882,7 +1882,7 @@ Function: goto_program2codet::cleanup_function_call
 \*******************************************************************/
 
 void goto_program2codet::cleanup_function_call(
-  const exprt &function,
+  exprt &function,
   code_function_callt::argumentst &arguments)
 {
   if(function.id()!=ID_symbol)
@@ -1890,6 +1890,12 @@ void goto_program2codet::cleanup_function_call(
 
   const symbol_exprt &fn=to_symbol_expr(function);
 
+  //clean function identifier
+  std::string name_str=id2string(function.get(ID_identifier));
+  size_t pos=name_str.find("$link");
+  if(pos!=std::string::npos)
+    function.set(ID_identifier,name_str.substr(0,pos));
+
   // don't edit function calls we might have introduced
   const symbolt *s;
   if(!ns.lookup(fn.get_identifier(), s))
diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h
index 02346e388ef..8ccf9d4d3e4 100644
--- a/src/goto-instrument/goto_program2code.h
+++ b/src/goto-instrument/goto_program2code.h
@@ -96,7 +96,7 @@ class goto_program2codet
   void cleanup_code(codet &code, const irep_idt parent_stmt);
 
   void cleanup_function_call(
-    const exprt &function,
+    exprt &function,
     code_function_callt::argumentst &arguments);
 
   void cleanup_code_block(
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index 88d2c435642..56bad4b0cff 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -144,6 +144,16 @@ void remove_internal_symbols(
     if(is_type)
     {
       // never EXPORTED by itself
+        // Without this code the symbol is lost when compiling with
+        // goto-cc
+        // So the problem with this approach is that this is per typedef
+        // we move the name of the typedef into the type it corresponds to
+        // e.g. will not elegantly work when more than one typedef for the same
+        // type. Instead we want to somehow whenever we find an expression
+        // that directly uses a typedef we want to record that that is the case
+        // so we can use the correct typedef
+#if 0
+#endif
     }
     else if(is_function)
     {