From b0f6a50fd37b332f467cb09e11edf09c5b4dc535 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Feb 2024 12:43:39 +0000
Subject: [PATCH 1/9] C library: implement log2{,f,l} and log10{,f,l}

Follows the same approximation approach as previously taken for log (and
logf, logl).
---
 regression/cbmc-library/log10-01/main.c     |  12 +
 regression/cbmc-library/log10-01/test.desc  |   8 +
 regression/cbmc-library/log10f-01/main.c    |  12 +
 regression/cbmc-library/log10f-01/test.desc |   8 +
 regression/cbmc-library/log10l-01/main.c    |  12 +
 regression/cbmc-library/log10l-01/test.desc |   8 +
 regression/cbmc-library/log2-01/main.c      |  12 +
 regression/cbmc-library/log2-01/test.desc   |   8 +
 regression/cbmc-library/log2f-01/main.c     |  12 +
 regression/cbmc-library/log2f-01/test.desc  |   8 +
 regression/cbmc-library/log2l-01/main.c     |  12 +
 regression/cbmc-library/log2l-01/test.desc  |   8 +
 src/ansi-c/library/math.c                   | 363 ++++++++++++++++++++
 13 files changed, 483 insertions(+)
 create mode 100644 regression/cbmc-library/log10-01/main.c
 create mode 100644 regression/cbmc-library/log10-01/test.desc
 create mode 100644 regression/cbmc-library/log10f-01/main.c
 create mode 100644 regression/cbmc-library/log10f-01/test.desc
 create mode 100644 regression/cbmc-library/log10l-01/main.c
 create mode 100644 regression/cbmc-library/log10l-01/test.desc
 create mode 100644 regression/cbmc-library/log2-01/main.c
 create mode 100644 regression/cbmc-library/log2-01/test.desc
 create mode 100644 regression/cbmc-library/log2f-01/main.c
 create mode 100644 regression/cbmc-library/log2f-01/test.desc
 create mode 100644 regression/cbmc-library/log2l-01/main.c
 create mode 100644 regression/cbmc-library/log2l-01/test.desc

diff --git a/regression/cbmc-library/log10-01/main.c b/regression/cbmc-library/log10-01/main.c
new file mode 100644
index 00000000000..c8eb0b4c676
--- /dev/null
+++ b/regression/cbmc-library/log10-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  double one = log10(10.0);
+  assert(one > 0.978 && one < 1.005);
+  return 0;
+}
diff --git a/regression/cbmc-library/log10-01/test.desc b/regression/cbmc-library/log10-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/log10-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/log10f-01/main.c b/regression/cbmc-library/log10f-01/main.c
new file mode 100644
index 00000000000..9d257a2998e
--- /dev/null
+++ b/regression/cbmc-library/log10f-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  float one = log10f(10.0f);
+  assert(one > 0.978f && one < 1.005f);
+  return 0;
+}
diff --git a/regression/cbmc-library/log10f-01/test.desc b/regression/cbmc-library/log10f-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/log10f-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/log10l-01/main.c b/regression/cbmc-library/log10l-01/main.c
new file mode 100644
index 00000000000..431b1474324
--- /dev/null
+++ b/regression/cbmc-library/log10l-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  long double one = log10l(10.0l);
+  assert(one > 0.978l && one < 1.005l);
+  return 0;
+}
diff --git a/regression/cbmc-library/log10l-01/test.desc b/regression/cbmc-library/log10l-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/log10l-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/log2-01/main.c b/regression/cbmc-library/log2-01/main.c
new file mode 100644
index 00000000000..4824405c2fb
--- /dev/null
+++ b/regression/cbmc-library/log2-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  double one = log2(2.0);
+  assert(one > 0.999 && one < 1.087);
+  return 0;
+}
diff --git a/regression/cbmc-library/log2-01/test.desc b/regression/cbmc-library/log2-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/log2-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/log2f-01/main.c b/regression/cbmc-library/log2f-01/main.c
new file mode 100644
index 00000000000..fb231eab153
--- /dev/null
+++ b/regression/cbmc-library/log2f-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  float one = log2f(2.0f);
+  assert(one > 0.999f && one < 1.087f);
+  return 0;
+}
diff --git a/regression/cbmc-library/log2f-01/test.desc b/regression/cbmc-library/log2f-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/log2f-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/log2l-01/main.c b/regression/cbmc-library/log2l-01/main.c
new file mode 100644
index 00000000000..e8666da27b8
--- /dev/null
+++ b/regression/cbmc-library/log2l-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  long double one = log2l(2.0l);
+  assert(one > 0.999l && one < 1.087l);
+  return 0;
+}
diff --git a/regression/cbmc-library/log2l-01/test.desc b/regression/cbmc-library/log2l-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/log2l-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 36826c575b4..1545cc8e214 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -2845,6 +2845,369 @@ long double logl(long double x)
 #endif
 }
 
+/* FUNCTION: log2 */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  ifdef _WIN32
+#    define _USE_MATH_DEFINES
+#  endif
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#  include <stdint.h>
+#  define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+int32_t __VERIFIER_nondet_int32_t(void);
+
+double log2(double x)
+{
+  if(__CPROVER_isnand(x) || (__CPROVER_isinfd(x) && !__CPROVER_signd(x)))
+    return x;
+  else if(x == 1.0)
+    return +0.0;
+  else if(fpclassify(x) == FP_ZERO)
+  {
+    errno = ERANGE;
+    return -HUGE_VAL;
+  }
+  else if(__CPROVER_signd(x))
+  {
+    errno = EDOM;
+    return 0.0 / 0.0;
+  }
+
+  _Static_assert(
+    sizeof(double) == 2 * sizeof(int32_t),
+    "bit width of double is 2x bit width of int32_t");
+  union
+  {
+    double d;
+    int32_t i[2];
+  } u = {x};
+  int32_t bias = (1 << 20) * ((1 << 10) - 1);
+  int32_t exp_c = __VERIFIER_nondet_int32_t();
+  __CPROVER_assume(exp_c >= -90253 && exp_c <= 1);
+#if !defined(__BYTE_ORDER__) || __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return ((double)u.i[1] - (double)(bias + exp_c)) / (double)(1 << 20);
+#else
+  return ((double)u.i[0] - (double)(bias + exp_c)) / (double)(1 << 20);
+#endif
+}
+
+/* FUNCTION: log2f */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  ifdef _WIN32
+#    define _USE_MATH_DEFINES
+#  endif
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#  include <stdint.h>
+#  define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+int32_t __VERIFIER_nondet_int32_t(void);
+
+float log2f(float x)
+{
+  if(__CPROVER_isnanf(x) || (__CPROVER_isinff(x) && !__CPROVER_signf(x)))
+    return x;
+  else if(x == 1.0f)
+    return +0.0f;
+  else if(fpclassify(x) == FP_ZERO)
+  {
+    errno = ERANGE;
+    return -HUGE_VALF;
+  }
+  else if(__CPROVER_signf(x))
+  {
+    errno = EDOM;
+    return 0.0f / 0.0f;
+  }
+
+  _Static_assert(
+    sizeof(float) == sizeof(int32_t),
+    "bit width of float and int32_t should match");
+  union
+  {
+    float f;
+    int32_t i;
+  } u = {x};
+  int32_t bias = (1 << 23) * ((1 << 7) - 1);
+  int32_t exp_c = __VERIFIER_nondet_int32_t();
+  __CPROVER_assume(exp_c >= -722019 && exp_c <= 1);
+  return ((float)u.i - (float)(bias + exp_c)) / (float)(1 << 23);
+}
+
+/* FUNCTION: log2l */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  ifdef _WIN32
+#    define _USE_MATH_DEFINES
+#  endif
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#  include <stdint.h>
+#  define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FLOAT_H_INCLUDED
+#  include <float.h>
+#  define __CPROVER_FLOAT_H_INCLUDED
+#endif
+
+int32_t __VERIFIER_nondet_int32_t(void);
+
+long double log2l(long double x)
+{
+  if(__CPROVER_isnanld(x) || (__CPROVER_isinfld(x) && !__CPROVER_signld(x)))
+    return x;
+  else if(x == 1.0l)
+    return +0.0l;
+  else if(fpclassify(x) == FP_ZERO)
+  {
+    errno = ERANGE;
+    return -HUGE_VALL;
+  }
+  else if(__CPROVER_signld(x))
+  {
+    errno = EDOM;
+    return 0.0l / 0.0l;
+  }
+
+#if LDBL_MAX_EXP == DBL_MAX_EXP
+  return log2(x);
+#else
+  _Static_assert(
+    sizeof(long double) % sizeof(int32_t) == 0,
+    "bit width of long double is a multiple of bit width of int32_t");
+  union
+  {
+    long double l;
+    int32_t i[sizeof(long double) / sizeof(int32_t)];
+  } u = {x};
+  int32_t bias = (1 << 16) * ((1 << 14) - 1);
+  int32_t exp_c = __VERIFIER_nondet_int32_t();
+  __CPROVER_assume(exp_c >= -5641 && exp_c <= 1);
+#  if !defined(__BYTE_ORDER__) || __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return ((long double)u.i[sizeof(long double) / sizeof(int32_t) - 1] -
+          (long double)(bias + exp_c)) /
+         (long double)(1 << 16);
+#  else
+  return ((long double)u.i[0] - (long double)(bias + exp_c)) /
+         (long double)(1 << 16);
+#  endif
+#endif
+}
+
+/* FUNCTION: log10 */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  ifdef _WIN32
+#    define _USE_MATH_DEFINES
+#  endif
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#  include <stdint.h>
+#  define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+int32_t __VERIFIER_nondet_int32_t(void);
+
+double log10(double x)
+{
+  if(__CPROVER_isnand(x) || (__CPROVER_isinfd(x) && !__CPROVER_signd(x)))
+    return x;
+  else if(x == 1.0)
+    return +0.0;
+  else if(fpclassify(x) == FP_ZERO)
+  {
+    errno = ERANGE;
+    return -HUGE_VAL;
+  }
+  else if(__CPROVER_signd(x))
+  {
+    errno = EDOM;
+    return 0.0 / 0.0;
+  }
+
+  _Static_assert(
+    sizeof(double) == 2 * sizeof(int32_t),
+    "bit width of double is 2x bit width of int32_t");
+  // https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/
+  union
+  {
+    double d;
+    int32_t i[2];
+  } u = {x};
+  int32_t bias = (1 << 20) * ((1 << 10) - 1);
+  int32_t exp_c = __VERIFIER_nondet_int32_t();
+  __CPROVER_assume(exp_c >= -90253 && exp_c <= 1);
+#if !defined(__BYTE_ORDER__) || __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return ((double)u.i[1] - (double)(bias + exp_c)) * (M_LN2 / M_LN10) /
+         (double)(1 << 20);
+#else
+  return ((double)u.i[0] - (double)(bias + exp_c)) * (M_LN2 / M_LN10) /
+         (double)(1 << 20);
+#endif
+}
+
+/* FUNCTION: log10f */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  ifdef _WIN32
+#    define _USE_MATH_DEFINES
+#  endif
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#  include <stdint.h>
+#  define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+int32_t __VERIFIER_nondet_int32_t(void);
+
+float log10f(float x)
+{
+  if(__CPROVER_isnanf(x) || (__CPROVER_isinff(x) && !__CPROVER_signf(x)))
+    return x;
+  else if(x == 1.0f)
+    return +0.0f;
+  else if(fpclassify(x) == FP_ZERO)
+  {
+    errno = ERANGE;
+    return -HUGE_VALF;
+  }
+  else if(__CPROVER_signf(x))
+  {
+    errno = EDOM;
+    return 0.0f / 0.0f;
+  }
+
+  _Static_assert(
+    sizeof(float) == sizeof(int32_t),
+    "bit width of float and int32_t should match");
+  // https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/
+  union
+  {
+    float f;
+    int32_t i;
+  } u = {x};
+  int32_t bias = (1 << 23) * ((1 << 7) - 1);
+  int32_t exp_c = __VERIFIER_nondet_int32_t();
+  __CPROVER_assume(exp_c >= -722019 && exp_c <= 1);
+  return ((float)u.i - (float)(bias + exp_c)) * (float)(M_LN2 / M_LN10) /
+         (float)(1 << 23);
+}
+
+/* FUNCTION: log10l */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  ifdef _WIN32
+#    define _USE_MATH_DEFINES
+#  endif
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_STDINT_H_INCLUDED
+#  include <stdint.h>
+#  define __CPROVER_STDINT_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FLOAT_H_INCLUDED
+#  include <float.h>
+#  define __CPROVER_FLOAT_H_INCLUDED
+#endif
+
+int32_t __VERIFIER_nondet_int32_t(void);
+
+long double log10l(long double x)
+{
+  if(__CPROVER_isnanld(x) || (__CPROVER_isinfld(x) && !__CPROVER_signld(x)))
+    return x;
+  else if(x == 1.0l)
+    return +0.0l;
+  else if(fpclassify(x) == FP_ZERO)
+  {
+    errno = ERANGE;
+    return -HUGE_VALL;
+  }
+  else if(__CPROVER_signld(x))
+  {
+    errno = EDOM;
+    return 0.0l / 0.0l;
+  }
+
+#if LDBL_MAX_EXP == DBL_MAX_EXP
+  return log10(x);
+#else
+  _Static_assert(
+    sizeof(long double) % sizeof(int32_t) == 0,
+    "bit width of long double is a multiple of bit width of int32_t");
+  union
+  {
+    long double l;
+    int32_t i[sizeof(long double) / sizeof(int32_t)];
+  } u = {x};
+  int32_t bias = (1 << 16) * ((1 << 14) - 1);
+  int32_t exp_c = __VERIFIER_nondet_int32_t();
+  __CPROVER_assume(exp_c >= -5641 && exp_c <= 1);
+#  if !defined(__BYTE_ORDER__) || __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
+  return ((long double)u.i[sizeof(long double) / sizeof(int32_t) - 1] -
+          (long double)(bias + exp_c)) *
+         (M_LN2 / M_LN10) / (long double)(1 << 16);
+#  else
+  return ((long double)u.i[0] - (long double)(bias + exp_c)) *
+         (M_LN2 / M_LN10) / (long double)(1 << 16);
+#  endif
+#endif
+}
+
 /* FUNCTION: pow */
 
 #ifndef __CPROVER_MATH_H_INCLUDED

From 9d6c3a5fbd49947d369b638ef952fdb0fbc698e4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Feb 2024 13:24:25 +0000
Subject: [PATCH 2/9] C library: fix logl in case long double == double

We previously ended up with recursion.
---
 src/ansi-c/library/math.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 1545cc8e214..71450f526ab 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -2821,7 +2821,7 @@ long double logl(long double x)
   }
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
-  return logl(x);
+  return log(x);
 #else
   _Static_assert(
     sizeof(long double) % sizeof(int32_t) == 0,

From 2a12580ed8b836ffb12f6a4d25f58175f517a2be Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Feb 2024 14:29:14 +0000
Subject: [PATCH 3/9] C library: implement feraiseexcept

Model floating-point exceptions as failing assertions.
---
 regression/cbmc-library/feraiseexcept-01/main.c    | 9 +++++++++
 regression/cbmc-library/feraiseexcept-01/test.desc | 8 ++++++++
 src/ansi-c/library/fenv.c                          | 9 +++++++++
 3 files changed, 26 insertions(+)
 create mode 100644 regression/cbmc-library/feraiseexcept-01/main.c
 create mode 100644 regression/cbmc-library/feraiseexcept-01/test.desc

diff --git a/regression/cbmc-library/feraiseexcept-01/main.c b/regression/cbmc-library/feraiseexcept-01/main.c
new file mode 100644
index 00000000000..e4d6dd90771
--- /dev/null
+++ b/regression/cbmc-library/feraiseexcept-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <fenv.h>
+
+int main()
+{
+  int exceptions;
+  feraiseexcept(exceptions);
+  return 0;
+}
diff --git a/regression/cbmc-library/feraiseexcept-01/test.desc b/regression/cbmc-library/feraiseexcept-01/test.desc
new file mode 100644
index 00000000000..e2d2d714649
--- /dev/null
+++ b/regression/cbmc-library/feraiseexcept-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/library/fenv.c b/src/ansi-c/library/fenv.c
index 31e17d615d2..0c3ba94f45b 100644
--- a/src/ansi-c/library/fenv.c
+++ b/src/ansi-c/library/fenv.c
@@ -40,3 +40,12 @@ __CPROVER_HIDE:;
     0;
   return 0; // we never fail
 }
+
+/* FUNCTION: feraiseexcept */
+
+int feraiseexcept(int excepts)
+{
+__CPROVER_HIDE:;
+  __CPROVER_assert(excepts == 0, "floating-point exception");
+  return 0; // we never fail
+}

From 7329adab5767fec36e3385ca08285656cd16708a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Feb 2024 14:02:28 +0000
Subject: [PATCH 4/9] C library: implement fma{,f,l}

Model fused multiply-add as documented in its man page.
---
 regression/cbmc-library/fma-01/main.c     |   9 ++
 regression/cbmc-library/fma-01/test.desc  |   8 ++
 regression/cbmc-library/fmaf-01/main.c    |   9 ++
 regression/cbmc-library/fmaf-01/test.desc |   8 ++
 regression/cbmc-library/fmal-01/main.c    |   9 ++
 regression/cbmc-library/fmal-01/test.desc |   8 ++
 src/ansi-c/library/math.c                 | 138 ++++++++++++++++++++++
 7 files changed, 189 insertions(+)
 create mode 100644 regression/cbmc-library/fma-01/main.c
 create mode 100644 regression/cbmc-library/fma-01/test.desc
 create mode 100644 regression/cbmc-library/fmaf-01/main.c
 create mode 100644 regression/cbmc-library/fmaf-01/test.desc
 create mode 100644 regression/cbmc-library/fmal-01/main.c
 create mode 100644 regression/cbmc-library/fmal-01/test.desc

diff --git a/regression/cbmc-library/fma-01/main.c b/regression/cbmc-library/fma-01/main.c
new file mode 100644
index 00000000000..0aff50077cb
--- /dev/null
+++ b/regression/cbmc-library/fma-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  double five = fma(1.0, 2.0, 3.0);
+  assert(five > 4.99 && five < 5.01);
+  return 0;
+}
diff --git a/regression/cbmc-library/fma-01/test.desc b/regression/cbmc-library/fma-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/fma-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/fmaf-01/main.c b/regression/cbmc-library/fmaf-01/main.c
new file mode 100644
index 00000000000..14ebfe45e89
--- /dev/null
+++ b/regression/cbmc-library/fmaf-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float five = fmaf(1.0f, 2.0f, 3.0f);
+  assert(five > 4.99f && five < 5.01f);
+  return 0;
+}
diff --git a/regression/cbmc-library/fmaf-01/test.desc b/regression/cbmc-library/fmaf-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/fmaf-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/fmal-01/main.c b/regression/cbmc-library/fmal-01/main.c
new file mode 100644
index 00000000000..76ea17f10d3
--- /dev/null
+++ b/regression/cbmc-library/fmal-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  long double five = fmal(1.0l, 2.0l, 3.0l);
+  assert(five > 4.99l && five < 5.01l);
+  return 0;
+}
diff --git a/regression/cbmc-library/fmal-01/test.desc b/regression/cbmc-library/fmal-01/test.desc
new file mode 100644
index 00000000000..3510d48c5c6
--- /dev/null
+++ b/regression/cbmc-library/fmal-01/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 71450f526ab..2e072dd506d 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -3599,3 +3599,141 @@ long double powl(long double x, long double y)
   return result_u.l;
 #endif
 }
+
+/* FUNCTION: fma */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#  include <fenv.h>
+#  define __CPROVER_FENV_H_INCLUDED
+#endif
+
+double __builtin_inf(void);
+
+double fma(double x, double y, double z)
+{
+  // see man fma (https://linux.die.net/man/3/fma)
+  if(isnan(x) || isnan(y))
+    return 0.0 / 0.0;
+  else if(
+    (isinf(x) || isinf(y)) &&
+    (fpclassify(x) == FP_ZERO || fpclassify(y) == FP_ZERO))
+  {
+    feraiseexcept(FE_INVALID);
+    return 0.0 / 0.0;
+  }
+  else if(isnan(z))
+    return 0.0 / 0.0;
+
+  double x_times_y = x * y;
+  if(
+    isinf(x_times_y) && isinf(z) &&
+    __CPROVER_signd(x_times_y) != __CPROVER_signd(z))
+  {
+    feraiseexcept(FE_INVALID);
+    return 0.0 / 0.0;
+  }
+
+  // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inf()
+  // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
+  return x_times_y + z;
+}
+
+/* FUNCTION: fmaf */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#  include <fenv.h>
+#  define __CPROVER_FENV_H_INCLUDED
+#endif
+
+float __builtin_inff(void);
+
+float fmaf(float x, float y, float z)
+{
+  // see man fma (https://linux.die.net/man/3/fma)
+  if(isnanf(x) || isnanf(y))
+    return 0.0f / 0.0f;
+  else if(
+    (isinff(x) || isinff(y)) &&
+    (fpclassify(x) == FP_ZERO || fpclassify(y) == FP_ZERO))
+  {
+    feraiseexcept(FE_INVALID);
+    return 0.0f / 0.0f;
+  }
+  else if(isnanf(z))
+    return 0.0f / 0.0f;
+
+  float x_times_y = x * y;
+  if(
+    isinff(x_times_y) && isinff(z) &&
+    __CPROVER_signf(x_times_y) != __CPROVER_signf(z))
+  {
+    feraiseexcept(FE_INVALID);
+    return 0.0f / 0.0f;
+  }
+
+  // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inff()
+  // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
+  return x_times_y + z;
+}
+
+/* FUNCTION: fmal */
+
+#ifndef __CPROVER_MATH_H_INCLUDED
+#  include <math.h>
+#  define __CPROVER_MATH_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FENV_H_INCLUDED
+#  include <fenv.h>
+#  define __CPROVER_FENV_H_INCLUDED
+#endif
+
+#ifndef __CPROVER_FLOAT_H_INCLUDED
+#  include <float.h>
+#  define __CPROVER_FLOAT_H_INCLUDED
+#endif
+
+long double __builtin_infl(void);
+
+long double fmal(long double x, long double y, long double z)
+{
+  // see man fma (https://linux.die.net/man/3/fma)
+  if(isnanl(x) || isnanl(y))
+    return 0.0l / 0.0l;
+  else if(
+    (isinfl(x) || isinfl(y)) &&
+    (fpclassify(x) == FP_ZERO || fpclassify(y) == FP_ZERO))
+  {
+    feraiseexcept(FE_INVALID);
+    return 0.0l / 0.0l;
+  }
+  else if(isnanl(z))
+    return 0.0l / 0.0l;
+
+  long double x_times_y = x * y;
+  if(
+    isinfl(x_times_y) && isinfl(z) &&
+    __CPROVER_signld(x_times_y) != __CPROVER_signld(z))
+  {
+    feraiseexcept(FE_INVALID);
+    return 0.0l / 0.0l;
+  }
+
+#if LDBL_MAX_EXP == DBL_MAX_EXP
+  return fma(x, y, z);
+#else
+  // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_infl()
+  // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
+  return x_times_y + z;
+#endif
+}

From 1bc9833caedbbf302ba0f571f99c2ea7e6abbffc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Feb 2024 14:41:28 +0000
Subject: [PATCH 5/9] C library: do not flag division-by-zero when building NaN

We construct NaN (and Inf) by dividing by zero, which is a
standards-compliant way in that Nan (Inf) is the correct result for
these cases. Do not flag these operations as division-by-zero, which the
user would not expect.
---
 regression/cbmc-library/pow-01/main.c |  10 +++
 src/ansi-c/library/math.c             | 120 ++++++++++++++++++++++++++
 2 files changed, 130 insertions(+)

diff --git a/regression/cbmc-library/pow-01/main.c b/regression/cbmc-library/pow-01/main.c
index eb38fb397dc..c2c37423083 100644
--- a/regression/cbmc-library/pow-01/main.c
+++ b/regression/cbmc-library/pow-01/main.c
@@ -1,9 +1,19 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 int main()
 {
   double four = pow(2.0, 2.0);
   assert(four > 3.999 && four < 4.345);
+
+  double x;
+  __CPROVER_assume(isnormal(x));
+  double limit = 1 << 15;
+  __CPROVER_assume(x > -limit && x < limit);
+  __CPROVER_assume(x > FLT_MIN || x < -FLT_MIN);
+  double sq = pow(x, 2.0);
+  assert(sq >= 0.0);
+
   return 0;
 }
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index 2e072dd506d..f506799e8e2 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -220,21 +220,33 @@ int __isnormalf(float f)
 
 float __builtin_inff(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-overflow"
   return 1.0f / 0.0f;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_inf */
 
 double __builtin_inf(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-overflow"
   return 1.0 / 0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_infl */
 
 long double __builtin_infl(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-overflow"
   return 1.0l / 0.0l;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_isinf */
@@ -276,21 +288,33 @@ int __builtin_isnanf(float f)
 
 float __builtin_huge_valf(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-overflow"
   return 1.0f / 0.0f;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_huge_val */
 
 double __builtin_huge_val(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-overflow"
   return 1.0 / 0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_huge_vall */
 
 long double __builtin_huge_vall(void)
 {
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
+#pragma CPROVER check disable "float-overflow"
   return 1.0l / 0.0l;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: _dsign */
@@ -597,7 +621,10 @@ double __builtin_nan(const char *str)
   // the 'str' argument is not yet used
 __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0/0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: __builtin_nanf */
@@ -607,7 +634,10 @@ float __builtin_nanf(const char *str)
   // the 'str' argument is not yet used
 __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0f/0.0f;
+#pragma CPROVER check pop
 }
 
 
@@ -630,7 +660,10 @@ double nan(const char *str) {
   // the 'str' argument is not yet used
  __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0/0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: nanf */
@@ -639,7 +672,10 @@ float nanf(const char *str) {
   // the 'str' argument is not yet used
  __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0f/0.0f;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: nanl */
@@ -648,7 +684,10 @@ long double nanl(const char *str) {
   // the 'str' argument is not yet used
  __CPROVER_hide:;
   (void)*str;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   return 0.0/0.0;
+#pragma CPROVER check pop
 }
 
 /* FUNCTION: nextUpf */
@@ -676,7 +715,10 @@ float nextUpf(float f)
 {
 __CPROVER_hide:;
   if (__CPROVER_isnanf(f))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f/0.0f;  // NaN
+#pragma CPROVER check pop
   else if (f == 0.0f)
     return 0x1p-149f;
   else if (f > 0.0f)
@@ -725,7 +767,10 @@ double nextUp(double d)
 {
 __CPROVER_hide:;
   if (__CPROVER_isnand(d))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0/0.0;  // NaN
+#pragma CPROVER check pop
   else if (d == 0.0)
     return 0x1.0p-1074;
   else if (d > 0.0)
@@ -773,7 +818,10 @@ long double nextUpl(long double d)
 {
 __CPROVER_hide:;
   if(__CPROVER_isnanld(d))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0/0.0;  // NaN
+#pragma CPROVER check pop
   else if (d == 0.0)
   {
     union mixl m;
@@ -840,7 +888,10 @@ float sqrtf(float f)
  __CPROVER_hide:;
 
   if ( f < 0.0f )
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f/0.0f; // NaN
+#pragma CPROVER check pop
   else if (__CPROVER_isinff(f) ||   // +Inf only
            f == 0.0f          ||   // Includes -0
            __CPROVER_isnanf(f))
@@ -927,7 +978,10 @@ double sqrt(double d)
  __CPROVER_hide:;
 
   if ( d < 0.0 )
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0/0.0; // NaN
+#pragma CPROVER check pop
   else if (__CPROVER_isinfd(d) ||   // +Inf only
            d == 0.0            ||   // Includes -0
            __CPROVER_isnand(d))
@@ -998,7 +1052,10 @@ long double sqrtl(long double d)
  __CPROVER_hide:;
 
   if(d < 0.0l)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l/0.0l; // NaN
+#pragma CPROVER check pop
   else if (__CPROVER_isinfld(d) ||   // +Inf only
            d == 0.0l            ||   // Includes -0
            __CPROVER_isnanld(d))
@@ -2700,7 +2757,10 @@ double log(double x)
   else if(__CPROVER_signd(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2758,7 +2818,10 @@ float logf(float x)
   else if(__CPROVER_signf(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2817,7 +2880,10 @@ long double logl(long double x)
   else if(__CPROVER_signld(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -2881,7 +2947,10 @@ double log2(double x)
   else if(__CPROVER_signd(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2938,7 +3007,10 @@ float log2f(float x)
   else if(__CPROVER_signf(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -2996,7 +3068,10 @@ long double log2l(long double x)
   else if(__CPROVER_signld(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -3060,7 +3135,10 @@ double log10(double x)
   else if(__CPROVER_signd(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -3120,7 +3198,10 @@ float log10f(float x)
   else if(__CPROVER_signf(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
 
   _Static_assert(
@@ -3180,7 +3261,10 @@ long double log10l(long double x)
   else if(__CPROVER_signld(x))
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
@@ -3237,7 +3321,10 @@ double pow(double x, double y)
     nearbyint(y) != y)
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
   }
   else if(x == 1.0)
     return 1.0;
@@ -3303,7 +3390,10 @@ double pow(double x, double y)
       return HUGE_VAL;
   }
   else if(isnan(x) || isnan(y))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0 / 0.0;
+#pragma CPROVER check pop
 
   _Static_assert(
     sizeof(double) == 2 * sizeof(int32_t),
@@ -3317,11 +3407,14 @@ double pow(double x, double y)
   int32_t bias = (1 << 20) * ((1 << 10) - 1);
   int32_t exp_c = __VERIFIER_nondet_int32_t();
   __CPROVER_assume(exp_c >= -90253 && exp_c <= 1);
+#pragma CPROVER check push
+#pragma CPROVER check disable "signed-overflow"
 #if !defined(__BYTE_ORDER__) || __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
   double mult_result = y * (double)(u.i[1] - (bias + exp_c));
 #else
   double mult_result = y * (double)(u.i[0] - (bias + exp_c));
 #endif
+#pragma CPROVER check pop
   if(fabs(mult_result) > (double)(1 << 30))
   {
     errno = ERANGE;
@@ -3366,7 +3459,10 @@ float powf(float x, float y)
     nearbyintf(y) != y)
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
   }
   else if(x == 1.0f)
     return 1.0f;
@@ -3435,7 +3531,10 @@ float powf(float x, float y)
       return HUGE_VALF;
   }
   else if(isnanf(x) || isnanf(y))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0f / 0.0f;
+#pragma CPROVER check pop
 
   _Static_assert(
     sizeof(float) == sizeof(int32_t),
@@ -3448,7 +3547,10 @@ float powf(float x, float y)
   int32_t bias = (1 << 23) * ((1 << 7) - 1);
   int32_t exp_c = __VERIFIER_nondet_int32_t();
   __CPROVER_assume(exp_c >= -722019 && exp_c <= 1);
+#pragma CPROVER check push
+#pragma CPROVER check disable "signed-overflow"
   float mult_result = y * (float)(u.i - (bias + exp_c));
+#pragma CPROVER check pop
   if(fabsf(mult_result) > (float)(1 << 30))
   {
     errno = ERANGE;
@@ -3492,7 +3594,10 @@ long double powl(long double x, long double y)
     nearbyintl(y) != y)
   {
     errno = EDOM;
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
   }
   else if(x == 1.0l)
     return 1.0l;
@@ -3562,7 +3667,10 @@ long double powl(long double x, long double y)
       return HUGE_VALL;
   }
   else if(isnanl(x) || isnanl(y))
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
     return 0.0l / 0.0l;
+#pragma CPROVER check pop
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return pow(x, y);
@@ -3583,7 +3691,10 @@ long double powl(long double x, long double y)
   int32_t bias = (1 << 16) * ((1 << 14) - 1);
   int32_t exp_c = __VERIFIER_nondet_int32_t();
   __CPROVER_assume(exp_c >= -5641 && exp_c <= 1);
+#  pragma CPROVER check push
+#  pragma CPROVER check disable "signed-overflow"
   long double mult_result = y * (long double)(exponent - (bias + exp_c));
+#  pragma CPROVER check pop
   if(fabsl(mult_result) > (long double)(1 << 30))
   {
     errno = ERANGE;
@@ -3617,6 +3728,8 @@ double __builtin_inf(void);
 double fma(double x, double y, double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   if(isnan(x) || isnan(y))
     return 0.0 / 0.0;
   else if(
@@ -3637,6 +3750,7 @@ double fma(double x, double y, double z)
     feraiseexcept(FE_INVALID);
     return 0.0 / 0.0;
   }
+#pragma CPROVER check pop
 
   // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inf()
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
@@ -3660,6 +3774,8 @@ float __builtin_inff(void);
 float fmaf(float x, float y, float z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   if(isnanf(x) || isnanf(y))
     return 0.0f / 0.0f;
   else if(
@@ -3680,6 +3796,7 @@ float fmaf(float x, float y, float z)
     feraiseexcept(FE_INVALID);
     return 0.0f / 0.0f;
   }
+#pragma CPROVER check pop
 
   // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inff()
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
@@ -3708,6 +3825,8 @@ long double __builtin_infl(void);
 long double fmal(long double x, long double y, long double z)
 {
   // see man fma (https://linux.die.net/man/3/fma)
+#pragma CPROVER check push
+#pragma CPROVER check disable "div-by-zero"
   if(isnanl(x) || isnanl(y))
     return 0.0l / 0.0l;
   else if(
@@ -3728,6 +3847,7 @@ long double fmal(long double x, long double y, long double z)
     feraiseexcept(FE_INVALID);
     return 0.0l / 0.0l;
   }
+#pragma CPROVER check pop
 
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return fma(x, y, z);

From 10009e7bd250f713dbe047d28df562f3bab9aee5 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Feb 2024 16:26:33 +0000
Subject: [PATCH 6/9] C library/fma: detect overflow

Fail as documented rather than via built-in assertions when overflowing.
---
 src/ansi-c/library/math.c | 24 +++++++++++++++++++++---
 1 file changed, 21 insertions(+), 3 deletions(-)

diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index f506799e8e2..c7dfc65bcf9 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -3742,6 +3742,7 @@ double fma(double x, double y, double z)
   else if(isnan(z))
     return 0.0 / 0.0;
 
+#pragma CPROVER check disable "float-overflow"
   double x_times_y = x * y;
   if(
     isinf(x_times_y) && isinf(z) &&
@@ -3752,8 +3753,13 @@ double fma(double x, double y, double z)
   }
 #pragma CPROVER check pop
 
-  // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inf()
+  if(isinf(x_times_y))
+  {
+    feraiseexcept(FE_OVERFLOW);
+    return __CPROVER_signd(x_times_y) ? -__builtin_inf() : __builtin_inf();
+  }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
+
   return x_times_y + z;
 }
 
@@ -3788,6 +3794,7 @@ float fmaf(float x, float y, float z)
   else if(isnanf(z))
     return 0.0f / 0.0f;
 
+#pragma CPROVER check disable "float-overflow"
   float x_times_y = x * y;
   if(
     isinff(x_times_y) && isinff(z) &&
@@ -3798,8 +3805,13 @@ float fmaf(float x, float y, float z)
   }
 #pragma CPROVER check pop
 
-  // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_inff()
+  if(isinff(x_times_y))
+  {
+    feraiseexcept(FE_OVERFLOW);
+    return __CPROVER_signf(x_times_y) ? -__builtin_inff() : __builtin_inff();
+  }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
+
   return x_times_y + z;
 }
 
@@ -3839,6 +3851,7 @@ long double fmal(long double x, long double y, long double z)
   else if(isnanl(z))
     return 0.0l / 0.0l;
 
+#pragma CPROVER check disable "float-overflow"
   long double x_times_y = x * y;
   if(
     isinfl(x_times_y) && isinfl(z) &&
@@ -3852,8 +3865,13 @@ long double fmal(long double x, long double y, long double z)
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return fma(x, y, z);
 #else
-  // TODO: detect overflow (FE_OVERFLOW), return +/- __builtin_infl()
+  if(isinfl(x_times_y))
+  {
+    feraiseexcept(FE_OVERFLOW);
+    return __CPROVER_signld(x_times_y) ? -__builtin_infl() : __builtin_infl();
+  }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
+
   return x_times_y + z;
 #endif
 }

From 085068c02b84a5052a2988095e400445cb369a11 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 7 Feb 2024 17:16:11 +0000
Subject: [PATCH 7/9] C library: do not report overflow in sqrt

We guess upper and lower bounds and check them for infinity afterwards.
Those multiplications should not be flagged by auto-generated
assertions.
---
 src/ansi-c/library/math.c | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index c7dfc65bcf9..dede7c22624 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -905,11 +905,14 @@ float sqrtf(float f)
     // number of exponent and significand bits.  Thus they are
     // given implicitly...
 
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     float lowerSquare = lower * lower;
     __CPROVER_assume(__CPROVER_isnormalf(lowerSquare));
 
     float upper = nextUpf(lower);
     float upperSquare = upper * upper;  // Might be +Inf
+#pragma CPROVER check pop
 
     // Restrict these to bound f and thus compute the possible
     // values for the square root.  Note that the lower bound
@@ -992,11 +995,14 @@ double sqrt(double d)
     __CPROVER_assume(lower > 0.0);
     __CPROVER_assume(__CPROVER_isnormald(lower));
 
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     double lowerSquare = lower * lower;
     __CPROVER_assume(__CPROVER_isnormald(lowerSquare));
 
     double upper = nextUp(lower);
     double upperSquare = upper * upper;  // Might be +Inf
+#pragma CPROVER check pop
 
     __CPROVER_assume(lowerSquare <= d);
     __CPROVER_assume(d < upperSquare);
@@ -1066,11 +1072,14 @@ long double sqrtl(long double d)
     __CPROVER_assume(lower > 0.0l);
     __CPROVER_assume(__CPROVER_isnormalld(lower));
 
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     long double lowerSquare = lower * lower;
     __CPROVER_assume(__CPROVER_isnormalld(lowerSquare));
 
     long double upper = nextUpl(lower);
     long double upperSquare = upper * upper;  // Might be +Inf
+#pragma CPROVER check pop
 
     __CPROVER_assume(lowerSquare <= d);
     __CPROVER_assume(d < upperSquare);

From 56d7fe73c41ab8d3770ea18d012db05df7b51bf2 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 8 Feb 2024 14:49:58 +0000
Subject: [PATCH 8/9] C library: fix _Static_assert for MSVC

Visual Studio knows static_assert, but not the standardised
_Static_assert.
---
 src/ansi-c/library/math.c | 150 ++++++++++++++++++++++++++------------
 1 file changed, 105 insertions(+), 45 deletions(-)

diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index dede7c22624..e10aabdc9b4 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -2575,9 +2575,13 @@ double exp(double x)
   __CPROVER_assume(result >= lower);
   __CPROVER_assume(result <= upper);
 
-  _Static_assert(
-    sizeof(double) == 2 * sizeof(int32_t),
-    "bit width of double is 2x bit width of int32_t");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(double) == 2 * sizeof(int32_t),
+     "bit width of double is 2x bit width of int32_t");
   union U
   {
     double d;
@@ -2642,9 +2646,13 @@ float expf(float x)
   __CPROVER_assume(result >= lower);
   __CPROVER_assume(result <= upper);
 
-  _Static_assert(
-    sizeof(float) == sizeof(int32_t),
-    "bit width of float and int32_t should match");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(float) == sizeof(int32_t),
+     "bit width of float and int32_t should match");
   union U
   {
     float f;
@@ -2713,9 +2721,13 @@ long double expl(long double x)
   __CPROVER_assume(result >= lower);
   __CPROVER_assume(result <= upper);
 
-  _Static_assert(
-    sizeof(long double) % sizeof(int32_t) == 0,
-    "bit width of long double is a multiple of bit width of int32_t");
+#  ifndef _MSC_VER
+  _Static_assert
+#  else
+  static_assert
+#  endif
+    (sizeof(long double) % sizeof(int32_t) == 0,
+     "bit width of long double is a multiple of bit width of int32_t");
   union
   {
     long double l;
@@ -2772,9 +2784,13 @@ double log(double x)
 #pragma CPROVER check pop
   }
 
-  _Static_assert(
-    sizeof(double) == 2 * sizeof(int32_t),
-    "bit width of double is 2x bit width of int32_t");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(double) == 2 * sizeof(int32_t),
+     "bit width of double is 2x bit width of int32_t");
   // https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/
   union
   {
@@ -2833,9 +2849,13 @@ float logf(float x)
 #pragma CPROVER check pop
   }
 
-  _Static_assert(
-    sizeof(float) == sizeof(int32_t),
-    "bit width of float and int32_t should match");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(float) == sizeof(int32_t),
+     "bit width of float and int32_t should match");
   // https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/
   union
   {
@@ -2898,9 +2918,13 @@ long double logl(long double x)
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return log(x);
 #else
-  _Static_assert(
-    sizeof(long double) % sizeof(int32_t) == 0,
-    "bit width of long double is a multiple of bit width of int32_t");
+#  ifndef _MSC_VER
+  _Static_assert
+#  else
+  static_assert
+#  endif
+    (sizeof(long double) % sizeof(int32_t) == 0,
+     "bit width of long double is a multiple of bit width of int32_t");
   union
   {
     long double l;
@@ -2962,9 +2986,13 @@ double log2(double x)
 #pragma CPROVER check pop
   }
 
-  _Static_assert(
-    sizeof(double) == 2 * sizeof(int32_t),
-    "bit width of double is 2x bit width of int32_t");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(double) == 2 * sizeof(int32_t),
+     "bit width of double is 2x bit width of int32_t");
   union
   {
     double d;
@@ -3022,9 +3050,13 @@ float log2f(float x)
 #pragma CPROVER check pop
   }
 
-  _Static_assert(
-    sizeof(float) == sizeof(int32_t),
-    "bit width of float and int32_t should match");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(float) == sizeof(int32_t),
+     "bit width of float and int32_t should match");
   union
   {
     float f;
@@ -3086,9 +3118,13 @@ long double log2l(long double x)
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return log2(x);
 #else
-  _Static_assert(
-    sizeof(long double) % sizeof(int32_t) == 0,
-    "bit width of long double is a multiple of bit width of int32_t");
+#  ifndef _MSC_VER
+  _Static_assert
+#  else
+  static_assert
+#  endif
+    (sizeof(long double) % sizeof(int32_t) == 0,
+     "bit width of long double is a multiple of bit width of int32_t");
   union
   {
     long double l;
@@ -3150,9 +3186,13 @@ double log10(double x)
 #pragma CPROVER check pop
   }
 
-  _Static_assert(
-    sizeof(double) == 2 * sizeof(int32_t),
-    "bit width of double is 2x bit width of int32_t");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(double) == 2 * sizeof(int32_t),
+     "bit width of double is 2x bit width of int32_t");
   // https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/
   union
   {
@@ -3213,9 +3253,13 @@ float log10f(float x)
 #pragma CPROVER check pop
   }
 
-  _Static_assert(
-    sizeof(float) == sizeof(int32_t),
-    "bit width of float and int32_t should match");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(float) == sizeof(int32_t),
+     "bit width of float and int32_t should match");
   // https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/
   union
   {
@@ -3279,9 +3323,13 @@ long double log10l(long double x)
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return log10(x);
 #else
-  _Static_assert(
-    sizeof(long double) % sizeof(int32_t) == 0,
-    "bit width of long double is a multiple of bit width of int32_t");
+#  ifndef _MSC_VER
+  _Static_assert
+#  else
+  static_assert
+#  endif
+    (sizeof(long double) % sizeof(int32_t) == 0,
+     "bit width of long double is a multiple of bit width of int32_t");
   union
   {
     long double l;
@@ -3404,9 +3452,13 @@ double pow(double x, double y)
     return 0.0 / 0.0;
 #pragma CPROVER check pop
 
-  _Static_assert(
-    sizeof(double) == 2 * sizeof(int32_t),
-    "bit width of double is 2x bit width of int32_t");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(double) == 2 * sizeof(int32_t),
+     "bit width of double is 2x bit width of int32_t");
   // https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/
   union
   {
@@ -3545,9 +3597,13 @@ float powf(float x, float y)
     return 0.0f / 0.0f;
 #pragma CPROVER check pop
 
-  _Static_assert(
-    sizeof(float) == sizeof(int32_t),
-    "bit width of float and int32_t should match");
+#ifndef _MSC_VER
+  _Static_assert
+#else
+  static_assert
+#endif
+    (sizeof(float) == sizeof(int32_t),
+     "bit width of float and int32_t should match");
   union
   {
     float f;
@@ -3684,9 +3740,13 @@ long double powl(long double x, long double y)
 #if LDBL_MAX_EXP == DBL_MAX_EXP
   return pow(x, y);
 #else
-  _Static_assert(
-    sizeof(long double) % sizeof(int32_t) == 0,
-    "bit width of long double is a multiple of bit width of int32_t");
+#  ifndef _MSC_VER
+  _Static_assert
+#  else
+  static_assert
+#  endif
+    (sizeof(long double) % sizeof(int32_t) == 0,
+     "bit width of long double is a multiple of bit width of int32_t");
   union U
   {
     long double l;

From c56f1672ed8e7c8cb5af5c265102ff87bd12185b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 8 Feb 2024 14:56:10 +0000
Subject: [PATCH 9/9] C library: do not flag float overflow with HUGE_VAL

Visual Studio uses `1.000000e+300 * 1.000000e+300` as value behind the
`HUGE_VAL` macro. We should not report an overflow for this approach of
producing infinity.
---
 src/ansi-c/library/math.c | 54 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 54 insertions(+)

diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index e10aabdc9b4..32a460297e5 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -2558,7 +2558,10 @@ double exp(double x)
   else if(x > 1024.0 * M_LN2)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return HUGE_VAL;
+#pragma CPROVER check pop
   }
 
   // Nicol N. Schraudolph: A Fast, Compact Approximation of the Exponential
@@ -2632,7 +2635,10 @@ float expf(float x)
   else if(x > 128.0f * (float)M_LN2)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return HUGE_VALF;
+#pragma CPROVER check pop
   }
 
   // 23 is 32 - 1 sign bit - 8 exponent bits
@@ -2708,7 +2714,10 @@ long double expl(long double x)
   else if(x > 16384.0l * M_LN2)
   {
     errno = ERANGE;
+#  pragma CPROVER check push
+#  pragma CPROVER check disable "float-overflow"
     return HUGE_VALL;
+#  pragma CPROVER check pop
   }
   // 16 is 32 - 1 sign bit - 15 exponent bits
   int32_t bias = (1 << 16) * ((1 << 14) - 1);
@@ -2773,7 +2782,10 @@ double log(double x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VAL;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signd(x))
   {
@@ -2838,7 +2850,10 @@ float logf(float x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VALF;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signf(x))
   {
@@ -2904,7 +2919,10 @@ long double logl(long double x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VALL;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signld(x))
   {
@@ -2975,7 +2993,10 @@ double log2(double x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VAL;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signd(x))
   {
@@ -3039,7 +3060,10 @@ float log2f(float x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VALF;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signf(x))
   {
@@ -3104,7 +3128,10 @@ long double log2l(long double x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VALL;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signld(x))
   {
@@ -3175,7 +3202,10 @@ double log10(double x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VAL;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signd(x))
   {
@@ -3242,7 +3272,10 @@ float log10f(float x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VALF;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signf(x))
   {
@@ -3309,7 +3342,10 @@ long double log10l(long double x)
   else if(fpclassify(x) == FP_ZERO)
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return -HUGE_VALL;
+#pragma CPROVER check pop
   }
   else if(__CPROVER_signld(x))
   {
@@ -3441,10 +3477,13 @@ double pow(double x, double y)
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signd(y))
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     if(__CPROVER_signd(x) && nearbyint(y) == y && fabs(fmod(y, 2.0)) == 1.0)
       return -HUGE_VAL;
     else
       return HUGE_VAL;
+#pragma CPROVER check pop
   }
   else if(isnan(x) || isnan(y))
 #pragma CPROVER check push
@@ -3479,7 +3518,10 @@ double pow(double x, double y)
   if(fabs(mult_result) > (double)(1 << 30))
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return y > 0.0 ? HUGE_VAL : 0.0;
+#pragma CPROVER check pop
   }
 #if !defined(__BYTE_ORDER__) || __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__
   u.i[1] = (int32_t)mult_result + (bias + exp_c);
@@ -3583,6 +3625,8 @@ float powf(float x, float y)
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signf(y))
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     if(
       __CPROVER_signf(x) && nearbyintf(y) == y && fabsf(fmodf(y, 2.0f)) == 1.0f)
     {
@@ -3590,6 +3634,7 @@ float powf(float x, float y)
     }
     else
       return HUGE_VALF;
+#pragma CPROVER check pop
   }
   else if(isnanf(x) || isnanf(y))
 #pragma CPROVER check push
@@ -3619,7 +3664,10 @@ float powf(float x, float y)
   if(fabsf(mult_result) > (float)(1 << 30))
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     return y > 0.0f ? HUGE_VALF : 0.0f;
+#pragma CPROVER check pop
   }
   u.i = (int32_t)mult_result + (bias + exp_c);
   return u.f;
@@ -3722,6 +3770,8 @@ long double powl(long double x, long double y)
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signld(y))
   {
     errno = ERANGE;
+#pragma CPROVER check push
+#pragma CPROVER check disable "float-overflow"
     if(
       __CPROVER_signld(x) && nearbyintl(y) == y &&
       fabsl(fmodl(y, 2.0l)) == 1.0l)
@@ -3730,6 +3780,7 @@ long double powl(long double x, long double y)
     }
     else
       return HUGE_VALL;
+#pragma CPROVER check pop
   }
   else if(isnanl(x) || isnanl(y))
 #pragma CPROVER check push
@@ -3767,7 +3818,10 @@ long double powl(long double x, long double y)
   if(fabsl(mult_result) > (long double)(1 << 30))
   {
     errno = ERANGE;
+#  pragma CPROVER check push
+#  pragma CPROVER check disable "float-overflow"
     return y > 0.0l ? HUGE_VALL : 0.0l;
+#  pragma CPROVER check pop
   }
   int32_t result = (int32_t)mult_result + (bias + exp_c);
   union U result_u = {.i = {0}};