Add regression tests for enum underlying type specification feature

Author: danpoe

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