Merge pull request #8543 from diffblue/enum_lhs

KNOWNBUG test for enum-range check inside LHS of an assignment

Author: tautschnig

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;
+}

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.
+