Evaluate expressions that delimit GCC switch/case ranges

tautschnig · tautschnig · commit 15d430732dfe · 2018-07-03T10:26:23.000Z
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).
diff --git a/regression/cbmc/gcc_switch_case_range2/main.c 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
@@ -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
@@ -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)

Original file line number	Diff line number	Diff line change
`@@ -535,6 +535,7 @@ void c_typecheck_baset::typecheck_switch_case(code_switch_caset &code)`
`535`	`535`	`exprt &case_expr=code.case_op();`
`536`	`536`	`typecheck_expr(case_expr);`
`537`	`537`	`implicit_typecast(case_expr, switch_op_type);`
	`538`	`+ make_constant(case_expr);`
`538`	`539`	`}`
`539`	`540`	`}`
`540`	`541`
`@@ -561,6 +562,8 @@ void c_typecheck_baset::typecheck_gcc_switch_case_range(codet &code)`
`561`	`562`	`typecheck_expr(code.op1());`
`562`	`563`	`implicit_typecast(code.op0(), switch_op_type);`
`563`	`564`	`implicit_typecast(code.op1(), switch_op_type);`
	`565`	`+ make_constant(code.op0());`
	`566`	`+ make_constant(code.op1());`
`564`	`567`	`}`
`565`	`568`
`566`	`569`	`void c_typecheck_baset::typecheck_gcc_local_label(codet &code)`