Correctly interpret underlying type specification of enums

regression/ansi-c/enum9/test.desc

@@ -3,8 +3,6 @@ main.c
 --verbosity 2
 ^EXIT=0$
 ^SIGNAL=0$
-(main.c:1:\d+)|(main.c\(1\)): warning: ignoring specification of underlying type for enum
-(main.c:6:\d+)|(main.c\(6\)): warning: ignoring specification of underlying type for enum
 (main.c:13:\d+)|(main.c\(13\)): warning: ignoring specification of underlying type for enum
 (main.c:14:\d+)|(main.c\(14\)): warning: ignoring specification of underlying type for enum
 (main.c:19:\d+)|(main.c\(19\)): warning: ignoring specification of underlying type for enum

regression/cbmc/enum_underlying_type_01/main.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+enum enum1
+{
+  E1
+};
+
+enum enum2 : signed char
+{
+  E2
+};
+
+typedef signed char signed_char_t;
+
+enum enum3 : signed_char_t
+{
+  E3
+};
+
+int main()
+{
+  assert(sizeof(int) != sizeof(signed char));
+  assert(sizeof(enum enum1) == sizeof(int));
+  assert(sizeof(enum enum2) == sizeof(signed char));
+  assert(sizeof(enum enum3) == sizeof(signed char));
+
+  enum enum2 e2 = 0xff;
+  assert(e2 == -1);
+
+  enum enum3 e3 = 0xff;
+  assert(e3 == -1);
+}

regression/cbmc/enum_underlying_type_01/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Checks that the underlying type specification of an enum is correctly
+interpreted, i.e., the size and signedness of the integral type chosen for the
+enum is the one specified. Also checks that it works with typedef'd types.

regression/cbmc/enum_underlying_type_02/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+enum enum1 : unsigned char
+{
+  E1 = 256
+};
+
+int main()
+{
+}

regression/cbmc/enum_underlying_type_02/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file main.c line \d+: enumerator value is not representable in the underlying type 'unsigned_char'$
+--
+^warning: ignoring
+--
+Checks that values that cannot be represented by the specified underlying type
+are rejected

regression/cbmc/enum_underlying_type_03/main.c

@@ -0,0 +1,10 @@
+#include <assert.h>
+
+enum enum1 : float
+{
+  E1
+};
+
+int main()
+{
+}

regression/cbmc/enum_underlying_type_03/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+^file main.c line \d+: non-integral type 'float' is an invalid underlying type$
+--
+^warning: ignoring
+--
+Checks that non-integral types are rejected

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();

src/ansi-c/parser.y

@@ -1840,6 +1840,9 @@ enum_name:
 basic_type_name_list:
     basic_type_name
   | basic_type_name_list basic_type_name
+  {
+    $$ = merge($1, $2);
+  }
 
 enum_underlying_type:
     basic_type_name_list