Set enum underlying type from specified type

Author: danpoe

src/ansi-c/c_typecheck_type.cpp

@@ -1160,10 +1160,20 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
     throw 0;
   }
 
-  if(as_expr.find(ID_enum_underlying_type).is_not_nil())
+  const bool have_underlying_type =
+    type.find_type(ID_enum_underlying_type).is_not_nil();
+
+  if(have_underlying_type)
   {
-    warning().source_location = source_location;
-    warning() << "ignoring specification of underlying type for enum" << eom;
+    typecheck_type(type.add_type(ID_enum_underlying_type));
+
+    if(!is_signed_or_unsigned_bitvector(
+        static_cast<const typet &>(type.find(ID_enum_underlying_type))))
+    {
+      error().source_location = source_location;
+      error() << "underlying type for enum must be an integral type" << eom;
+      throw 0;
+    }
   }
 
   // enums start at zero;
@@ -1211,8 +1221,24 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
     if(value>max_value)
       max_value=value;
 
-    typet constant_type=
-      enum_constant_type(min_value, max_value);
+    typet constant_type;
+
+    if(have_underlying_type)
+    {
+      constant_type = type.find_type(ID_enum_underlying_type);
+      const auto &tmp = to_integer_bitvector_type(constant_type);
+
+      if(value < tmp.smallest() || value > tmp.largest())
+      {
+        error().source_location = v.source_location();
+        error() << "enum constant value cannot be represented with underlying type" << eom;
+        throw 0;
+      }
+    }
+    else
+    {
+      constant_type = enum_constant_type(min_value, max_value);
+    }
 
     v=from_integer(value, constant_type);
 
@@ -1245,8 +1271,16 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
   bool is_packed=type.get_bool(ID_C_packed);
 
   // We use a subtype to store the underlying type.
-  bitvector_typet underlying_type =
-    enum_underlying_type(min_value, max_value, is_packed);
+  bitvector_typet underlying_type(ID_nil);
+
+  if(have_underlying_type)
+  {
+    underlying_type = to_bitvector_type(type.find_type(ID_enum_underlying_type));
+  }
+  else
+  {
+    underlying_type = enum_underlying_type(min_value, max_value, is_packed);
+  }
 
   // Get the width to make the values have a bitvector type
   std::size_t width = underlying_type.get_width();