further support for union_tag and struct_tag

Author: Daniel Kroening

src/ansi-c/c_typecheck_type.cpp

@@ -93,6 +93,11 @@ void c_typecheck_baset::typecheck_type(typet &type)
     typecheck_symbol_type(to_symbol_type(type));
   else if(type.id() == ID_typedef_type)
     typecheck_typedef_type(type);
+  else if(type.id() == ID_struct_tag ||
+          type.id() == ID_union_tag)
+  {
+    // nothing to do, these stay as is
+  }
   else if(type.id()==ID_vector)
     typecheck_vector_type(to_vector_type(type));
   else if(type.id()==ID_custom_unsignedbv ||

src/cpp/cpp_typecheck_type.cpp

@@ -189,6 +189,12 @@ void cpp_typecheckt::typecheck_type(typet &type)
   else if(type.id() == ID_symbol_type)
   {
   }
+  else if(type.id() == ID_struct_tag)
+  {
+  }
+  else if(type.id() == ID_union_tag)
+  {
+  }
   else if(type.id()==ID_constructor ||
           type.id()==ID_destructor)
   {

src/goto-symex/goto_symex_state.cpp

@@ -760,7 +760,10 @@ void goto_symex_statet::rename_address(
 
       // type might not have been renamed in case of nesting of
       // structs and pointers/arrays
-      if(member_expr.struct_op().type().id() != ID_symbol_type)
+      if(
+        member_expr.struct_op().type().id() != ID_symbol_type &&
+        member_expr.struct_op().type().id() != ID_struct_tag &&
+        member_expr.struct_op().type().id() != ID_union_tag)
       {
         const struct_union_typet &su_type=
           to_struct_union_type(member_expr.struct_op().type());
@@ -845,8 +848,19 @@ void goto_symex_statet::rename(
   }
   else if(type.id() == ID_symbol_type)
   {
-    const symbolt &symbol=
-      ns.lookup(to_symbol_type(type).get_identifier());
+    const symbolt &symbol = ns.lookup(to_symbol_type(type));
+    type = symbol.type;
+    rename(type, l1_identifier, ns, level);
+  }
+  else if(type.id() == ID_union_tag)
+  {
+    const symbolt &symbol = ns.lookup(to_union_tag_type(type));
+    type = symbol.type;
+    rename(type, l1_identifier, ns, level);
+  }
+  else if(type.id() == ID_struct_tag)
+  {
+    const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
     type=symbol.type;
     rename(type, l1_identifier, ns, level);
   }