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/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);
   }

src/util/replace_symbol.cpp

@@ -197,6 +197,28 @@ bool replace_symbolt::replace(typet &dest) const
       result=false;
     }
   }
+  else if(dest.id() == ID_union_tag)
+  {
+    type_mapt::const_iterator it =
+      type_map.find(to_union_tag_type(dest).get_identifier());
+
+    if(it != type_map.end())
+    {
+      dest = it->second;
+      result = false;
+    }
+  }
+  else if(dest.id() == ID_struct_tag)
+  {
+    type_mapt::const_iterator it =
+      type_map.find(to_struct_tag_type(dest).get_identifier());
+
+    if(it != type_map.end())
+    {
+      dest = it->second;
+      result = false;
+    }
+  }
   else if(dest.id()==ID_array)
   {
     array_typet &array_type=to_array_type(dest);