Merge pull request #2490 from tautschnig/switch-range

Evaluate expressions that delimit GCC switch/case ranges

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)