From fbee5c1f9f48b12987589ba334d2dd43671192b3 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 23 Dec 2024 17:03:47 +0000
Subject: [PATCH] KNOWNBUG test for enum-range check inside LHS of an
 assignment

85b90f304ba90ca83d4f1f3c78e28293c51c057b 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.
---
 regression/cbmc/enum_is_in_range/enum_lhs.c    | 17 +++++++++++++++++
 regression/cbmc/enum_is_in_range/enum_lhs.desc | 11 +++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 regression/cbmc/enum_is_in_range/enum_lhs.c
 create mode 100644 regression/cbmc/enum_is_in_range/enum_lhs.desc

diff --git a/regression/cbmc/enum_is_in_range/enum_lhs.c b/regression/cbmc/enum_is_in_range/enum_lhs.c
new file mode 100644
index 00000000000..6ff7dd47ee1
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/enum_is_in_range/enum_lhs.desc b/regression/cbmc/enum_is_in_range/enum_lhs.desc
new file mode 100644
index 00000000000..2860a11d4c5
--- /dev/null
+++ b/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.
+