Skip to content

Commit fbee5c1

Browse files
committed
KNOWNBUG test for enum-range check inside LHS of an assignment
85b90f3 has added a check that enum-typed expressions correspond to one of the enum constants. This adds a test that should fail an enum-range check inside the LHS of an assignment.
1 parent c4aaafd commit fbee5c1

File tree

2 files changed

+28
-0
lines changed

2 files changed

+28
-0
lines changed

Diff for: regression/cbmc/enum_is_in_range/enum_lhs.c

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
typedef enum my_enum
2+
{
3+
A = 1,
4+
B = 2
5+
};
6+
int my_array[10];
7+
8+
int main()
9+
{
10+
// should fail
11+
(enum my_enumt)3;
12+
13+
// should fail
14+
my_array[(enum my_enumt)4] = 10;
15+
16+
return 0;
17+
}

Diff for: regression/cbmc/enum_is_in_range/enum_lhs.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
KNOWNBUG
2+
enum_lhs.c
3+
--enum-range-check
4+
^\[main\.enum-range-check\.2\] line 14 enum range check in \(my_enumt\)4: FAILURE$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
The conversion to enum on the LHS should fail the enum-range check, but
10+
doesn't.
11+

0 commit comments

Comments
 (0)