From 15d430732dfec4bccb85c160e33d9625885462f5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 27 Jun 2018 14:30:20 +0000
Subject: [PATCH] Evaluate expressions that delimit GCC switch/case ranges

Type casts may reasonably occur in here (and maybe also other expressions that
evaluate to constants). The regression test addionally covers the case of enum
values being used, which works fine (even without this change).
---
 regression/cbmc/gcc_switch_case_range2/main.c | 32 +++++++++++++++++++
 .../cbmc/gcc_switch_case_range2/test.desc     |  9 ++++++
 src/ansi-c/c_typecheck_code.cpp               |  3 ++
 3 files changed, 44 insertions(+)
 create mode 100644 regression/cbmc/gcc_switch_case_range2/main.c
 create mode 100644 regression/cbmc/gcc_switch_case_range2/test.desc

diff --git a/regression/cbmc/gcc_switch_case_range2/main.c b/regression/cbmc/gcc_switch_case_range2/main.c
new file mode 100644
index 00000000000..6858a9e8c3a
--- /dev/null
+++ b/regression/cbmc/gcc_switch_case_range2/main.c
@@ -0,0 +1,32 @@
+typedef enum
+{
+  VALUE_1,
+  VALUE_2,
+  VALUE_3,
+  VALUE_4
+} values;
+
+int main()
+{
+  unsigned x;
+  switch(x)
+  {
+  case VALUE_1:
+    __CPROVER_assert(0, "0 works");
+    break;
+#ifdef __GNUC__
+  case VALUE_2 ... 3:
+#else
+  case VALUE_2:
+  case VALUE_3:
+  case VALUE_4:
+#endif
+    __CPROVER_assert(0, "... works");
+    break;
+  default:
+    __CPROVER_assert(0, "default works");
+    break;
+  }
+
+  return 0;
+}
diff --git a/regression/cbmc/gcc_switch_case_range2/test.desc b/regression/cbmc/gcc_switch_case_range2/test.desc
new file mode 100644
index 00000000000..cfa6e0b1e20
--- /dev/null
+++ b/regression/cbmc/gcc_switch_case_range2/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 3 of 3 failed
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index 31eda7a4c33..a591883ad24 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -535,6 +535,7 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)
     exprt &case_expr=code.case_op();
     typecheck_expr(case_expr);
     implicit_typecast(case_expr, switch_op_type);
+    make_constant(case_expr);
   }
 }
 
@@ -561,6 +562,8 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)
   typecheck_expr(code.op1());
   implicit_typecast(code.op0(), switch_op_type);
   implicit_typecast(code.op1(), switch_op_type);
+  make_constant(code.op0());
+  make_constant(code.op1());
 }
 
 void c_typecheck_baset::typecheck_gcc_local_label(codet &code)