From 285893a53b684b1fd99889bf75b397f3e2c09ace Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 11 Jan 2024 16:05:49 +0000
Subject: [PATCH] Conversion check: fix off-by-one error for float-to-unsigned

We use less-than in the comparison, so make the bound one larger than
the largest representable value (as we do in the other cases of
float-to-signed/unsigned conversion checks).

Fixes: #8131
---
 regression/cbmc/overflow/float_conversion.c   | 20 +++++++++++++++++++
 .../cbmc/overflow/float_conversion.desc       |  8 ++++++++
 src/ansi-c/goto_check_c.cpp                   |  2 +-
 3 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/overflow/float_conversion.c
 create mode 100644 regression/cbmc/overflow/float_conversion.desc

diff --git a/regression/cbmc/overflow/float_conversion.c b/regression/cbmc/overflow/float_conversion.c
new file mode 100644
index 00000000000..05275fd8876
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc/overflow/float_conversion.desc b/regression/cbmc/overflow/float_conversion.desc
new file mode 100644
index 00000000000..2eb6a659bef
--- /dev/null
+++ b/regression/cbmc/overflow/float_conversion.desc
@@ -0,0 +1,8 @@
+CORE
+float_conversion.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
index a05a9953b17..b21b76af1ea 100644
--- a/src/ansi-c/goto_check_c.cpp
+++ b/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());