Merge pull request #2926 from diffblue/struct-tag

Use struct tags

Author: tautschnig

src/ansi-c/c_typecheck_code.cpp

@@ -383,8 +383,12 @@ bool c_typecheck_baset::is_complete_type(const typet &type) const
   }
   else if(type.id()==ID_vector)
     return is_complete_type(type.subtype());
-  else if(type.id() == ID_symbol_type)
+  else if(
+    type.id() == ID_symbol_type || type.id() == ID_struct_tag ||
+    type.id() == ID_union_tag)
+  {
     return is_complete_type(follow(type));
+  }
 
   return true;
 }

src/ansi-c/c_typecheck_type.cpp

@@ -822,18 +822,17 @@ void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
 
   c_qualifierst original_qualifiers(type);
 
-  if(type.id() == ID_union)
-  {
-    union_tag_typet tag_type(identifier);
-    tag_type.add_source_location() = type.source_location();
-    type.swap(tag_type);
-  }
+  typet tag_type;
+
+  if(type.id() == ID_union || type.id() == ID_incomplete_union)
+    tag_type = union_tag_typet(identifier);
+  else if(type.id() == ID_struct || type.id() == ID_incomplete_struct)
+    tag_type = struct_tag_typet(identifier);
   else
-  {
-    symbol_typet symbol_type(identifier);
-    symbol_type.add_source_location() = type.source_location();
-    type.swap(symbol_type);
-  }
+    UNREACHABLE;
+
+  tag_type.add_source_location() = type.source_location();
+  type.swap(tag_type);
 
   original_qualifiers.write(type);
 }

src/goto-instrument/dump_c.cpp

@@ -322,11 +322,12 @@ void dump_ct::convert_compound(
     if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       convert_compound(symbol.type, unresolved, recursive, os);
   }
-  else if(type.id()==ID_c_enum_tag)
+  else if(
+    type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
+    type.id() == ID_union_tag)
   {
-    const symbolt &symbol=
-      ns.lookup(to_c_enum_tag_type(type).get_identifier());
-    DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
+    const symbolt &symbol = ns.lookup(to_tag_type(type));
+    DATA_INVARIANT(symbol.is_type, "tag expected to be type symbol");
 
     if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
       convert_compound(symbol.type, unresolved, recursive, os);
@@ -674,6 +675,13 @@ void dump_ct::collect_typedefs_rec(
       ns.lookup(to_symbol_type(type).get_identifier());
     collect_typedefs_rec(symbol.type, early, local_deps);
   }
+  else if(
+    type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
+    type.id() == ID_union_tag)
+  {
+    const symbolt &symbol = ns.lookup(to_tag_type(type));
+    collect_typedefs_rec(symbol.type, early, local_deps);
+  }
 
   const irep_idt &typedef_str=type.get(ID_C_typedef);
 

src/util/expr_initializer.cpp

@@ -291,17 +291,23 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   }
   else if(type_id==ID_struct_tag)
   {
-    return
-      expr_initializer_rec(
-        ns.follow_tag(to_struct_tag_type(type)),
-        source_location);
+    exprt result = expr_initializer_rec(
+      ns.follow_tag(to_struct_tag_type(type)), source_location);
+
+    // use the tag type
+    result.type() = type;
+
+    return result;
   }
   else if(type_id==ID_union_tag)
   {
-    return
-      expr_initializer_rec(
-        ns.follow_tag(to_union_tag_type(type)),
-        source_location);
+    exprt result = expr_initializer_rec(
+      ns.follow_tag(to_union_tag_type(type)), source_location);
+
+    // use the tag type
+    result.type() = type;
+
+    return result;
   }
   else if(type_id==ID_string)
   {

src/util/std_types.cpp

@@ -234,7 +234,9 @@ bool is_constant_or_has_constant_components(
   // we have to use the namespace to resolve to its definition:
   // struct t { const int a; };
   // struct t t1;
-  if(type.id() == ID_symbol_type)
+  if(type.id() == ID_symbol_type ||
+     type.id() == ID_struct_tag ||
+     type.id() == ID_union_tag)
   {
     const auto &resolved_type = ns.follow(type);
     return has_constant_components(resolved_type);