diff --git a/regression/cbmc/enum_is_in_range/enum_lhs.c b/regression/cbmc/enum_is_in_range/enum_lhs.c new file mode 100644 index 00000000000..6ff7dd47ee1 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_lhs.c @@ -0,0 +1,17 @@ +typedef enum my_enum +{ + A = 1, + B = 2 +}; +int my_array[10]; + +int main() +{ + // should fail + (enum my_enumt)3; + + // should fail + my_array[(enum my_enumt)4] = 10; + + return 0; +} diff --git a/regression/cbmc/enum_is_in_range/enum_lhs.desc b/regression/cbmc/enum_is_in_range/enum_lhs.desc new file mode 100644 index 00000000000..2860a11d4c5 --- /dev/null +++ b/regression/cbmc/enum_is_in_range/enum_lhs.desc @@ -0,0 +1,11 @@ +KNOWNBUG +enum_lhs.c +--enum-range-check +^\[main\.enum-range-check\.2\] line 14 enum range check in \(my_enumt\)4: FAILURE$ +^EXIT=10$ +^SIGNAL=0$ +-- +-- +The conversion to enum on the LHS should fail the enum-range check, but +doesn't. +