From 6776f0cc59e6e726742669de6174873ab3e7e9a7 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 18 Jan 2022 09:54:31 +0000
Subject: [PATCH] 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().
---
 src/ansi-c/c_typecast.cpp                     |  8 +++---
 src/ansi-c/c_typecheck_expr.cpp               |  9 +++---
 src/ansi-c/c_typecheck_type.cpp               | 28 +++++++++----------
 src/ansi-c/expr2c.cpp                         |  5 ++--
 src/ansi-c/padding.cpp                        | 19 +++++++------
 src/cpp/cpp_typecheck_enum_type.cpp           |  4 +--
 src/goto-instrument/goto_program2code.cpp     |  4 ++-
 src/goto-programs/goto_trace.cpp              |  2 +-
 src/goto-programs/json_expr.cpp               | 13 +++++----
 src/goto-programs/xml_expr.cpp                | 13 +++++----
 .../c_bit_field_replacement_type.cpp          | 16 +++++------
 src/solvers/smt2/smt2_conv.cpp                |  8 ++----
 src/util/arith_tools.cpp                      | 16 +++++------
 src/util/c_types.h                            | 24 +++++++++++++++-
 src/util/pointer_offset_size.cpp              |  5 ++--
 src/util/simplify_expr.cpp                    |  4 +--
 src/util/simplify_expr_floatbv.cpp            |  4 +--
 src/util/simplify_utils.cpp                   |  6 ++--
 18 files changed, 109 insertions(+), 79 deletions(-)

diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp
index abe6ac6a9d8..c9b6565ecb6 100644
--- 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
index 90f49e4faff..8815156e1ba 100644
--- 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
index 2c61f525b0d..de24cd80caf 100644
--- 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
index b4aff20aa69..0a7b8c4a7cc 100644
--- 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
index 4feb7afdbf5..2d27452bebd 100644
--- 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
index 9639ae578f8..3134d986e36 100644
--- 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
index 0ff9d5d2ed9..8f02dfddaf4 100644
--- 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
index 85140c26ad7..708a4cd9bd4 100644
--- 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
index 795e42972b4..de0a6dda3c8 100644
--- 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
index df33dde42af..32059b1eff1 100644
--- 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
index 6c11b1dffa2..1e52d54bdfc 100644
--- 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
index 6288a2b1151..29a6c68df18 100644
--- 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)
   {
@@ -2772,10 +2772,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
index 67d20a18687..b306c4bef4d 100644
--- 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
index 6eda9c9fd45..7fe0752f210 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -25,7 +25,17 @@ class c_bit_field_typet : public bitvector_typet
     subtype().swap(_subtype);
   }
 
-  // These have a sub-type
+  // These have a sub-type. The preferred way to access it
+  // are the underlying_type methods.
+  const typet &underlying_type() const
+  {
+    return subtype();
+  }
+
+  typet &underlying_type()
+  {
+    return subtype();
+  }
 };
 
 /// Check whether a reference to a typet is a \ref c_bit_field_typet.
@@ -256,6 +266,18 @@ class c_enum_typet : public type_with_subtypet
   {
     set(ID_incomplete, true);
   }
+
+  // The preferred way to access the subtype
+  // are the underlying_type methods.
+  const typet &underlying_type() const
+  {
+    return subtype();
+  }
+
+  typet &underlying_type()
+  {
+    return subtype();
+  }
 };
 
 /// Check whether a reference to a typet is a \ref c_enum_typet.
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index d6be1f65240..99a9f2decb0 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -178,7 +178,8 @@ pointer_offset_bits(const typet &type, const namespacet &ns)
   }
   else if(type.id()==ID_c_enum)
   {
-    return mp_integer(to_bitvector_type(to_c_enum_type(type).subtype()).get_width());
+    return mp_integer(
+      to_bitvector_type(to_c_enum_type(type).underlying_type()).get_width());
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -451,7 +452,7 @@ optionalt<exprt> size_of_expr(const typet &type, const namespacet &ns)
   else if(type.id()==ID_c_enum)
   {
     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();
     std::size_t bytes=width/8;
     if(bytes*8!=width)
       bytes++;
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 9afb82cc23d..14c7a00fe71 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -1269,7 +1269,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     else if(op_type_id==ID_c_enum_tag) // enum to int
     {
       const typet &base_type =
-        ns.follow_tag(to_c_enum_tag_type(op_type)).subtype();
+        ns.follow_tag(to_c_enum_tag_type(op_type)).underlying_type();
       if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
       {
         // enum constants use the representation of their base type
@@ -1280,7 +1280,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     }
     else if(op_type_id==ID_c_enum) // enum to int
     {
-      const typet &base_type=to_c_enum_type(op_type).subtype();
+      const typet &base_type = to_c_enum_type(op_type).underlying_type();
       if(base_type.id()==ID_signedbv || base_type.id()==ID_unsignedbv)
       {
         // enum constants use the representation of their base type
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index dd836d10b51..f7fdd2952b3 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -233,8 +233,8 @@ simplify_exprt::simplify_floatbv_typecast(const floatbv_typecast_exprt &expr)
       {
         // go through underlying type
         const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(src_type));
-        exprt simplified_typecast =
-          simplify_expr(typecast_exprt(casted_expr, enum_type.subtype()), ns);
+        exprt simplified_typecast = simplify_expr(
+          typecast_exprt(casted_expr, enum_type.underlying_type()), ns);
         if(simplified_typecast.is_constant())
         {
           floatbv_typecast_exprt new_floatbv_typecast_expr = expr;
diff --git a/src/util/simplify_utils.cpp b/src/util/simplify_utils.cpp
index 3199a6cd57a..50255c1a3f1 100644
--- a/src/util/simplify_utils.cpp
+++ b/src/util/simplify_utils.cpp
@@ -235,8 +235,8 @@ optionalt<exprt> bits2expr(
   }
   else if(type.id() == ID_c_enum)
   {
-    auto val =
-      bits2expr(bits, to_c_enum_type(type).subtype(), little_endian, ns);
+    auto val = bits2expr(
+      bits, to_c_enum_type(type).underlying_type(), little_endian, ns);
     if(val.has_value())
     {
       val->type() = type;
@@ -443,7 +443,7 @@ expr2bits(const exprt &expr, bool little_endian, const namespacet &ns)
     else if(type.id() == ID_c_enum)
     {
       return expr2bits(
-        constant_exprt(value, to_c_enum_type(type).subtype()),
+        constant_exprt(value, to_c_enum_type(type).underlying_type()),
         little_endian,
         ns);
     }