We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent c4aaafd commit 7aeea9eCopy full SHA for 7aeea9e
regression/cbmc/enum_is_in_range/enum_lhs.c
@@ -0,0 +1,13 @@
1
+typedef enum my_enum { A = 1, B = 2 };
2
+int my_array[10];
3
+
4
+int main()
5
+{
6
+ // should fail
7
+ (enum my_enumt)3;
8
9
10
+ my_array[(enum my_enumt)4] = 10;
11
12
+ return 0;
13
+}
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 10 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.
0 commit comments