c_enum_typet::underlying_type() and c_bitfield_typet::underlying_type()

This introduces c_enum_typet::underlying_type() and
c_bitfield_typet::underlying_type(), to be used instead of typet::subtype().

Author: kroening

src/ansi-c/c_typecast.cpp

@@ -365,17 +365,17 @@ c_typecastt::c_typet c_typecastt::get_c_type(
     // of bits given
     typet underlying_type;
 
-    if(bit_field_type.subtype().id() == ID_c_enum_tag)
+    if(bit_field_type.underlying_type().id() == ID_c_enum_tag)
     {
       const auto &followed =
-        ns.follow_tag(to_c_enum_tag_type(bit_field_type.subtype()));
+        ns.follow_tag(to_c_enum_tag_type(bit_field_type.underlying_type()));
       if(followed.is_incomplete())
         return INT;
       else
-        underlying_type = followed.subtype();
+        underlying_type = followed.underlying_type();
     }
     else
-      underlying_type = bit_field_type.subtype();
+      underlying_type = bit_field_type.underlying_type();
 
     const bitvector_typet new_type(
       underlying_type.id(), bit_field_type.get_width());

src/ansi-c/c_typecheck_expr.cpp

@@ -1849,13 +1849,14 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)
       }
 
       // increment/decrement on underlying type
-      to_unary_expr(expr).op() = typecast_exprt(op0, enum_type.subtype());
-      expr.type() = enum_type.subtype();
+      to_unary_expr(expr).op() =
+        typecast_exprt(op0, enum_type.underlying_type());
+      expr.type() = enum_type.underlying_type();
     }
     else if(type0.id() == ID_c_bit_field)
     {
       // promote to underlying type
-      typet underlying_type = to_c_bit_field_type(type0).subtype();
+      typet underlying_type = to_c_bit_field_type(type0).underlying_type();
       to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);
       expr.type()=underlying_type;
     }
@@ -3057,7 +3058,7 @@ exprt c_typecheck_baset::do_special_functions(
 
     // use underlying type for bit fields
     if(type.id() == ID_c_bit_field)
-      type = to_c_bit_field_type(type).subtype();
+      type = to_c_bit_field_type(type).underlying_type();
 
     unsigned type_number;
 

src/ansi-c/c_typecheck_type.cpp

@@ -134,8 +134,8 @@ void c_typecheck_baset::typecheck_type(typet &type)
     // but we'll try to interpret it the GCC way
     if(underlying_type.id()==ID_c_enum_tag)
     {
-      underlying_type=
-        follow_tag(to_c_enum_tag_type(underlying_type)).subtype();
+      underlying_type =
+        follow_tag(to_c_enum_tag_type(underlying_type)).underlying_type();
 
       assert(underlying_type.id()==ID_signedbv ||
              underlying_type.id()==ID_unsignedbv);
@@ -1480,7 +1480,7 @@ void c_typecheck_baset::typecheck_c_enum_tag_type(c_enum_tag_typet &type)
 
 void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
 {
-  typecheck_type(type.subtype());
+  typecheck_type(type.underlying_type());
 
   mp_integer i;
 
@@ -1508,28 +1508,28 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
     type.remove(ID_size);
   }
 
-  const typet &subtype = type.subtype();
+  const typet &underlying_type = type.underlying_type();
 
   std::size_t sub_width=0;
 
-  if(subtype.id()==ID_bool)
+  if(underlying_type.id() == ID_bool)
   {
     // This is the 'proper' bool.
     sub_width=1;
   }
-  else if(subtype.id()==ID_signedbv ||
-          subtype.id()==ID_unsignedbv ||
-          subtype.id()==ID_c_bool)
+  else if(
+    underlying_type.id() == ID_signedbv ||
+    underlying_type.id() == ID_unsignedbv || underlying_type.id() == ID_c_bool)
   {
-    sub_width=to_bitvector_type(subtype).get_width();
+    sub_width = to_bitvector_type(underlying_type).get_width();
   }
-  else if(subtype.id()==ID_c_enum_tag)
+  else if(underlying_type.id() == ID_c_enum_tag)
   {
     // These point to an enum, which has a sub-subtype,
     // which may be smaller or larger than int, and we thus have
     // to check.
     const auto &c_enum_type =
-      to_c_enum_type(follow_tag(to_c_enum_tag_type(subtype)));
+      to_c_enum_type(follow_tag(to_c_enum_tag_type(underlying_type)));
 
     if(c_enum_type.is_incomplete())
     {
@@ -1538,13 +1538,13 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)
       throw 0;
     }
 
-    sub_width = to_bitvector_type(c_enum_type.subtype()).get_width();
+    sub_width = to_bitvector_type(c_enum_type.underlying_type()).get_width();
   }
   else
   {
     error().source_location=type.source_location();
-    error() << "bit field with non-integer type: "
-            << to_string(subtype) << eom;
+    error() << "bit field with non-integer type: " << to_string(underlying_type)
+            << eom;
     throw 0;
   }
 

src/ansi-c/expr2c.cpp

@@ -412,8 +412,9 @@ std::string expr2ct::convert_rec(
     if(!to_c_enum_type(src).is_incomplete())
     {
       const c_enum_typet &c_enum_type = to_c_enum_type(src);
-      const bool is_signed = c_enum_type.subtype().id() == ID_signedbv;
-      const auto width = to_bitvector_type(c_enum_type.subtype()).get_width();
+      const bool is_signed = c_enum_type.underlying_type().id() == ID_signedbv;
+      const auto width =
+        to_bitvector_type(c_enum_type.underlying_type()).get_width();
 
       result += '{';
 

src/ansi-c/padding.cpp

@@ -104,28 +104,29 @@ mp_integer alignment(const typet &type, const namespacet &ns)
 static optionalt<std::size_t>
 underlying_width(const c_bit_field_typet &type, const namespacet &ns)
 {
-  const typet &subtype = type.subtype();
+  const typet &underlying_type = type.underlying_type();
 
-  if(subtype.id() == ID_bool)
+  if(underlying_type.id() == ID_bool)
   {
     // This is the 'proper' bool.
     return 1;
   }
   else if(
-    subtype.id() == ID_signedbv || subtype.id() == ID_unsignedbv ||
-    subtype.id() == ID_c_bool)
+    underlying_type.id() == ID_signedbv ||
+    underlying_type.id() == ID_unsignedbv || underlying_type.id() == ID_c_bool)
   {
-    return to_bitvector_type(subtype).get_width();
+    return to_bitvector_type(underlying_type).get_width();
   }
-  else if(subtype.id() == ID_c_enum_tag)
+  else if(underlying_type.id() == ID_c_enum_tag)
   {
     // These point to an enum, which has a sub-subtype,
     // which may be smaller or larger than int, and we thus have
     // to check.
-    const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));
+    const auto &c_enum_type =
+      ns.follow_tag(to_c_enum_tag_type(underlying_type));
 
     if(!c_enum_type.is_incomplete())
-      return to_bitvector_type(c_enum_type.subtype()).get_width();
+      return to_bitvector_type(c_enum_type.underlying_type()).get_width();
     else
       return {};
   }
@@ -352,7 +353,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
 
     if(it_type.id()==ID_c_bit_field)
     {
-      a=alignment(to_c_bit_field_type(it_type).subtype(), ns);
+      a = alignment(to_c_bit_field_type(it_type).underlying_type(), ns);
 
       // A zero-width bit-field causes alignment to the base-type.
       if(to_c_bit_field_type(it_type).get_width()==0)

src/cpp/cpp_typecheck_enum_type.cpp

@@ -38,7 +38,7 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol)
     {
       exprt &value = static_cast<exprt &>(component.add(ID_value));
       typecheck_expr(value);
-      implicit_typecast(value, c_enum_type.subtype());
+      implicit_typecast(value, c_enum_type.underlying_type());
       make_constant(value);
       if(to_integer(to_constant_expr(value), i))
       {
@@ -48,7 +48,7 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol)
       }
     }
 
-    exprt value_expr=from_integer(i, c_enum_type.subtype());
+    exprt value_expr = from_integer(i, c_enum_type.underlying_type());
     value_expr.type()=enum_tag_type; // override type
 
     symbolt symbol;

src/goto-instrument/goto_program2code.cpp

@@ -1604,7 +1604,9 @@ void goto_program2codet::remove_const(typet &type)
       remove_const(it->type());
   }
   else if(type.id() == ID_c_bit_field)
-    to_c_bit_field_type(type).subtype().remove(ID_C_constant);
+  {
+    to_c_bit_field_type(type).underlying_type().remove(ID_C_constant);
+  }
 }
 
 static bool has_labels(const codet &code)

src/goto-programs/goto_trace.cpp

@@ -170,7 +170,7 @@ static std::string numeric_representation(
 
   const typet &underlying_type =
     expr_type.id() == ID_c_enum_tag
-      ? ns.follow_tag(to_c_enum_tag_type(expr_type)).subtype()
+      ? ns.follow_tag(to_c_enum_tag_type(expr_type)).underlying_type()
       : expr_type;
 
   const irep_idt &value = expr.get_value();

src/goto-programs/json_expr.cpp

@@ -132,8 +132,9 @@ json_objectt json(const typet &type, const namespacet &ns, const irep_idt &mode)
   }
   else if(type.id() == ID_c_enum_tag)
   {
-    // we return the base type
-    return json(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns, mode);
+    // we return the underlying type
+    return json(
+      ns.follow_tag(to_c_enum_tag_type(type)).underlying_type(), ns, mode);
   }
   else if(type.id() == ID_fixedbv)
   {
@@ -206,7 +207,8 @@ static std::string binary(const constant_exprt &src)
 {
   std::size_t width;
   if(src.type().id() == ID_c_enum)
-    width = to_bitvector_type(to_c_enum_type(src.type()).subtype()).get_width();
+    width = to_bitvector_type(to_c_enum_type(src.type()).underlying_type())
+              .get_width();
   else
     width = to_bitvector_type(src.type()).get_width();
   const auto int_val = bvrep2integer(src.get_value(), width, false);
@@ -236,7 +238,8 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
       lang = std::unique_ptr<languaget>(get_default_language());
 
     const typet &underlying_type =
-      type.id() == ID_c_bit_field ? to_c_bit_field_type(type).subtype() : type;
+      type.id() == ID_c_bit_field ? to_c_bit_field_type(type).underlying_type()
+                                  : type;
 
     std::string type_string;
     bool error = lang->from_type(underlying_type, type_string, ns);
@@ -262,7 +265,7 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
       result["name"] = json_stringt("integer");
       result["binary"] = json_stringt(binary(constant_expr));
       result["width"] = json_numbert(std::to_string(
-        to_bitvector_type(to_c_enum_type(type).subtype()).get_width()));
+        to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width()));
       result["type"] = json_stringt("enum");
       result["data"] = json_stringt(value_string);
     }

src/goto-programs/xml_expr.cpp

@@ -54,8 +54,8 @@ xmlt xml(const typet &type, const namespacet &ns)
   }
   else if(type.id() == ID_c_enum_tag)
   {
-    // we return the base type
-    return xml(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);
+    // we return the underlying type
+    return xml(ns.follow_tag(to_c_enum_tag_type(type)).underlying_type(), ns);
   }
   else if(type.id() == ID_fixedbv)
   {
@@ -148,9 +148,10 @@ xmlt xml(const exprt &expr, const namespacet &ns)
       result.set_attribute("binary", integer2binary(i, width));
       result.set_attribute("width", width);
 
-      const typet &underlying_type = type.id() == ID_c_bit_field
-                                       ? to_c_bit_field_type(type).subtype()
-                                       : type;
+      const typet &underlying_type =
+        type.id() == ID_c_bit_field
+          ? to_c_bit_field_type(type).underlying_type()
+          : type;
 
       bool is_signed = underlying_type.id() == ID_signedbv;
 
@@ -174,7 +175,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
     else if(type.id() == ID_c_enum)
     {
       const auto width =
-        to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
+        to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
 
       const auto integer_value = bvrep2integer(value, width, false);
       result.name = "integer";