remove symbol_typet [blocks: #4056]

src/analyses/invariant_propagation.cpp

@@ -191,8 +191,6 @@ bool invariant_propagationt::check_type(const typet &type) const
     return false;
   else if(type.id()==ID_array)
     return false;
-  else if(type.id() == ID_symbol_type)
-    return check_type(ns.follow(type));
   else if(type.id()==ID_unsignedbv ||
           type.id()==ID_signedbv)
     return true;

src/ansi-c/c_typecheck_base.cpp

@@ -415,8 +415,6 @@ void c_typecheck_baset::typecheck_redefinition_non_type(
        to_array_type(final_new).size().is_not_nil() &&
        final_old.subtype()==final_new.subtype())
     {
-      // we don't do symbol types for arrays anymore
-      PRECONDITION(old_symbol.type.id() != ID_symbol_type);
       old_symbol.type=new_symbol.type;
     }
     else if(

src/ansi-c/c_typecheck_initializer.cpp

@@ -504,7 +504,6 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
     const typet &type=designator.back().subtype;
     const typet &full_type=follow(type);
-    CHECK_RETURN(full_type.id() != ID_symbol_type);
 
     // do we initialize a scalar?
     if(full_type.id()!=ID_struct &&

src/ansi-c/expr2c.cpp

@@ -440,43 +440,6 @@ std::string expr2ct::convert_rec(
   {
     return convert_array_type(src, qualifiers, declarator);
   }
-  else if(src.id() == ID_symbol_type)
-  {
-    symbol_typet symbolic_type=to_symbol_type(src);
-    const irep_idt &typedef_identifer=symbolic_type.get(ID_typedef);
-
-    // Providing we have a valid identifer, we can just use that rather than
-    // trying to find the concrete type
-    if(typedef_identifer!="")
-    {
-      return q+id2string(typedef_identifer)+d;
-    }
-    else
-    {
-      const typet &followed=ns.follow(src);
-
-      if(followed.id()==ID_struct)
-      {
-        std::string dest=q+"struct";
-        const irep_idt &tag=to_struct_type(followed).get_tag();
-        if(tag!="")
-          dest+=" "+id2string(tag);
-        dest+=d;
-        return dest;
-      }
-      else if(followed.id()==ID_union)
-      {
-        std::string dest=q+"union";
-        const irep_idt &tag=to_union_type(followed).get_tag();
-        if(tag!="")
-          dest+=" "+id2string(tag);
-        dest+=d;
-        return dest;
-      }
-      else
-        return convert_rec(followed, new_qualifiers, declarator);
-    }
-  }
   else if(src.id()==ID_struct_tag)
   {
     const struct_tag_typet &struct_tag_type=

src/cpp/cpp_typecheck_compound_type.cpp

@@ -894,7 +894,6 @@ void cpp_typecheckt::typecheck_friend_declaration(
 
     // TODO
     //    typecheck_type(ftype);
-    //    assert(ftype.id()==ID_symbol_type);
     //    symbol.type.add("ID_C_friends").move_to_sub(ftype);
 
     return;

src/cpp/cpp_typecheck_constructor.cpp

@@ -442,8 +442,8 @@ void cpp_typecheckt::check_member_initializers(
       for(const auto &b : bases)
       {
         if(
-          to_symbol_type(member_type).get_identifier() ==
-          to_symbol_type(b.type()).get_identifier())
+          to_struct_tag_type(member_type).get_identifier() ==
+          to_struct_tag_type(b.type()).get_identifier())
         {
           ok=true;
           break;
@@ -483,14 +483,15 @@ void cpp_typecheckt::check_member_initializers(
         if(c.type().id() != ID_struct_tag)
           continue;
 
-        const symbolt &symb = lookup(to_symbol_type(c.type()).get_identifier());
+        const symbolt &symb =
+          lookup(to_struct_tag_type(c.type()).get_identifier());
         if(symb.type.id()!=ID_struct)
           break;
 
         // check for a direct parent
         for(const auto &b : bases)
         {
-          if(symb.name == to_symbol_type(b.type()).get_identifier())
+          if(symb.name == to_struct_tag_type(b.type()).get_identifier())
           {
             ok=true;
             break;
@@ -513,7 +514,7 @@ void cpp_typecheckt::check_member_initializers(
         {
           if(
             member_type.get(ID_identifier) ==
-            to_symbol_type(b.type()).get_identifier())
+            to_struct_tag_type(b.type()).get_identifier())
           {
             ok=true;
             break;
@@ -638,8 +639,8 @@ void cpp_typecheckt::full_member_initialization(
           break;
 
         if(
-          to_symbol_type(b.type()).get_identifier() ==
-          to_symbol_type(member_type).get_identifier())
+          to_struct_tag_type(b.type()).get_identifier() ==
+          to_struct_tag_type(member_type).get_identifier())
         {
           final_initializers.move_to_sub(initializer);
           found=true;

src/cpp/cpp_typecheck_template.cpp

@@ -808,7 +808,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
 
     if(cpp_declarator_converter.is_typedef)
     {
-      parameter = exprt(ID_type, symbol_typet(symbol.name));
+      parameter = exprt(ID_type, struct_tag_typet(symbol.name));
       parameter.type().add_source_location()=declaration.find_location();
     }
     else

src/goto-instrument/dump_c.cpp

@@ -61,18 +61,18 @@ void dump_ct::operator()(std::ostream &os)
     {
       typet &type=it2->type();
 
-      if(type.id() == ID_symbol_type && type.get_bool(ID_C_transparent_union))
+      if(type.id() == ID_union_tag && type.get_bool(ID_C_transparent_union))
       {
-        symbolt new_type_sym=
-          ns.lookup(to_symbol_type(type).get_identifier());
+        symbolt new_type_sym =
+          ns.lookup(to_union_tag_type(type).get_identifier());
 
         new_type_sym.name=id2string(new_type_sym.name)+"$transparent";
         new_type_sym.type.set(ID_C_transparent_union, true);
 
         // we might have it already, in which case this has no effect
         symbols_transparent.add(new_type_sym);
 
-        to_symbol_type(type).set_identifier(new_type_sym.name);
+        to_union_tag_type(type).set_identifier(new_type_sym.name);
         type.remove(ID_C_transparent_union);
       }
     }
@@ -181,9 +181,16 @@ void dump_ct::operator()(std::ostream &os)
 
         if(type_id==ID_c_enum)
           convert_compound_enum(symbol.type, global_decl_stream);
+        else if(type_id == ID_struct)
+        {
+          global_decl_stream << type_to_string(struct_tag_typet{symbol.name})
+                             << ";\n\n";
+        }
         else
-          global_decl_stream << type_to_string(symbol_typet(symbol.name))
+        {
+          global_decl_stream << type_to_string(union_tag_typet{symbol.name})
                              << ";\n\n";
+        }
       }
     }
     else if(symbol.is_static_lifetime && symbol.type.id()!=ID_code)
@@ -297,10 +304,12 @@ void dump_ct::convert_compound_declaration(
     return;
 
   // do compound type body
-  if(symbol.type.id()==ID_struct ||
-     symbol.type.id()==ID_union ||
-     symbol.type.id()==ID_c_enum)
-    convert_compound(symbol.type, symbol_typet(symbol.name), true, os_body);
+  if(symbol.type.id() == ID_struct)
+    convert_compound(symbol.type, struct_tag_typet(symbol.name), true, os_body);
+  else if(symbol.type.id() == ID_union)
+    convert_compound(symbol.type, union_tag_typet(symbol.name), true, os_body);
+  else if(symbol.type.id() == ID_c_enum)
+    convert_compound(symbol.type, c_enum_tag_typet(symbol.name), true, os_body);
 }
 
 void dump_ct::convert_compound(
@@ -309,16 +318,7 @@ void dump_ct::convert_compound(
   bool recursive,
   std::ostream &os)
 {
-  if(type.id() == ID_symbol_type)
-  {
-    const symbolt &symbol=
-      ns.lookup(to_symbol_type(type).get_identifier());
-    DATA_INVARIANT(symbol.is_type, "symbol expected to be type symbol");
-
-    if(!system_symbols.is_symbol_internal_symbol(symbol, system_headers))
-      convert_compound(symbol.type, unresolved, recursive, os);
-  }
-  else if(
+  if(
     type.id() == ID_c_enum_tag || type.id() == ID_struct_tag ||
     type.id() == ID_union_tag)
   {
@@ -346,7 +346,13 @@ void dump_ct::convert_compound(
           it!=syms.end();
           ++it)
       {
-        symbol_typet s_type(*it);
+        const symbolt &type_symbol = ns.lookup(*it);
+        irep_idt tag_kind =
+          type_symbol.type.id() == ID_c_enum
+            ? ID_c_enum_tag
+            : (type_symbol.type.id() == ID_union ? ID_union_tag
+                                                 : ID_struct_tag);
+        tag_typet s_type(tag_kind, *it);
         convert_compound(s_type, s_type, recursive, os);
       }
     }
@@ -378,7 +384,7 @@ void dump_ct::convert_compound(
     UNREACHABLE;
     /*
     assert(parent_it->id() == ID_base);
-    assert(parent_it->get(ID_type) == ID_symbol_type);
+    assert(parent_it->get(ID_type) == ID_struct_tag);
 
     const irep_idt &base_id=
       parent_it->find(ID_type).get(ID_identifier);
@@ -657,12 +663,6 @@ void dump_ct::collect_typedefs_rec(
   {
     collect_typedefs_rec(type.subtype(), early, local_deps);
   }
-  else if(type.id() == ID_symbol_type)
-  {
-    const symbolt &symbol=
-      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)
@@ -1183,7 +1183,11 @@ void dump_ct::insert_local_type_decls(
     // a comment block ...
     std::ostringstream os_body;
     os_body << *it << " */\n";
-    convert_compound(type, symbol_typet(*it), false, os_body);
+    irep_idt tag_kind =
+      type.id() == ID_c_enum
+        ? ID_c_enum_tag
+        : (type.id() == ID_union ? ID_union_tag : ID_struct_tag);
+    convert_compound(type, tag_typet(tag_kind, *it), false, os_body);
     os_body << "/*";
 
     code_skipt skip;

src/goto-instrument/goto_program2code.cpp

@@ -1410,31 +1410,22 @@ goto_programt::const_targett goto_program2codet::convert_catch(
 
 void goto_program2codet::add_local_types(const typet &type)
 {
-  if(type.id() == ID_symbol_type)
+  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
   {
     const typet &full_type=ns.follow(type);
 
-    if(full_type.id()==ID_pointer ||
-       full_type.id()==ID_array)
-    {
-      add_local_types(full_type.subtype());
-    }
-    else if(full_type.id()==ID_struct ||
-            full_type.id()==ID_union)
-    {
-      const irep_idt &identifier=to_symbol_type(type).get_identifier();
-      const symbolt &symbol=ns.lookup(identifier);
+    const irep_idt &identifier = to_tag_type(type).get_identifier();
+    const symbolt &symbol = ns.lookup(identifier);
 
-      if(symbol.location.get_function().empty() ||
-         !type_names_set.insert(identifier).second)
-        return;
+    if(
+      symbol.location.get_function().empty() ||
+      !type_names_set.insert(identifier).second)
+      return;
 
-      for(const auto &c : to_struct_union_type(full_type).components())
-        add_local_types(c.type());
+    for(const auto &c : to_struct_union_type(full_type).components())
+      add_local_types(c.type());
 
-      assert(!identifier.empty());
-      type_names.push_back(identifier);
-    }
+    type_names.push_back(identifier);
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -1633,9 +1624,9 @@ void goto_program2codet::remove_const(typet &type)
   if(type.get_bool(ID_C_constant))
     type.remove(ID_C_constant);
 
-  if(type.id() == ID_symbol_type)
+  if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
   {
-    const irep_idt &identifier=to_symbol_type(type).get_identifier();
+    const irep_idt &identifier = to_tag_type(type).get_identifier();
     if(!const_removed.insert(identifier).second)
       return;
 
@@ -1833,8 +1824,9 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
     if(no_typecast)
       return;
 
-    DATA_INVARIANT(expr.type().id() == ID_symbol_type,
-                   "type of union/struct expressions");
+    DATA_INVARIANT(
+      expr.type().id() == ID_struct_tag || expr.type().id() == ID_union_tag,
+      "union/struct expressions should have a tag type");
 
     const typet &t=expr.type();
 

src/goto-instrument/nondet_volatile.cpp

@@ -16,19 +16,16 @@ Date: September 2011
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
-bool is_volatile(
-  const symbol_tablet &symbol_table,
-  const typet &src)
+static bool is_volatile(const namespacet &ns, const typet &src)
 {
   if(src.get_bool(ID_C_volatile))
     return true;
 
-  if(src.id()==ID_symbol)
+  if(
+    src.id() == ID_struct_tag || src.id() == ID_union_tag ||
+    src.id() == ID_c_enum_tag)
   {
-    symbol_tablet::symbolst::const_iterator s_it=
-      symbol_table.symbols.find(to_symbol_type(src).get_identifier());
-    assert(s_it!=symbol_table.symbols.end());
-    return is_volatile(symbol_table, s_it->second.type);
+    return is_volatile(ns, ns.follow(src));
   }
 
   return false;
@@ -42,7 +39,8 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
   if(expr.id()==ID_symbol ||
      expr.id()==ID_dereference)
   {
-    if(is_volatile(symbol_table, expr.type()))
+    const namespacet ns(symbol_table);
+    if(is_volatile(ns, expr.type()))
     {
       typet t=expr.type();
       t.remove(ID_C_volatile);

src/goto-programs/destructor.cpp

@@ -19,9 +19,9 @@ code_function_callt get_destructor(
   const namespacet &ns,
   const typet &type)
 {
-  if(type.id() == ID_symbol_type)
+  if(type.id() == ID_struct_tag)
   {
-    return get_destructor(ns, ns.follow(type));
+    return get_destructor(ns, ns.follow_tag(to_struct_tag_type(type)));
   }
   else if(type.id()==ID_struct)
   {

src/goto-programs/interpreter.cpp

@@ -1030,9 +1030,9 @@ mp_integer interpretert::get_size(const typet &type)
     }
     return subtype_size;
   }
-  else if(type.id() == ID_symbol_type || type.id() == ID_struct_tag)
+  else if(type.id() == ID_struct_tag)
   {
-    return get_size(ns.follow(type));
+    return get_size(ns.follow_tag(to_struct_tag_type(type)));
   }
 
   return 1;

src/goto-programs/json_expr.cpp

@@ -97,9 +97,6 @@ static exprt simplify_json_expr(const exprt &src)
 /// \return a json object
 json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
 {
-  if(type.id() == ID_symbol_type)
-    return json(ns.follow(type), ns, mode);
-
   json_objectt result;
 
   if(type.id() == ID_unsignedbv)