@@ -1160,10 +1160,20 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
1160
1160
throw 0 ;
1161
1161
}
1162
1162
1163
- if (as_expr.find (ID_enum_underlying_type).is_not_nil ())
1163
+ const bool have_underlying_type =
1164
+ type.find_type (ID_enum_underlying_type).is_not_nil ();
1165
+
1166
+ if (have_underlying_type)
1164
1167
{
1165
- warning ().source_location = source_location;
1166
- warning () << " ignoring specification of underlying type for enum" << eom;
1168
+ typecheck_type (type.add_type (ID_enum_underlying_type));
1169
+
1170
+ if (!is_signed_or_unsigned_bitvector (
1171
+ static_cast <const typet &>(type.find (ID_enum_underlying_type))))
1172
+ {
1173
+ error ().source_location = source_location;
1174
+ error () << " underlying type for enum must be an integral type" << eom;
1175
+ throw 0 ;
1176
+ }
1167
1177
}
1168
1178
1169
1179
// enums start at zero;
@@ -1211,8 +1221,26 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
1211
1221
if (value>max_value)
1212
1222
max_value=value;
1213
1223
1214
- typet constant_type=
1215
- enum_constant_type (min_value, max_value);
1224
+ typet constant_type;
1225
+
1226
+ if (have_underlying_type)
1227
+ {
1228
+ constant_type = type.find_type (ID_enum_underlying_type);
1229
+ const auto &tmp = to_integer_bitvector_type (constant_type);
1230
+
1231
+ if (value < tmp.smallest () || value > tmp.largest ())
1232
+ {
1233
+ error ().source_location = v.source_location ();
1234
+ error ()
1235
+ << " enum constant value cannot be represented with underlying type"
1236
+ << eom;
1237
+ throw 0 ;
1238
+ }
1239
+ }
1240
+ else
1241
+ {
1242
+ constant_type = enum_constant_type (min_value, max_value);
1243
+ }
1216
1244
1217
1245
v=from_integer (value, constant_type);
1218
1246
@@ -1245,8 +1273,17 @@ void c_typecheck_baset::typecheck_c_enum_type(typet &type)
1245
1273
bool is_packed=type.get_bool (ID_C_packed);
1246
1274
1247
1275
// We use a subtype to store the underlying type.
1248
- bitvector_typet underlying_type =
1249
- enum_underlying_type (min_value, max_value, is_packed);
1276
+ bitvector_typet underlying_type (ID_nil);
1277
+
1278
+ if (have_underlying_type)
1279
+ {
1280
+ underlying_type =
1281
+ to_bitvector_type (type.find_type (ID_enum_underlying_type));
1282
+ }
1283
+ else
1284
+ {
1285
+ underlying_type = enum_underlying_type (min_value, max_value, is_packed);
1286
+ }
1250
1287
1251
1288
// Get the width to make the values have a bitvector type
1252
1289
std::size_t width = underlying_type.get_width ();
0 commit comments