Mark already-typechecked types as such

src/cpp/cpp_typecheck_code.cpp

@@ -384,6 +384,9 @@ void cpp_typecheckt::typecheck_decl(codet &code)
     return;
   }
 
+  // mark as 'already typechecked'
+  make_already_typechecked(type);
+
   codet new_code(ID_decl_block);
   new_code.reserve_operands(declaration.declarators().size());
 

src/cpp/cpp_typecheck_declaration.cpp

@@ -129,6 +129,10 @@ void cpp_typecheckt::convert_non_template_declaration(
   if(!is_typedef)
     elaborate_class_template(declaration_type);
 
+  // mark as 'already typechecked'
+  if(!declaration.declarators().empty())
+    make_already_typechecked(declaration_type);
+
   // Special treatment for anonymous unions
   if(declaration.declarators().empty() &&
      follow(declaration.type()).get_bool(ID_C_is_anonymous))

src/cpp/cpp_typecheck_type.cpp

@@ -260,6 +260,10 @@ void cpp_typecheckt::typecheck_type(typet &type)
   else if(type.id()==ID_nullptr)
   {
   }
+  else if(type.id()==ID_already_typechecked)
+  {
+    c_typecheck_baset::typecheck_type(type);
+  }
   else
   {
     error().source_location=type.source_location();

src/cpp/cpp_util.h

@@ -17,7 +17,7 @@ exprt cpp_symbol_expr(const symbolt &symbol);
 
 inline void already_typechecked(irept &irep)
 {
-  exprt tmp("already_typechecked");
+  exprt tmp(ID_already_typechecked);
   tmp.copy_to_operands(static_cast<exprt &>(irep));
   irep.swap(tmp);
 }