use union_tag_type instead of symbol_type

Author: Daniel Kroening

src/ansi-c/c_typecheck_type.cpp

@@ -93,6 +93,9 @@ 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_union_tag)
+  {
+  }
   else if(type.id()==ID_vector)
     typecheck_vector_type(to_vector_type(type));
   else if(type.id()==ID_custom_unsignedbv ||
@@ -795,12 +798,24 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
     }
   }
 
-  symbol_typet symbol_type(identifier);
-  symbol_type.add_source_location()=type.source_location();
+  if(type.id() == ID_union)
+  {
+    union_tag_typet tag_type(identifier);
+    tag_type.add_source_location() = type.source_location();
+
+    c_qualifierst original_qualifiers(type);
+    type.swap(tag_type);
+    original_qualifiers.write(type);
+  }
+  else
+  {
+    symbol_typet symbol_type(identifier);
+    symbol_type.add_source_location() = type.source_location();
 
-  c_qualifierst original_qualifiers(type);
-  type.swap(symbol_type);
-  original_qualifiers.write(type);
+    c_qualifierst original_qualifiers(type);
+    type.swap(symbol_type);
+    original_qualifiers.write(type);
+  }
 }
 
 void c_typecheck_baset::typecheck_compound_body(

src/goto-symex/goto_symex_state.cpp

@@ -760,7 +760,8 @@ 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)
+      if(member_expr.struct_op().type().id()!=ID_symbol &&
+         member_expr.struct_op().type().id()!=ID_union_tag)
       {
         const struct_union_typet &su_type=
           to_struct_union_type(member_expr.struct_op().type());