use a struct_tag to identify base classes

Author: Daniel Kroening

src/util/std_types.cpp

@@ -70,6 +70,35 @@ struct_union_typet::component_type(const irep_idt &component_name) const
   return c.type();
 }
 
+struct_tag_typet &struct_typet::baset::type()
+{
+  return to_struct_tag_type(exprt::type());
+}
+
+const struct_tag_typet &struct_typet::baset::type() const
+{
+  return to_struct_tag_type(exprt::type());
+}
+
+struct_typet::baset::baset(const struct_tag_typet &base) : exprt(ID_base, base)
+{
+}
+
+void struct_typet::add_base(const struct_tag_typet &base)
+{
+  bases().push_back(baset(base));
+}
+
+optionalt<struct_typet::baset> struct_typet::get_base(const irep_idt &id) const
+{
+  for(const auto &b : bases())
+  {
+    if(to_struct_tag_type(b.type()).get_identifier() == id)
+      return b;
+  }
+  return {};
+}
+
 /// Returns true if the struct is a prefix of \a other, i.e., if this struct
 /// has n components then the component types and names of this struct must
 /// match the first n components of \a other struct.

src/util/std_types.h

@@ -271,6 +271,8 @@ inline struct_union_typet &to_struct_union_type(typet &type)
   return static_cast<struct_union_typet &>(type);
 }
 
+class struct_tag_typet;
+
 /// Structure type, corresponds to C style structs
 class struct_typet:public struct_union_typet
 {
@@ -291,19 +293,9 @@ class struct_typet:public struct_union_typet
   class baset : public exprt
   {
   public:
-    symbol_typet &type()
-    {
-      return to_symbol_type(exprt::type());
-    }
-
-    const symbol_typet &type() const
-    {
-      return to_symbol_type(exprt::type());
-    }
-
-    explicit baset(const symbol_typet &base) : exprt(ID_base, base)
-    {
-    }
+    struct_tag_typet &type();
+    const struct_tag_typet &type() const;
+    explicit baset(const struct_tag_typet &base);
   };
 
   typedef std::vector<baset> basest;
@@ -322,23 +314,12 @@ class struct_typet:public struct_union_typet
 
   /// Add a base class/struct
   /// \param base: Type of case/class struct to be added.
-  void add_base(const symbol_typet &base)
-  {
-    bases().push_back(baset(base));
-  }
+  void add_base(const struct_tag_typet &base);
 
   /// Return the base with the given name, if exists.
   /// \param id The name of the base we are looking for.
   /// \return The base if exists.
-  optionalt<baset> get_base(const irep_idt &id) const
-  {
-    for(const auto &b : bases())
-    {
-      if(to_symbol_type(b.type()).get_identifier() == id)
-        return b;
-    }
-    return {};
-  }
+  optionalt<baset> get_base(const irep_idt &id) const;
 
   /// Test whether `id` is a base class/struct.
   /// \param id: symbol type name