Merge pull request #8157 from tautschnig/bugfixes/8131-float-overflow…

…-off-by-one

Conversion check: fix off-by-one error for float-to-unsigned

regression/cbmc/overflow/float_conversion.c

@@ -0,0 +1,20 @@
+#include <stdint.h>
+
+int main()
+{
+  uint32_t u = 0xffffffffu;
+
+  // since the double type seems to be implemented with a IEEE 754 binary64
+  // format in CBMC, which has 53 bits of mantissa, double has enough bits to
+  // represent the exact value of u, use, e.g., http://weitz.de/ieee/ to check;
+  // therefore, C17, section 6.3.1.4, paragraph 2 says that this is
+  // defined behavior and d should store the exact value that u stores
+  double d = u;
+
+  // defined behavior behavior as well, by C17 section 6.3.1.4, paragraph 1,
+  // because the 'unsigned' type can represent the value; however,
+  // cbmc --conversion-check used to complain
+  u = (uint32_t)d;
+
+  return 0;
+}

regression/cbmc/overflow/float_conversion.desc

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

src/ansi-c/goto_check_c.cpp

@@ -796,7 +796,7 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
       {
         // Note that the fractional part is truncated!
         ieee_floatt upper(to_floatbv_type(old_type));
-        upper.from_integer(power(2, new_width) - 1);
+        upper.from_integer(power(2, new_width));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());