C front-end: constant folding for floating-point

Author: Daniel Kroening

regression/cbmc/switch7/main.c

@@ -0,0 +1,23 @@
+// These need to be constant-folded at compile time
+
+#define C1 (int) ( 0. / 1. + 0.5)
+#define C2 (int) ( 1. / 1. + 0.5)
+
+int nondet_int();
+
+int main(void)
+{
+  int i=nondet_int();
+
+  switch(i)
+  {
+  case C1:
+    break;
+
+  case C2:
+    break;
+
+  default:
+    break;
+  }
+}

regression/cbmc/switch7/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -24,6 +24,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/string_constant.h>
 
+#include <goto-programs/adjust_float_expressions.h>
+
 #include "builtin_factory.h"
 #include "c_typecast.h"
 #include "c_qualifiers.h"
@@ -3372,6 +3374,13 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
 
 void c_typecheck_baset::make_constant(exprt &expr)
 {
+  // Floating-point expressions may require a rounding mode.
+  // The compile-time rounding mode may differ from the
+  // run-time rounding mode.
+  const auto rounding_mode =
+    from_integer(config.ansi_c.rounding_mode, signed_int_type());
+  adjust_float_expressions(expr, rounding_mode);
+
   simplify(expr, *this);
 
   if(!expr.is_constant() &&