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 fcff91fCopy full SHA for fcff91f
regression/cbmc/enum_is_in_range/enum_lhs.c
@@ -0,0 +1,11 @@
1
+typedef enum { A = 1, B = 2 } my_enumt;
2
+int my_array[10];
3
+
4
+int main()
5
+{
6
+ // should fail
7
+ (my_enumt)3;
8
9
10
+ my_array[(my_enumt)4] = 10;
11
+}
regression/cbmc/enum_is_in_range/enum_lhs.desc
+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