Skip to content

Commit

Permalink
KNOWNBUG test for enum-range check inside LHS of an assignment
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
kroening committed Dec 23, 2024
1 parent c4aaafd commit 51b35ac
Show file tree
Hide file tree
Showing 2 changed files with 28 additions and 0 deletions.
17 changes: 17 additions & 0 deletions regression/cbmc/enum_is_in_range/enum_lhs.c
Original file line number Diff line number Diff line change
@@ -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;
}
11 changes: 11 additions & 0 deletions regression/cbmc/enum_is_in_range/enum_lhs.desc
Original file line number Diff line number Diff line change
@@ -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 comments on commit 51b35ac

Please sign in to comment.