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).

Author: tautschnig

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;
+}

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

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)