Set enum underlying type from specified type

Author: danpoe

src/ansi-c/c_typecheck_type.cpp

@@ -1160,10 +1160,24 @@ 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));
+
+    const typet &underlying_type =
+      static_cast<const typet &>(type.find(ID_enum_underlying_type));
+
+    if(!is_signed_or_unsigned_bitvector(underlying_type))
+    {
+      std::ostringstream msg;
+      msg << source_location << ": non-integral type '"
+          << underlying_type.get(ID_C_c_type)
+          << "' is an invalid underlying type";
+      throw invalid_source_file_exceptiont{msg.str()};
+    }
   }
 
   // enums start at zero;
@@ -1211,8 +1225,27 @@ 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())
+      {
+        std::ostringstream msg;
+        msg
+          << v.source_location()
+          << ": enumerator value is not representable in the underlying type '"
+          << constant_type.get(ID_C_c_type) << "'";
+        throw invalid_source_file_exceptiont{msg.str()};
+      }
+    }
+    else
+    {
+      constant_type = enum_constant_type(min_value, max_value);
+    }
 
     v=from_integer(value, constant_type);
 
@@ -1245,8 +1278,17 @@ 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();