Merge pull request #2697 from diffblue/union_tag

Introduce union tag type

Author: tautschnig

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 ||
@@ -815,11 +820,21 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
     }
   }
 
-  symbol_typet symbol_type(identifier);
-  symbol_type.add_source_location()=type.source_location();
-
   c_qualifierst original_qualifiers(type);
-  type.swap(symbol_type);
+
+  if(type.id() == ID_union)
+  {
+    union_tag_typet tag_type(identifier);
+    tag_type.add_source_location() = type.source_location();
+    type.swap(tag_type);
+  }
+  else
+  {
+    symbol_typet symbol_type(identifier);
+    symbol_type.add_source_location() = type.source_location();
+    type.swap(symbol_type);
+  }
+
   original_qualifiers.write(type);
 }
 

src/cpp/cpp_typecheck_compound_type.cpp

@@ -135,6 +135,7 @@ void cpp_typecheckt::typecheck_compound_type(
   cpp_scopet *dest_scope=nullptr;
   bool has_body=type.find(ID_body).is_not_nil();
   bool tag_only_declaration=type.get_bool(ID_C_tag_only_declaration);
+  bool is_union = type.id() == ID_union;
 
   if(!has_tag)
   {
@@ -263,10 +264,20 @@ void cpp_typecheckt::typecheck_compound_type(
     }
   }
 
-  // create type symbol
-  symbol_typet symbol_type(symbol_name);
-  qualifiers.write(symbol_type);
-  type.swap(symbol_type);
+  if(is_union)
+  {
+    // create union tag
+    union_tag_typet tag_type(symbol_name);
+    qualifiers.write(tag_type);
+    type.swap(tag_type);
+  }
+  else
+  {
+    // create type symbol
+    symbol_typet symbol_type(symbol_name);
+    qualifiers.write(symbol_type);
+    type.swap(symbol_type);
+  }
 }
 
 void cpp_typecheckt::typecheck_compound_declarator(

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