Merge pull request #6588 from diffblue/c_enum_underlying_type

tautschnig · web-flow · commit 195458a0c9ad · 2022-01-19T13:20:46.000+01:00
c_enum_typet::underlying_type() and c_bitfield_typet::underlying_type()
diff --git a/src/ansi-c/c_typecast.cpp b/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());
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/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;
 
diff --git a/src/ansi-c/c_typecheck_type.cpp b/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;
   }
 
diff --git a/src/ansi-c/expr2c.cpp b/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 += '{';
 
diff --git a/src/ansi-c/padding.cpp b/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)
diff --git a/src/cpp/cpp_typecheck_enum_type.cpp b/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;
diff --git a/src/goto-instrument/goto_program2code.cpp b/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)
diff --git a/src/goto-programs/goto_trace.cpp b/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();
diff --git a/src/goto-programs/json_expr.cpp b/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);
     }
diff --git a/src/goto-programs/xml_expr.cpp b/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";
diff --git a/src/solvers/flattening/c_bit_field_replacement_type.cpp b/src/solvers/flattening/c_bit_field_replacement_type.cpp
@@ -16,22 +16,22 @@ typet c_bit_field_replacement_type(
   const c_bit_field_typet &src,
   const namespacet &ns)
 {
-  const typet &subtype=src.subtype();
+  const typet &underlying_type = src.underlying_type();
 
-  if(subtype.id()==ID_unsignedbv ||
-     subtype.id()==ID_signedbv ||
-     subtype.id()==ID_c_bool)
+  if(
+    underlying_type.id() == ID_unsignedbv ||
+    underlying_type.id() == ID_signedbv || underlying_type.id() == ID_c_bool)
   {
-    bitvector_typet result=to_bitvector_type(subtype);
+    bitvector_typet result = to_bitvector_type(underlying_type);
     result.set_width(src.get_width());
     return std::move(result);
   }
   else
   {
-    PRECONDITION(subtype.id() == ID_c_enum_tag);
+    PRECONDITION(underlying_type.id() == ID_c_enum_tag);
 
-    const typet &sub_subtype=
-      ns.follow_tag(to_c_enum_tag_type(subtype)).subtype();
+    const typet &sub_subtype =
+      ns.follow_tag(to_c_enum_tag_type(underlying_type)).underlying_type();
 
     PRECONDITION(
       sub_subtype.id() == ID_signedbv || sub_subtype.id() == ID_unsignedbv);
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -931,7 +931,7 @@ std::string smt2_convt::type2id(const typet &type) const
   }
   else if(type.id()==ID_c_enum_tag)
   {
-    return type2id(ns.follow_tag(to_c_enum_tag_type(type)).subtype());
+    return type2id(ns.follow_tag(to_c_enum_tag_type(type)).underlying_type());
   }
   else if(type.id() == ID_pointer)
   {
@@ -2775,10 +2775,8 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
 
       // We first convert to 'underlying type'
       floatbv_typecast_exprt tmp=expr;
-      tmp.op()=
-        typecast_exprt(
-          src,
-          ns.follow_tag(to_c_enum_tag_type(src_type)).subtype());
+      tmp.op() = typecast_exprt(
+        src, ns.follow_tag(to_c_enum_tag_type(src_type)).underlying_type());
       convert_floatbv_typecast(tmp);
     }
     else
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
@@ -56,14 +56,14 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   }
   else if(type_id==ID_c_enum)
   {
-    const typet &subtype=to_c_enum_type(type).subtype();
-    if(subtype.id()==ID_signedbv)
+    const typet &underlying_type = to_c_enum_type(type).underlying_type();
+    if(underlying_type.id() == ID_signedbv)
     {
       const auto width = to_signedbv_type(type).get_width();
       int_value = bvrep2integer(value, width, true);
       return false;
     }
-    else if(subtype.id()==ID_unsignedbv)
+    else if(underlying_type.id() == ID_unsignedbv)
     {
       const auto width = to_unsignedbv_type(type).get_width();
       int_value = bvrep2integer(value, width, false);
@@ -74,19 +74,19 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)
   {
     const auto &c_bit_field_type = to_c_bit_field_type(type);
     const auto width = c_bit_field_type.get_width();
-    const typet &subtype = c_bit_field_type.subtype();
+    const typet &underlying_type = c_bit_field_type.underlying_type();
 
-    if(subtype.id()==ID_signedbv)
+    if(underlying_type.id() == ID_signedbv)
     {
       int_value = bvrep2integer(value, width, true);
       return false;
     }
-    else if(subtype.id()==ID_unsignedbv)
+    else if(underlying_type.id() == ID_unsignedbv)
     {
       int_value = bvrep2integer(value, width, false);
       return false;
     }
-    else if(subtype.id() == ID_c_bool)
+    else if(underlying_type.id() == ID_c_bool)
     {
       int_value = bvrep2integer(value, width, false);
       return false;
@@ -129,7 +129,7 @@ constant_exprt from_integer(
   else if(type_id==ID_c_enum)
   {
     const std::size_t width =
-      to_bitvector_type(to_c_enum_type(type).subtype()).get_width();
+      to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();
     return constant_exprt(integer2bvrep(int_value, width), type);
   }
   else if(type_id==ID_c_bool)
diff --git a/src/util/c_types.h b/src/util/c_types.h
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp

Original file line number	Diff line number	Diff line change
`@@ -1849,13 +1849,14 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr)`
`1849`	`1849`	`}`
`1850`	`1850`
`1851`	`1851`	`// increment/decrement on underlying type`
`1852`		`- to_unary_expr(expr).op() = typecast_exprt(op0, enum_type.subtype());`
`1853`		`- expr.type() = enum_type.subtype();`
	`1852`	`+ to_unary_expr(expr).op() =`
	`1853`	`+ typecast_exprt(op0, enum_type.underlying_type());`
	`1854`	`+ expr.type() = enum_type.underlying_type();`
`1854`	`1855`	`}`
`1855`	`1856`	`else if(type0.id() == ID_c_bit_field)`
`1856`	`1857`	`{`
`1857`	`1858`	`// promote to underlying type`
`1858`		`- typet underlying_type = to_c_bit_field_type(type0).subtype();`
	`1859`	`+ typet underlying_type = to_c_bit_field_type(type0).underlying_type();`
`1859`	`1860`	`to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type);`
`1860`	`1861`	`expr.type()=underlying_type;`
`1861`	`1862`	`}`
`@@ -3057,7 +3058,7 @@ exprt c_typecheck_baset::do_special_functions(`
`3057`	`3058`
`3058`	`3059`	`// use underlying type for bit fields`
`3059`	`3060`	`if(type.id() == ID_c_bit_field)`
`3060`		`- type = to_c_bit_field_type(type).subtype();`
	`3061`	`+ type = to_c_bit_field_type(type).underlying_type();`
`3061`	`3062`
`3062`	`3063`	`unsigned type_number;`
`3063`	`3064`
Original file line number	Diff line number	Diff line change
`@@ -134,8 +134,8 @@ void c_typecheck_baset::typecheck_type(typet &type)`
`134`	`134`	`// but we'll try to interpret it the GCC way`
`135`	`135`	`if(underlying_type.id()==ID_c_enum_tag)`
`136`	`136`	`{`
`137`		`- underlying_type=`
`138`		`- follow_tag(to_c_enum_tag_type(underlying_type)).subtype();`
	`137`	`+ underlying_type =`
	`138`	`+ follow_tag(to_c_enum_tag_type(underlying_type)).underlying_type();`
`139`	`139`
`140`	`140`	`assert(underlying_type.id()==ID_signedbv \|\|`
`141`	`141`	`underlying_type.id()==ID_unsignedbv);`
`@@ -1480,7 +1480,7 @@ void c_typecheck_baset::typecheck_c_enum_tag_type(c_enum_tag_typet &type)`
`1480`	`1480`
`1481`	`1481`	`void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)`
`1482`	`1482`	`{`
`1483`		`- typecheck_type(type.subtype());`
	`1483`	`+ typecheck_type(type.underlying_type());`
`1484`	`1484`
`1485`	`1485`	`mp_integer i;`
`1486`	`1486`
`@@ -1508,28 +1508,28 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)`
`1508`	`1508`	`type.remove(ID_size);`
`1509`	`1509`	`}`
`1510`	`1510`
`1511`		`- const typet &subtype = type.subtype();`
	`1511`	`+ const typet &underlying_type = type.underlying_type();`
`1512`	`1512`
`1513`	`1513`	`std::size_t sub_width=0;`
`1514`	`1514`
`1515`		`- if(subtype.id()==ID_bool)`
	`1515`	`+ if(underlying_type.id() == ID_bool)`
`1516`	`1516`	`{`
`1517`	`1517`	`// This is the 'proper' bool.`
`1518`	`1518`	`sub_width=1;`
`1519`	`1519`	`}`
`1520`		`- else if(subtype.id()==ID_signedbv \|\|`
`1521`		`- subtype.id()==ID_unsignedbv \|\|`
`1522`		`- subtype.id()==ID_c_bool)`
	`1520`	`+ else if(`
	`1521`	`+ underlying_type.id() == ID_signedbv \|\|`
	`1522`	`+ underlying_type.id() == ID_unsignedbv \|\| underlying_type.id() == ID_c_bool)`
`1523`	`1523`	`{`
`1524`		`- sub_width=to_bitvector_type(subtype).get_width();`
	`1524`	`+ sub_width = to_bitvector_type(underlying_type).get_width();`
`1525`	`1525`	`}`
`1526`		`- else if(subtype.id()==ID_c_enum_tag)`
	`1526`	`+ else if(underlying_type.id() == ID_c_enum_tag)`
`1527`	`1527`	`{`
`1528`	`1528`	`// These point to an enum, which has a sub-subtype,`
`1529`	`1529`	`// which may be smaller or larger than int, and we thus have`
`1530`	`1530`	`// to check.`
`1531`	`1531`	`const auto &c_enum_type =`
`1532`		`- to_c_enum_type(follow_tag(to_c_enum_tag_type(subtype)));`
	`1532`	`+ to_c_enum_type(follow_tag(to_c_enum_tag_type(underlying_type)));`
`1533`	`1533`
`1534`	`1534`	`if(c_enum_type.is_incomplete())`
`1535`	`1535`	`{`
`@@ -1538,13 +1538,13 @@ void c_typecheck_baset::typecheck_c_bit_field_type(c_bit_field_typet &type)`
`1538`	`1538`	`throw 0;`
`1539`	`1539`	`}`
`1540`	`1540`
`1541`		`- sub_width = to_bitvector_type(c_enum_type.subtype()).get_width();`
	`1541`	`+ sub_width = to_bitvector_type(c_enum_type.underlying_type()).get_width();`
`1542`	`1542`	`}`
`1543`	`1543`	`else`
`1544`	`1544`	`{`
`1545`	`1545`	`error().source_location=type.source_location();`
`1546`		`- error() << "bit field with non-integer type: "`
`1547`		`- << to_string(subtype) << eom;`
	`1546`	`+ error() << "bit field with non-integer type: " << to_string(underlying_type)`
	`1547`	`+ << eom;`
`1548`	`1548`	`throw 0;`
`1549`	`1549`	`}`
`1550`	`1550`
Original file line number	Diff line number	Diff line change
`@@ -104,28 +104,29 @@ mp_integer alignment(const typet &type, const namespacet &ns)`
`104`	`104`	`static optionalt<std::size_t>`
`105`	`105`	`underlying_width(const c_bit_field_typet &type, const namespacet &ns)`
`106`	`106`	`{`
`107`		`- const typet &subtype = type.subtype();`
	`107`	`+ const typet &underlying_type = type.underlying_type();`
`108`	`108`
`109`		`- if(subtype.id() == ID_bool)`
	`109`	`+ if(underlying_type.id() == ID_bool)`
`110`	`110`	`{`
`111`	`111`	`// This is the 'proper' bool.`
`112`	`112`	`return 1;`
`113`	`113`	`}`
`114`	`114`	`else if(`
`115`		`- subtype.id() == ID_signedbv \|\| subtype.id() == ID_unsignedbv \|\|`
`116`		`- subtype.id() == ID_c_bool)`
	`115`	`+ underlying_type.id() == ID_signedbv \|\|`
	`116`	`+ underlying_type.id() == ID_unsignedbv \|\| underlying_type.id() == ID_c_bool)`
`117`	`117`	`{`
`118`		`- return to_bitvector_type(subtype).get_width();`
	`118`	`+ return to_bitvector_type(underlying_type).get_width();`
`119`	`119`	`}`
`120`		`- else if(subtype.id() == ID_c_enum_tag)`
	`120`	`+ else if(underlying_type.id() == ID_c_enum_tag)`
`121`	`121`	`{`
`122`	`122`	`// These point to an enum, which has a sub-subtype,`
`123`	`123`	`// which may be smaller or larger than int, and we thus have`
`124`	`124`	`// to check.`
`125`		`- const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(subtype));`
	`125`	`+ const auto &c_enum_type =`
	`126`	`+ ns.follow_tag(to_c_enum_tag_type(underlying_type));`
`126`	`127`
`127`	`128`	`if(!c_enum_type.is_incomplete())`
`128`		`- return to_bitvector_type(c_enum_type.subtype()).get_width();`
	`129`	`+ return to_bitvector_type(c_enum_type.underlying_type()).get_width();`
`129`	`130`	`else`
`130`	`131`	`return {};`
`131`	`132`	`}`
`@@ -352,7 +353,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)`
`352`	`353`
`353`	`354`	`if(it_type.id()==ID_c_bit_field)`
`354`	`355`	`{`
`355`		`- a=alignment(to_c_bit_field_type(it_type).subtype(), ns);`
	`356`	`+ a = alignment(to_c_bit_field_type(it_type).underlying_type(), ns);`
`356`	`357`
`357`	`358`	`// A zero-width bit-field causes alignment to the base-type.`
`358`	`359`	`if(to_c_bit_field_type(it_type).get_width()==0)`
Original file line number	Diff line number	Diff line change
`@@ -38,7 +38,7 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol)`
`38`	`38`	`{`
`39`	`39`	`exprt &value = static_cast<exprt &>(component.add(ID_value));`
`40`	`40`	`typecheck_expr(value);`
`41`		`- implicit_typecast(value, c_enum_type.subtype());`
	`41`	`+ implicit_typecast(value, c_enum_type.underlying_type());`
`42`	`42`	`make_constant(value);`
`43`	`43`	`if(to_integer(to_constant_expr(value), i))`
`44`	`44`	`{`
`@@ -48,7 +48,7 @@ void cpp_typecheckt::typecheck_enum_body(symbolt &enum_symbol)`
`48`	`48`	`}`
`49`	`49`	`}`
`50`	`50`
`51`		`- exprt value_expr=from_integer(i, c_enum_type.subtype());`
	`51`	`+ exprt value_expr = from_integer(i, c_enum_type.underlying_type());`
`52`	`52`	`value_expr.type()=enum_tag_type; // override type`
`53`	`53`
`54`	`54`	`symbolt symbol;`
Original file line number	Diff line number	Diff line change
`@@ -1604,7 +1604,9 @@ void goto_program2codet::remove_const(typet &type)`
`1604`	`1604`	`remove_const(it->type());`
`1605`	`1605`	`}`
`1606`	`1606`	`else if(type.id() == ID_c_bit_field)`
`1607`		`- to_c_bit_field_type(type).subtype().remove(ID_C_constant);`
	`1607`	`+ {`
	`1608`	`+ to_c_bit_field_type(type).underlying_type().remove(ID_C_constant);`
	`1609`	`+ }`
`1608`	`1610`	`}`
`1609`	`1611`
`1610`	`1612`	`static bool has_labels(const codet &code)`
Original file line number	Diff line number	Diff line change
`@@ -54,8 +54,8 @@ xmlt xml(const typet &type, const namespacet &ns)`
`54`	`54`	`}`
`55`	`55`	`else if(type.id() == ID_c_enum_tag)`
`56`	`56`	`{`
`57`		`- // we return the base type`
`58`		`- return xml(ns.follow_tag(to_c_enum_tag_type(type)).subtype(), ns);`
	`57`	`+ // we return the underlying type`
	`58`	`+ return xml(ns.follow_tag(to_c_enum_tag_type(type)).underlying_type(), ns);`
`59`	`59`	`}`
`60`	`60`	`else if(type.id() == ID_fixedbv)`
`61`	`61`	`{`
`@@ -148,9 +148,10 @@ xmlt xml(const exprt &expr, const namespacet &ns)`
`148`	`148`	`result.set_attribute("binary", integer2binary(i, width));`
`149`	`149`	`result.set_attribute("width", width);`
`150`	`150`
`151`		`- const typet &underlying_type = type.id() == ID_c_bit_field`
`152`		`- ? to_c_bit_field_type(type).subtype()`
`153`		`- : type;`
	`151`	`+ const typet &underlying_type =`
	`152`	`+ type.id() == ID_c_bit_field`
	`153`	`+ ? to_c_bit_field_type(type).underlying_type()`
	`154`	`+ : type;`
`154`	`155`
`155`	`156`	`bool is_signed = underlying_type.id() == ID_signedbv;`
`156`	`157`
`@@ -174,7 +175,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)`
`174`	`175`	`else if(type.id() == ID_c_enum)`
`175`	`176`	`{`
`176`	`177`	`const auto width =`
`177`		`- to_bitvector_type(to_c_enum_type(type).subtype()).get_width();`
	`178`	`+ to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();`
`178`	`179`
`179`	`180`	`const auto integer_value = bvrep2integer(value, width, false);`
`180`	`181`	`result.name = "integer";`
Original file line number	Diff line number	Diff line change
`@@ -931,7 +931,7 @@ std::string smt2_convt::type2id(const typet &type) const`
`931`	`931`	`}`
`932`	`932`	`else if(type.id()==ID_c_enum_tag)`
`933`	`933`	`{`
`934`		`- return type2id(ns.follow_tag(to_c_enum_tag_type(type)).subtype());`
	`934`	`+ return type2id(ns.follow_tag(to_c_enum_tag_type(type)).underlying_type());`
`935`	`935`	`}`
`936`	`936`	`else if(type.id() == ID_pointer)`
`937`	`937`	`{`
`@@ -2775,10 +2775,8 @@ void smt2_convt::convert_floatbv_typecast(const floatbv_typecast_exprt &expr)`
`2775`	`2775`
`2776`	`2776`	`// We first convert to 'underlying type'`
`2777`	`2777`	`floatbv_typecast_exprt tmp=expr;`
`2778`		`- tmp.op()=`
`2779`		`- typecast_exprt(`
`2780`		`- src,`
`2781`		`- ns.follow_tag(to_c_enum_tag_type(src_type)).subtype());`
	`2778`	`+ tmp.op() = typecast_exprt(`
	`2779`	`+ src, ns.follow_tag(to_c_enum_tag_type(src_type)).underlying_type());`
`2782`	`2780`	`convert_floatbv_typecast(tmp);`
`2783`	`2781`	`}`
`2784`	`2782`	`else`
Original file line number	Diff line number	Diff line change
`@@ -56,14 +56,14 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`56`	`56`	`}`
`57`	`57`	`else if(type_id==ID_c_enum)`
`58`	`58`	`{`
`59`		`- const typet &subtype=to_c_enum_type(type).subtype();`
`60`		`- if(subtype.id()==ID_signedbv)`
	`59`	`+ const typet &underlying_type = to_c_enum_type(type).underlying_type();`
	`60`	`+ if(underlying_type.id() == ID_signedbv)`
`61`	`61`	`{`
`62`	`62`	`const auto width = to_signedbv_type(type).get_width();`
`63`	`63`	`int_value = bvrep2integer(value, width, true);`
`64`	`64`	`return false;`
`65`	`65`	`}`
`66`		`- else if(subtype.id()==ID_unsignedbv)`
	`66`	`+ else if(underlying_type.id() == ID_unsignedbv)`
`67`	`67`	`{`
`68`	`68`	`const auto width = to_unsignedbv_type(type).get_width();`
`69`	`69`	`int_value = bvrep2integer(value, width, false);`
`@@ -74,19 +74,19 @@ bool to_integer(const constant_exprt &expr, mp_integer &int_value)`
`74`	`74`	`{`
`75`	`75`	`const auto &c_bit_field_type = to_c_bit_field_type(type);`
`76`	`76`	`const auto width = c_bit_field_type.get_width();`
`77`		`- const typet &subtype = c_bit_field_type.subtype();`
	`77`	`+ const typet &underlying_type = c_bit_field_type.underlying_type();`
`78`	`78`
`79`		`- if(subtype.id()==ID_signedbv)`
	`79`	`+ if(underlying_type.id() == ID_signedbv)`
`80`	`80`	`{`
`81`	`81`	`int_value = bvrep2integer(value, width, true);`
`82`	`82`	`return false;`
`83`	`83`	`}`
`84`		`- else if(subtype.id()==ID_unsignedbv)`
	`84`	`+ else if(underlying_type.id() == ID_unsignedbv)`
`85`	`85`	`{`
`86`	`86`	`int_value = bvrep2integer(value, width, false);`
`87`	`87`	`return false;`
`88`	`88`	`}`
`89`		`- else if(subtype.id() == ID_c_bool)`
	`89`	`+ else if(underlying_type.id() == ID_c_bool)`
`90`	`90`	`{`
`91`	`91`	`int_value = bvrep2integer(value, width, false);`
`92`	`92`	`return false;`
`@@ -129,7 +129,7 @@ constant_exprt from_integer(`
`129`	`129`	`else if(type_id==ID_c_enum)`
`130`	`130`	`{`
`131`	`131`	`const std::size_t width =`
`132`		`- to_bitvector_type(to_c_enum_type(type).subtype()).get_width();`
	`132`	`+ to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width();`
`133`	`133`	`return constant_exprt(integer2bvrep(int_value, width), type);`
`134`	`134`	`}`
`135`	`135`	`else if(type_id==ID_c_bool)`