From 63789b9f3f611ac6e3960d4bc39d0d312779d976 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 4 Jul 2025 19:35:32 +0000
Subject: [PATCH 1/4] Math library models: add missing *BSD variants, cleanup

BSD systems appear to use `__` prefixed variants of several functions.
Define these as needed. Also, avoid handling some GCC-style
`__builtin_`-prefixed functions via models when others are done directly
in the type checker: do all of them in the type checker.
---
 regression/cbmc-library/__builtin_fabs/main.c |   9 --
 .../cbmc-library/__builtin_fabs/test.desc     |   8 -
 .../cbmc-library/__builtin_fabsf/main.c       |   9 --
 .../cbmc-library/__builtin_fabsf/test.desc    |   8 -
 .../cbmc-library/__builtin_fabsl/main.c       |   9 --
 .../cbmc-library/__builtin_fabsl/test.desc    |   8 -
 regression/cbmc-library/__fpclassify/main.c   |  29 ++++
 regression/cbmc-library/__isinf/main.c        |   9 --
 regression/cbmc-library/__isinf/test.desc     |   8 -
 regression/cbmc-library/__isinff/main.c       |   9 --
 regression/cbmc-library/__isinff/test.desc    |   8 -
 regression/cbmc-library/__isinfl/main.c       |   9 --
 regression/cbmc-library/__isinfl/test.desc    |   8 -
 regression/cbmc-library/__isnan/main.c        |   9 --
 regression/cbmc-library/__isnan/test.desc     |   8 -
 regression/cbmc-library/__isnanf/main.c       |   9 --
 regression/cbmc-library/__isnanf/test.desc    |   8 -
 regression/cbmc-library/__isnanl/main.c       |   9 --
 regression/cbmc-library/__isnanl/test.desc    |   8 -
 regression/cbmc-library/__isnormalf/main.c    |   9 --
 regression/cbmc-library/__isnormalf/test.desc |   8 -
 regression/cbmc-library/__signbit/main.c      |   9 --
 regression/cbmc-library/__signbit/test.desc   |   8 -
 regression/cbmc-library/__signbitf/main.c     |   9 --
 regression/cbmc-library/__signbitf/test.desc  |   8 -
 regression/cbmc-library/isfinite/main.c       |  15 +-
 regression/cbmc-library/isfinite/test.desc    |   4 +-
 regression/cbmc-library/isinf/main.c          |  16 ++
 regression/cbmc-library/isinff/main.c         |   9 --
 regression/cbmc-library/isinff/test.desc      |   8 -
 regression/cbmc-library/isinfl/main.c         |   9 --
 regression/cbmc-library/isinfl/test.desc      |   8 -
 regression/cbmc-library/isnanf/main.c         |   9 --
 regression/cbmc-library/isnanf/test.desc      |   8 -
 regression/cbmc-library/isnanl/main.c         |   9 --
 regression/cbmc-library/isnanl/test.desc      |   8 -
 regression/cbmc-library/isnormal/main.c       |   7 +-
 regression/cbmc-library/isnormal/test.desc    |   4 +-
 regression/cbmc-library/signbit/main.c        |   7 +
 src/ansi-c/c_typecheck_expr.cpp               |  29 ++--
 src/ansi-c/library/math.c                     | 143 ++++++++++--------
 src/ansi-c/library_check.sh                   |   7 +
 42 files changed, 175 insertions(+), 358 deletions(-)
 delete mode 100644 regression/cbmc-library/__builtin_fabs/main.c
 delete mode 100644 regression/cbmc-library/__builtin_fabs/test.desc
 delete mode 100644 regression/cbmc-library/__builtin_fabsf/main.c
 delete mode 100644 regression/cbmc-library/__builtin_fabsf/test.desc
 delete mode 100644 regression/cbmc-library/__builtin_fabsl/main.c
 delete mode 100644 regression/cbmc-library/__builtin_fabsl/test.desc
 delete mode 100644 regression/cbmc-library/__isinf/main.c
 delete mode 100644 regression/cbmc-library/__isinf/test.desc
 delete mode 100644 regression/cbmc-library/__isinff/main.c
 delete mode 100644 regression/cbmc-library/__isinff/test.desc
 delete mode 100644 regression/cbmc-library/__isinfl/main.c
 delete mode 100644 regression/cbmc-library/__isinfl/test.desc
 delete mode 100644 regression/cbmc-library/__isnan/main.c
 delete mode 100644 regression/cbmc-library/__isnan/test.desc
 delete mode 100644 regression/cbmc-library/__isnanf/main.c
 delete mode 100644 regression/cbmc-library/__isnanf/test.desc
 delete mode 100644 regression/cbmc-library/__isnanl/main.c
 delete mode 100644 regression/cbmc-library/__isnanl/test.desc
 delete mode 100644 regression/cbmc-library/__isnormalf/main.c
 delete mode 100644 regression/cbmc-library/__isnormalf/test.desc
 delete mode 100644 regression/cbmc-library/__signbit/main.c
 delete mode 100644 regression/cbmc-library/__signbit/test.desc
 delete mode 100644 regression/cbmc-library/__signbitf/main.c
 delete mode 100644 regression/cbmc-library/__signbitf/test.desc
 delete mode 100644 regression/cbmc-library/isinff/main.c
 delete mode 100644 regression/cbmc-library/isinff/test.desc
 delete mode 100644 regression/cbmc-library/isinfl/main.c
 delete mode 100644 regression/cbmc-library/isinfl/test.desc
 delete mode 100644 regression/cbmc-library/isnanf/main.c
 delete mode 100644 regression/cbmc-library/isnanf/test.desc
 delete mode 100644 regression/cbmc-library/isnanl/main.c
 delete mode 100644 regression/cbmc-library/isnanl/test.desc

diff --git a/regression/cbmc-library/__builtin_fabs/main.c b/regression/cbmc-library/__builtin_fabs/main.c
deleted file mode 100644
index 38b521fe15c..00000000000
--- a/regression/cbmc-library/__builtin_fabs/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_fabs();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_fabs/test.desc b/regression/cbmc-library/__builtin_fabs/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabs/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__builtin_fabsf/main.c b/regression/cbmc-library/__builtin_fabsf/main.c
deleted file mode 100644
index 7c4cc5cc1fd..00000000000
--- a/regression/cbmc-library/__builtin_fabsf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_fabsf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_fabsf/test.desc b/regression/cbmc-library/__builtin_fabsf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabsf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__builtin_fabsl/main.c b/regression/cbmc-library/__builtin_fabsl/main.c
deleted file mode 100644
index 6e69656f497..00000000000
--- a/regression/cbmc-library/__builtin_fabsl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __builtin_fabsl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__builtin_fabsl/test.desc b/regression/cbmc-library/__builtin_fabsl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__builtin_fabsl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__fpclassify/main.c b/regression/cbmc-library/__fpclassify/main.c
index 8b05699e4a6..fbbeffb63a6 100644
--- a/regression/cbmc-library/__fpclassify/main.c
+++ b/regression/cbmc-library/__fpclassify/main.c
@@ -1,4 +1,5 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 #ifdef __GNUC__
@@ -49,5 +50,33 @@ int main(void)
   simplifiedInductiveStepHunt(g);
 #endif
 
+// Visual Studio needs to be 2013 onwards
+#if defined(_MSC_VER) && !defined(__CYGWIN__) && _MSC_VER < 1800
+
+  // see http://www.johndcook.com/math_h.html
+
+#else
+  assert(fpclassify(DBL_MAX + DBL_MAX) == FP_INFINITE);
+  assert(fpclassify(0 * (DBL_MAX + DBL_MAX)) == FP_NAN);
+  assert(fpclassify(1.0) == FP_NORMAL);
+  assert(fpclassify(DBL_MIN) == FP_NORMAL);
+  assert(fpclassify(DBL_MIN / 2) == FP_SUBNORMAL);
+  assert(fpclassify(-0.0) == FP_ZERO);
+#endif
+
+#if !defined(__clang__) && defined(__GNUC__)
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MAX + DBL_MAX) == 1);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, 0 * (DBL_MAX + DBL_MAX)) == 0);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, 1.0) == 2);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN) == 2);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN / 2) == 3);
+  assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0) == 4);
+
+  // these are compile-time
+  _Static_assert(
+    __builtin_fpclassify(0, 1, 2, 3, 4, -0.0) == 4,
+    "__builtin_fpclassify is constant");
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/__isinf/main.c b/regression/cbmc-library/__isinf/main.c
deleted file mode 100644
index 3441084533d..00000000000
--- a/regression/cbmc-library/__isinf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isinf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isinf/test.desc b/regression/cbmc-library/__isinf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isinff/main.c b/regression/cbmc-library/__isinff/main.c
deleted file mode 100644
index 446e25a9512..00000000000
--- a/regression/cbmc-library/__isinff/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isinff();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isinff/test.desc b/regression/cbmc-library/__isinff/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinff/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isinfl/main.c b/regression/cbmc-library/__isinfl/main.c
deleted file mode 100644
index df21c681f43..00000000000
--- a/regression/cbmc-library/__isinfl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isinfl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isinfl/test.desc b/regression/cbmc-library/__isinfl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isinfl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnan/main.c b/regression/cbmc-library/__isnan/main.c
deleted file mode 100644
index 3bd8ba542ca..00000000000
--- a/regression/cbmc-library/__isnan/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnan();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnan/test.desc b/regression/cbmc-library/__isnan/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnan/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnanf/main.c b/regression/cbmc-library/__isnanf/main.c
deleted file mode 100644
index 074fea3bf29..00000000000
--- a/regression/cbmc-library/__isnanf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnanf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnanf/test.desc b/regression/cbmc-library/__isnanf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnanf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnanl/main.c b/regression/cbmc-library/__isnanl/main.c
deleted file mode 100644
index bdda6af323e..00000000000
--- a/regression/cbmc-library/__isnanl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnanl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnanl/test.desc b/regression/cbmc-library/__isnanl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnanl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__isnormalf/main.c b/regression/cbmc-library/__isnormalf/main.c
deleted file mode 100644
index d21572bc163..00000000000
--- a/regression/cbmc-library/__isnormalf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __isnormalf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__isnormalf/test.desc b/regression/cbmc-library/__isnormalf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__isnormalf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__signbit/main.c b/regression/cbmc-library/__signbit/main.c
deleted file mode 100644
index e1147fa1a82..00000000000
--- a/regression/cbmc-library/__signbit/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __signbit();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__signbit/test.desc b/regression/cbmc-library/__signbit/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__signbit/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/__signbitf/main.c b/regression/cbmc-library/__signbitf/main.c
deleted file mode 100644
index a34833282f3..00000000000
--- a/regression/cbmc-library/__signbitf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  __signbitf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/__signbitf/test.desc b/regression/cbmc-library/__signbitf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/__signbitf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isfinite/main.c b/regression/cbmc-library/isfinite/main.c
index 9a739d27435..cb7aeb77c19 100644
--- a/regression/cbmc-library/isfinite/main.c
+++ b/regression/cbmc-library/isfinite/main.c
@@ -3,7 +3,18 @@
 
 int main()
 {
-  isfinite();
-  assert(0);
+  assert(isfinite(1.0));
+  assert(isfinite(1.0f));
+  assert(isfinite(1.0l));
+  float f;
+  assert(
+    !!isfinite(f) == (fpclassify(f) != FP_NAN && fpclassify(f) != FP_INFINITE));
+  double d;
+  assert(
+    !!isfinite(d) == (fpclassify(d) != FP_NAN && fpclassify(d) != FP_INFINITE));
+  long double ld;
+  assert(
+    !!isfinite(ld) ==
+    (fpclassify(ld) != FP_NAN && fpclassify(ld) != FP_INFINITE));
   return 0;
 }
diff --git a/regression/cbmc-library/isfinite/test.desc b/regression/cbmc-library/isfinite/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/isfinite/test.desc
+++ b/regression/cbmc-library/isfinite/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/isinf/main.c b/regression/cbmc-library/isinf/main.c
index 37fe2cc5d9e..18b7bb4062c 100644
--- a/regression/cbmc-library/isinf/main.c
+++ b/regression/cbmc-library/isinf/main.c
@@ -1,4 +1,5 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 #ifdef __GNUC__
@@ -21,5 +22,20 @@ int main(void)
   f00(f);
 #endif
 
+#if !defined(__clang__) && defined(__GNUC__)
+  assert(__builtin_isinf(DBL_MAX + DBL_MAX) == 1);
+  assert(__builtin_isinf(0.0) == 0);
+  assert(__builtin_isinf(-(DBL_MAX + DBL_MAX)) == 1);
+
+  assert(__builtin_isinf_sign(DBL_MAX + DBL_MAX) == 1);
+  assert(__builtin_isinf_sign(0.0) == 0);
+  assert(__builtin_isinf_sign(-(DBL_MAX + DBL_MAX)) == -1);
+
+  _Static_assert(!__builtin_isinf(0.0), "__builtin_isinf is constant");
+
+  _Static_assert(
+    __builtin_isinf_sign(0.0) == 0, "__builtin_isinf_sign is constant");
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/isinff/main.c b/regression/cbmc-library/isinff/main.c
deleted file mode 100644
index 083703644b2..00000000000
--- a/regression/cbmc-library/isinff/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isinff();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isinff/test.desc b/regression/cbmc-library/isinff/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isinff/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isinfl/main.c b/regression/cbmc-library/isinfl/main.c
deleted file mode 100644
index f8fcfd36425..00000000000
--- a/regression/cbmc-library/isinfl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isinfl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isinfl/test.desc b/regression/cbmc-library/isinfl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isinfl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isnanf/main.c b/regression/cbmc-library/isnanf/main.c
deleted file mode 100644
index 34b8ebb4296..00000000000
--- a/regression/cbmc-library/isnanf/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isnanf();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isnanf/test.desc b/regression/cbmc-library/isnanf/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isnanf/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isnanl/main.c b/regression/cbmc-library/isnanl/main.c
deleted file mode 100644
index ef90ee15aa9..00000000000
--- a/regression/cbmc-library/isnanl/main.c
+++ /dev/null
@@ -1,9 +0,0 @@
-#include <assert.h>
-#include <math.h>
-
-int main()
-{
-  isnanl();
-  assert(0);
-  return 0;
-}
diff --git a/regression/cbmc-library/isnanl/test.desc b/regression/cbmc-library/isnanl/test.desc
deleted file mode 100644
index 9542d988e8d..00000000000
--- a/regression/cbmc-library/isnanl/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-KNOWNBUG
-main.c
---pointer-check --bounds-check
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/regression/cbmc-library/isnormal/main.c b/regression/cbmc-library/isnormal/main.c
index d4a976517e3..927306ed586 100644
--- a/regression/cbmc-library/isnormal/main.c
+++ b/regression/cbmc-library/isnormal/main.c
@@ -1,9 +1,12 @@
 #include <assert.h>
+#include <float.h>
 #include <math.h>
 
 int main()
 {
-  isnormal();
-  assert(0);
+#if !defined(__clang__) && defined(__GNUC__)
+  _Static_assert(__builtin_isnormal(DBL_MIN), "__builtin_isnormal is constant");
+#endif
+
   return 0;
 }
diff --git a/regression/cbmc-library/isnormal/test.desc b/regression/cbmc-library/isnormal/test.desc
index 9542d988e8d..9efefbc7362 100644
--- a/regression/cbmc-library/isnormal/test.desc
+++ b/regression/cbmc-library/isnormal/test.desc
@@ -1,6 +1,6 @@
-KNOWNBUG
+CORE
 main.c
---pointer-check --bounds-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/cbmc-library/signbit/main.c b/regression/cbmc-library/signbit/main.c
index 111356bcd36..6e0858bf1f3 100644
--- a/regression/cbmc-library/signbit/main.c
+++ b/regression/cbmc-library/signbit/main.c
@@ -3,6 +3,13 @@
 
 int main(int argc, char **argv)
 {
+  assert(signbit(-1.0) != 0);
+  assert(signbit(1.0) == 0);
+#if !defined(__APPLE__) || __ENVIRONMENT_OS_VERSION_MIN_REQUIRED__ >= 150000
+  assert(signbit(-1.0l) != 0);
+#endif
+  assert(signbit(1.0l) == 0);
+
   float f = -0x1p-129f;
   float g = 0x1p-129f;
   float target = 0x0;
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index d2219a7a29a..8876c9c81f3 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -3228,10 +3228,11 @@ exprt c_typecheck_baset::do_special_functions(
             arguments[4],
             arguments[3])))); // subnormal
   }
-  else if(identifier==CPROVER_PREFIX "isnanf" ||
-          identifier==CPROVER_PREFIX "isnand" ||
-          identifier==CPROVER_PREFIX "isnanld" ||
-          identifier=="__builtin_isnan")
+  else if(
+    identifier == CPROVER_PREFIX "isnanf" ||
+    identifier == CPROVER_PREFIX "isnand" ||
+    identifier == CPROVER_PREFIX "isnanld" || identifier == "__builtin_isnan" ||
+    identifier == "__builtin_isnanf" || identifier == "__builtin_isnanl")
   {
     if(expr.arguments().size()!=1)
     {
@@ -3247,9 +3248,11 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt::conditional_cast(isnan_expr, expr.type());
   }
-  else if(identifier==CPROVER_PREFIX "isfinitef" ||
-          identifier==CPROVER_PREFIX "isfinited" ||
-          identifier==CPROVER_PREFIX "isfiniteld")
+  else if(
+    identifier == CPROVER_PREFIX "isfinitef" ||
+    identifier == CPROVER_PREFIX "isfinited" ||
+    identifier == CPROVER_PREFIX "isfiniteld" ||
+    identifier == "__builtin_isfinite")
   {
     if(expr.arguments().size()!=1)
     {
@@ -3322,7 +3325,8 @@ exprt c_typecheck_baset::do_special_functions(
     identifier == CPROVER_PREFIX "imaxabs" ||
     identifier == CPROVER_PREFIX "fabs" ||
     identifier == CPROVER_PREFIX "fabsf" ||
-    identifier == CPROVER_PREFIX "fabsl")
+    identifier == CPROVER_PREFIX "fabsl" || identifier == "__builtin_fabs" ||
+    identifier == "__builtin_fabsf" || identifier == "__builtin_fabsl")
   {
     if(expr.arguments().size()!=1)
     {
@@ -3432,10 +3436,11 @@ exprt c_typecheck_baset::do_special_functions(
 
     return std::move(old_expr);
   }
-  else if(identifier==CPROVER_PREFIX "isinff" ||
-          identifier==CPROVER_PREFIX "isinfd" ||
-          identifier==CPROVER_PREFIX "isinfld" ||
-          identifier=="__builtin_isinf")
+  else if(
+    identifier == CPROVER_PREFIX "isinff" ||
+    identifier == CPROVER_PREFIX "isinfd" ||
+    identifier == CPROVER_PREFIX "isinfld" || identifier == "__builtin_isinf" ||
+    identifier == "__builtin_isinff" || identifier == "__builtin_isinfl")
   {
     if(expr.arguments().size()!=1)
     {
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
index c8cf190fc8e..4ebb0454e1e 100644
--- a/src/ansi-c/library/math.c
+++ b/src/ansi-c/library/math.c
@@ -19,27 +19,6 @@ float fabsf(float f)
   return __CPROVER_fabsf(f);
 }
 
-/* FUNCTION: __builtin_fabs */
-
-double __builtin_fabs(double d)
-{
-  return __CPROVER_fabs(d);
-}
-
-/* FUNCTION: __builtin_fabsl */
-
-long double __builtin_fabsl(long double d)
-{
-  return __CPROVER_fabsl(d);
-}
-
-/* FUNCTION: __builtin_fabsf */
-
-float __builtin_fabsf(float f)
-{
-  return __CPROVER_fabsf(f);
-}
-
 /* FUNCTION: __CPROVER_isgreaterf */
 
 int __CPROVER_isgreaterf(float f, float g) { return f > g; }
@@ -112,6 +91,27 @@ int __finitef(float f) { return __CPROVER_isfinitef(f); }
 
 int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); }
 
+/* FUNCTION: __isfinitef */
+
+int __isfinitef(float f)
+{
+  return __CPROVER_isfinitef(f);
+}
+
+/* FUNCTION: __isfinite */
+
+int __isfinite(double d)
+{
+  return __CPROVER_isfinited(d);
+}
+
+/* FUNCTION: __isfinitel */
+
+int __isfinitel(long double ld)
+{
+  return __CPROVER_isfiniteld(ld);
+}
+
 /* FUNCTION: isinf */
 
 #undef isinf
@@ -172,6 +172,13 @@ int __isnan(double d)
   return __CPROVER_isnand(d);
 }
 
+/* FUNCTION: __isnand */
+
+int __isnand(double d)
+{
+  return __CPROVER_isnand(d);
+}
+
 /* FUNCTION: __isnanf */
 
 int __isnanf(float f)
@@ -216,6 +223,20 @@ int __isnormalf(float f)
   return __CPROVER_isnormalf(f);
 }
 
+/* FUNCTION: __isnormal */
+
+int __isnormal(double d)
+{
+  return __CPROVER_isnormald(d);
+}
+
+/* FUNCTION: __isnormall */
+
+int __isnormall(long double ld)
+{
+  return __CPROVER_isnormalld(ld);
+}
+
 /* FUNCTION: __builtin_isinf */
 
 int __builtin_isinf(double d)
@@ -330,7 +351,14 @@ int __signbitf(float f)
 
 /* FUNCTION: __signbit */
 
-int __signbit(double ld)
+int __signbit(double d)
+{
+  return __CPROVER_signd(d);
+}
+
+/* FUNCTION: __signbitl */
+
+int __signbitl(long double ld)
 {
   return __CPROVER_signld(ld);
 }
@@ -3044,8 +3072,6 @@ long double log10l(long double x)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-double __builtin_inf(void);
-
 double pow(double x, double y)
 {
   // see man pow (https://linux.die.net/man/3/pow)
@@ -3078,7 +3104,7 @@ double pow(double x, double y)
     else if(__CPROVER_signd(y))
     {
       if(fabs(x) < 1.0)
-        return __builtin_inf();
+        return __CPROVER_inf();
       else
         return +0.0;
     }
@@ -3087,7 +3113,7 @@ double pow(double x, double y)
       if(fabs(x) < 1.0)
         return +0.0;
       else
-        return __builtin_inf();
+        return __CPROVER_inf();
     }
   }
   else if(isinf(x) && __CPROVER_signd(x))
@@ -3102,9 +3128,9 @@ double pow(double x, double y)
     else
     {
       if(nearbyint(y) == y && fabs(fmod(y, 2.0)) == 1.0)
-        return -__builtin_inf();
+        return -__CPROVER_inf();
       else
-        return __builtin_inf();
+        return __CPROVER_inf();
     }
   }
   else if(isinf(x) && !__CPROVER_signd(x))
@@ -3112,7 +3138,7 @@ double pow(double x, double y)
     if(__CPROVER_signd(y))
       return +0.0;
     else
-      return __builtin_inf();
+      return __CPROVER_inf();
   }
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signd(y))
   {
@@ -3192,8 +3218,6 @@ double pow(double x, double y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-float __builtin_inff(void);
-
 float powf(float x, float y)
 {
   // see man pow (https://linux.die.net/man/3/pow)
@@ -3226,7 +3250,7 @@ float powf(float x, float y)
     else if(__CPROVER_signf(y))
     {
       if(fabsf(x) < 1.0f)
-        return __builtin_inff();
+        return __CPROVER_inff();
       else
         return +0.0f;
     }
@@ -3235,7 +3259,7 @@ float powf(float x, float y)
       if(fabsf(x) < 1.0f)
         return +0.0f;
       else
-        return __builtin_inff();
+        return __CPROVER_inff();
     }
   }
   else if(isinff(x) && __CPROVER_signf(x))
@@ -3250,9 +3274,9 @@ float powf(float x, float y)
     else
     {
       if(nearbyintf(y) == y && fabsf(fmodf(y, 2.0f)) == 1.0f)
-        return -__builtin_inff();
+        return -__CPROVER_inff();
       else
-        return __builtin_inff();
+        return __CPROVER_inff();
     }
   }
   else if(isinff(x) && !__CPROVER_signf(x))
@@ -3260,7 +3284,7 @@ float powf(float x, float y)
     if(__CPROVER_signf(y))
       return +0.0f;
     else
-      return __builtin_inff();
+      return __CPROVER_inff();
   }
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signf(y))
   {
@@ -3337,8 +3361,6 @@ float powf(float x, float y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-long double __builtin_infl(void);
-
 long double powl(long double x, long double y)
 {
   // see man pow (https://linux.die.net/man/3/pow)
@@ -3371,7 +3393,7 @@ long double powl(long double x, long double y)
     else if(__CPROVER_signld(y))
     {
       if(fabsl(x) < 1.0l)
-        return __builtin_infl();
+        return __CPROVER_infl();
       else
         return +0.0l;
     }
@@ -3380,7 +3402,7 @@ long double powl(long double x, long double y)
       if(fabsl(x) < 1.0l)
         return +0.0l;
       else
-        return __builtin_infl();
+        return __CPROVER_infl();
     }
   }
   else if(isinfl(x) && __CPROVER_signld(x))
@@ -3395,9 +3417,9 @@ long double powl(long double x, long double y)
     else
     {
       if(nearbyintl(y) == y && fabsl(fmodl(y, 2.0l)) == 1.0l)
-        return -__builtin_infl();
+        return -__CPROVER_infl();
       else
-        return __builtin_infl();
+        return __CPROVER_infl();
     }
   }
   else if(isinfl(x) && !__CPROVER_signld(x))
@@ -3405,7 +3427,7 @@ long double powl(long double x, long double y)
     if(__CPROVER_signld(y))
       return +0.0f;
     else
-      return __builtin_infl();
+      return __CPROVER_infl();
   }
   else if(fpclassify(x) == FP_ZERO && __CPROVER_signld(y))
   {
@@ -3486,8 +3508,6 @@ long double powl(long double x, long double y)
 #  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)
@@ -3519,7 +3539,7 @@ double fma(double x, double y, double z)
   if(isinf(x_times_y))
   {
     feraiseexcept(FE_OVERFLOW);
-    return __CPROVER_signd(x_times_y) ? -__builtin_inf() : __builtin_inf();
+    return __CPROVER_signd(x_times_y) ? -__CPROVER_inf() : __CPROVER_inf();
   }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
 
@@ -3538,8 +3558,6 @@ double fma(double x, double y, double z)
 #  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)
@@ -3571,7 +3589,7 @@ float fmaf(float x, float y, float z)
   if(isinff(x_times_y))
   {
     feraiseexcept(FE_OVERFLOW);
-    return __CPROVER_signf(x_times_y) ? -__builtin_inff() : __builtin_inff();
+    return __CPROVER_signf(x_times_y) ? -__CPROVER_inff() : __CPROVER_inff();
   }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
 
@@ -3595,8 +3613,6 @@ float fmaf(float x, float y, float z)
 #  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)
@@ -3631,7 +3647,7 @@ long double fmal(long double x, long double y, long double z)
   if(isinfl(x_times_y))
   {
     feraiseexcept(FE_OVERFLOW);
-    return __CPROVER_signld(x_times_y) ? -__builtin_infl() : __builtin_infl();
+    return __CPROVER_signld(x_times_y) ? -__CPROVER_infl() : __CPROVER_infl();
   }
   // TODO: detect underflow (FE_UNDERFLOW), return +/- 0
 
@@ -3658,8 +3674,6 @@ long double fmal(long double x, long double y, long double z)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-double __builtin_inf(void);
-
 double __builtin_powi(double x, int y)
 {
   // see man pow (https://linux.die.net/man/3/pow), specialized for y being an
@@ -3687,9 +3701,9 @@ double __builtin_powi(double x, int y)
     else
     {
       if(y % 2 == 1)
-        return -__builtin_inf();
+        return -__CPROVER_inf();
       else
-        return __builtin_inf();
+        return __CPROVER_inf();
     }
   }
   else if(isinf(x) && !__CPROVER_signd(x))
@@ -3697,7 +3711,7 @@ double __builtin_powi(double x, int y)
     if(y < 0)
       return +0.0;
     else
-      return __builtin_inf();
+      return __CPROVER_inf();
   }
   else if(fpclassify(x) == FP_ZERO && y < 0)
   {
@@ -3777,8 +3791,6 @@ double __builtin_powi(double x, int y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-float __builtin_inff(void);
-
 float __builtin_powif(float x, int y)
 {
   // see man pow (https://linux.die.net/man/3/pow), specialized for y being an
@@ -3806,9 +3818,9 @@ float __builtin_powif(float x, int y)
     else
     {
       if(y % 2 == 1)
-        return -__builtin_inff();
+        return -__CPROVER_inff();
       else
-        return __builtin_inff();
+        return __CPROVER_inff();
     }
   }
   else if(isinff(x) && !__CPROVER_signf(x))
@@ -3816,7 +3828,7 @@ float __builtin_powif(float x, int y)
     if(y < 0)
       return +0.0f;
     else
-      return __builtin_inff();
+      return __CPROVER_inff();
   }
   else if(fpclassify(x) == FP_ZERO && y < 0)
   {
@@ -3892,7 +3904,6 @@ float __builtin_powif(float x, int y)
 
 int32_t __VERIFIER_nondet_int32_t(void);
 
-long double __builtin_infl(void);
 double __builtin_powi(double, int);
 
 long double __builtin_powil(long double x, int y)
@@ -3922,9 +3933,9 @@ long double __builtin_powil(long double x, int y)
     else
     {
       if(y % 2 == 1)
-        return -__builtin_infl();
+        return -__CPROVER_infl();
       else
-        return __builtin_infl();
+        return __CPROVER_infl();
     }
   }
   else if(isinf(x) && !__CPROVER_signld(x))
@@ -3932,7 +3943,7 @@ long double __builtin_powil(long double x, int y)
     if(y < 0)
       return +0.0f;
     else
-      return __builtin_infl();
+      return __CPROVER_infl();
   }
   else if(fpclassify(x) == FP_ZERO && y < 0)
   {
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
index 6883984ae26..5902b79aba1 100755
--- a/src/ansi-c/library_check.sh
+++ b/src/ansi-c/library_check.sh
@@ -68,12 +68,19 @@ perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
 perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen
 perl -p -i -e 's/^fopen64\n//' __functions # fopen
 perl -p -i -e 's/^freopen64\n//' __functions # freopen
+perl -p -i -e 's/^isinf[fl]\n//' __functions # isinf
+perl -p -i -e 's/^isnan[fl]\n//' __functions # isnan
 perl -p -i -e 's/^mmap64\n//' __functions # mmap
 perl -p -i -e 's/^munmap\n//' __functions # mmap-01
 perl -p -i -e 's/^__fgets_chk\n//' __functions # fgets/__fgets_chk.desc
 perl -p -i -e 's/^__fprintf_chk\n//' __functions # fprintf/__fprintf_chk.desc
 perl -p -i -e 's/^__fread_chk\n//' __functions # fread/__fread_chk.desc
+perl -p -i -e 's/^__isfinite[fl]?\n//' __functions # isfinite
+perl -p -i -e 's/^__isinf[fl]?\n//' __functions # isinf
+perl -p -i -e 's/^__isnan[dfl]?\n//' __functions # isnan
+perl -p -i -e 's/^__isnormal[fl]?\n//' __functions # isnormal
 perl -p -i -e 's/^__printf_chk\n//' __functions # printf/__printf_chk.desc
+perl -p -i -e 's/^__signbit[fl]?\n//' __functions # signbit, __signbitd
 perl -p -i -e 's/^__syslog_chk\n//' __functions # syslog/__syslog_chk.desc
 perl -p -i -e 's/^_syslog\$DARWIN_EXTSN\n//' __functions # syslog/test.desc
 perl -p -i -e 's/^__time64\n//' __functions # time

From 886547d8f79b9324fb257b88e55833d3053b4901 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 29 Sep 2023 11:45:30 +0000
Subject: [PATCH 2/4] C library: Refine and improve stdio models

Fixes portability to FreeBSD, which redefines several functions as
macros that would only conditionally call that function. Also, ensure
that stdin/stdout/stderr point to valid objects when those are
fdopen'ed.
---
 .github/workflows/bsd.yaml                    |   6 +
 regression/cbmc-library/fileno/main.c         |   8 +-
 regression/cbmc-library/tolower/main.c        |   4 +
 regression/cbmc-library/toupper/main.c        |   4 +
 .../variant_multidimensional_ackermann/main.c |   3 +-
 src/ansi-c/library/stdio.c                    | 145 ++++++++++++++++--
 6 files changed, 146 insertions(+), 24 deletions(-)

diff --git a/.github/workflows/bsd.yaml b/.github/workflows/bsd.yaml
index 17662383fd7..99e7ea5a37f 100644
--- a/.github/workflows/bsd.yaml
+++ b/.github/workflows/bsd.yaml
@@ -66,6 +66,7 @@ jobs:
             # gmake TAGS='[!shouldfail]' -C jbmc/unit test
             echo "Run regression tests"
             gmake -C regression/cbmc test
+            gmake -C regression/cbmc-library test
             # gmake -C regression test-parallel JOBS=2
             # gmake -C regression/cbmc test-paths-lifo
             # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
@@ -128,6 +129,10 @@ jobs:
             # gmake TAGS='[!shouldfail]' -C jbmc/unit test
             echo "Run regression tests"
             gmake -C regression/cbmc test
+            # TODO: fileno and *fprintf tests are failing, requires debugging
+            # https://github.com/openbsd/src/blob/master/include/stdio.h may be
+            # useful (likely need to allocate __sF)
+            gmake -C regression/cbmc-library test || true
             # gmake -C regression test-parallel JOBS=2
             # gmake -C regression/cbmc test-paths-lifo
             # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
@@ -193,6 +198,7 @@ jobs:
             echo "Run regression tests"
             # TODO: we need to model some more library functions
             gmake -C regression/cbmc test || true
+            gmake -C regression/cbmc-library test || true
             # gmake -C regression test-parallel JOBS=2
             # gmake -C regression/cbmc test-paths-lifo
             # env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
diff --git a/regression/cbmc-library/fileno/main.c b/regression/cbmc-library/fileno/main.c
index c186de1b88d..7820f7ebe28 100644
--- a/regression/cbmc-library/fileno/main.c
+++ b/regression/cbmc-library/fileno/main.c
@@ -3,14 +3,10 @@
 
 int main()
 {
-  // requires initialization of stdin/stdout/stderr
-  // assert(fileno(stdin) == 0);
-  // assert(fileno(stdout) == 1);
-  // assert(fileno(stderr) == 2);
-
   int fd;
   FILE *some_file = fdopen(fd, "");
-  assert(fileno(some_file) >= -1);
+  if(some_file)
+    assert(fileno(some_file) >= -1);
 
   return 0;
 }
diff --git a/regression/cbmc-library/tolower/main.c b/regression/cbmc-library/tolower/main.c
index 8e528b4a9e1..8568da85a97 100644
--- a/regression/cbmc-library/tolower/main.c
+++ b/regression/cbmc-library/tolower/main.c
@@ -3,8 +3,12 @@
 
 int main()
 {
+#if !defined(__FreeBSD__) && !defined(__OpenBSD__) && !defined(__NetBSD__)
+  // We would need to model conversion tables, where each of the BSDs has their
+  // peculiar approach.
   int x;
   int r = tolower(x);
   assert(r >= x);
+#endif
   return 0;
 }
diff --git a/regression/cbmc-library/toupper/main.c b/regression/cbmc-library/toupper/main.c
index 3b98daecf37..f833a8d82d6 100644
--- a/regression/cbmc-library/toupper/main.c
+++ b/regression/cbmc-library/toupper/main.c
@@ -3,8 +3,12 @@
 
 int main()
 {
+#if !defined(__FreeBSD__) && !defined(__OpenBSD__) && !defined(__NetBSD__)
+  // We would need to model conversion tables, where each of the BSDs has their
+  // peculiar approach.
   int x;
   int r = toupper(x);
   assert(r <= x);
+#endif
   return 0;
 }
diff --git a/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c b/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c
index 7f7e5c1be1f..f8648b9fa56 100644
--- a/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c
+++ b/regression/contracts-dfcc/variant_multidimensional_ackermann/main.c
@@ -8,7 +8,8 @@ int main()
   int n = 5;
   int result = ackermann(m, n);
 
-  printf("Result of the Ackermann function: %d\n", result);
+  // we don't currently have contracts on what printf is assigning to
+  // printf("Result of the Ackermann function: %d\n", result);
   return 0;
 }
 
diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index 47a2be1ba6b..c99f7780207 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -6,15 +6,7 @@
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
-/* undefine macros in OpenBSD's stdio.h that are problematic to the checker. */
-#if defined(__OpenBSD__)
-#undef getchar
 #undef putchar
-#undef getc
-#undef feof
-#undef ferror
-#undef fileno
-#endif
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void);
 
@@ -237,7 +229,8 @@ __CPROVER_HIDE:;
   __CPROVER_set_must(stream, "closed");
 #endif
   int return_value=__VERIFIER_nondet_int();
-  free(stream);
+  if(stream != stdin && stream != stdout && stream != stderr)
+    free(stream);
   return return_value;
 }
 
@@ -253,25 +246,87 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
 FILE *fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
-  (void)handle;
+  if(handle < 0)
+  {
+    errno = EBADF;
+    return NULL;
+  }
   (void)*mode;
 #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
 #endif
 
-#if !defined(__linux__) || defined(__GLIBC__)
-  FILE *f=malloc(sizeof(FILE));
+#if defined(_WIN32) || defined(__OpenBSD__) || defined(__NetBSD__)
+  switch(handle)
+  {
+  case 0:
+    return stdin;
+  case 1:
+    return stdout;
+  case 2:
+    return stderr;
+  default:
+  {
+    FILE *f = malloc(sizeof(FILE));
+    if(f == NULL)
+      return NULL;
+    __CPROVER_assume(fileno(f) == handle);
+    return f;
+  }
+  }
 #else
-  // libraries need to expose the definition of FILE; this is the
+#  if !defined(__linux__) || defined(__GLIBC__)
+  static FILE stdin_file;
+  static FILE stdout_file;
+  static FILE stderr_file;
+#  else
+  // libraries need not expose the definition of FILE; this is the
   // case for musl
-  FILE *f=malloc(sizeof(int));
-#endif
+  static int stdin_file;
+  static int stdout_file;
+  static int stderr_file;
+#  endif
+
+  FILE *f = NULL;
+  switch(handle)
+  {
+  case 0:
+    stdin = &stdin_file;
+    __CPROVER_havoc_object(&stdin_file);
+    f = &stdin_file;
+    break;
+  case 1:
+    stdout = &stdout_file;
+    __CPROVER_havoc_object(&stdout_file);
+    f = &stdout_file;
+    break;
+  case 2:
+    stderr = &stderr_file;
+    __CPROVER_havoc_object(&stderr_file);
+    f = &stderr_file;
+    break;
+  default:
+#  if !defined(__linux__) || defined(__GLIBC__)
+    f = malloc(sizeof(FILE));
+#  else
+    f = malloc(sizeof(int));
+#  endif
+  }
 
+  if(f == NULL)
+    return NULL;
+  __CPROVER_assume(fileno(f) == handle);
   return f;
+#endif
 }
 
 /* FUNCTION: _fdopen */
@@ -291,19 +346,62 @@ FILE *fdopen(int handle, const char *mode)
 #define __CPROVER_STDLIB_H_INCLUDED
 #endif
 
+#ifndef __CPROVER_ERRNO_H_INCLUDED
+#  include <errno.h>
+#  define __CPROVER_ERRNO_H_INCLUDED
+#endif
+
 #ifdef __APPLE__
+
+#  ifndef LIBRARY_CHECK
+FILE *stdin;
+FILE *stdout;
+FILE *stderr;
+#  endif
+
 FILE *_fdopen(int handle, const char *mode)
 {
   __CPROVER_HIDE:;
-  (void)handle;
+  if(handle < 0)
+  {
+    errno = EBADF;
+    return NULL;
+  }
   (void)*mode;
 #ifdef __CPROVER_STRING_ABSTRACTION
   __CPROVER_assert(__CPROVER_is_zero_string(mode),
     "fdopen zero-termination of 2nd argument");
 #endif
 
-  FILE *f=malloc(sizeof(FILE));
+  static FILE stdin_file;
+  static FILE stdout_file;
+  static FILE stderr_file;
+
+  FILE *f = NULL;
+  switch(handle)
+  {
+  case 0:
+    stdin = &stdin_file;
+    __CPROVER_havoc_object(&stdin_file);
+    f = &stdin_file;
+    break;
+  case 1:
+    stdout = &stdout_file;
+    __CPROVER_havoc_object(&stdout_file);
+    f = &stdout_file;
+    break;
+  case 2:
+    stderr = &stderr_file;
+    __CPROVER_havoc_object(&stderr_file);
+    f = &stderr_file;
+    break;
+  default:
+    f = malloc(sizeof(FILE));
+  }
 
+  if(f == NULL)
+    return NULL;
+  __CPROVER_assume(fileno(f) == handle);
   return f;
 }
 #endif
@@ -506,6 +604,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef feof
+
 int __VERIFIER_nondet_int(void);
 
 int feof(FILE *stream)
@@ -538,6 +638,8 @@ int feof(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef ferror
+
 int __VERIFIER_nondet_int(void);
 
 int ferror(FILE *stream)
@@ -570,6 +672,8 @@ int ferror(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef fileno
+
 int __VERIFIER_nondet_int(void);
 
 int fileno(FILE *stream)
@@ -735,6 +839,8 @@ int fgetc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef getc
+
 int __VERIFIER_nondet_int(void);
 
 int getc(FILE *stream)
@@ -771,6 +877,8 @@ int getc(FILE *stream)
 #define __CPROVER_STDIO_H_INCLUDED
 #endif
 
+#undef getchar
+
 int __VERIFIER_nondet_int(void);
 
 int getchar(void)
@@ -1939,10 +2047,13 @@ FILE *__acrt_iob_func(unsigned fd)
   switch(fd)
   {
   case 0:
+    __CPROVER_havoc_object(&stdin_file);
     return &stdin_file;
   case 1:
+    __CPROVER_havoc_object(&stdout_file);
     return &stdout_file;
   case 2:
+    __CPROVER_havoc_object(&stderr_file);
     return &stderr_file;
   default:
     return (FILE *)0;

From 09260708d6d84ae362122f73353e909034d3f324 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 13 Mar 2026 13:05:01 +0000
Subject: [PATCH 3/4] C front-end: handle macOS SDK __inline_signbit* as
 special functions

On macOS, the SDK's signbit macro expands to __inline_signbitf,
__inline_signbitd, or __inline_signbitl (inline functions defined in the
SDK header). These perform union-based bit manipulation that CBMC does
not model correctly, especially for 80-bit long double on x86_64.

Handle these the same way as __builtin_signbit* by converting them
directly to sign_exprt in do_special_functions.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/ansi-c/c_typecheck_expr.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 8876c9c81f3..2ab23eab096 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -3526,12 +3526,13 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt::conditional_cast(isnormal_expr, expr.type());
   }
-  else if(identifier==CPROVER_PREFIX "signf" ||
-          identifier==CPROVER_PREFIX "signd" ||
-          identifier==CPROVER_PREFIX "signld" ||
-          identifier=="__builtin_signbit" ||
-          identifier=="__builtin_signbitf" ||
-          identifier=="__builtin_signbitl")
+  else if(
+    identifier == CPROVER_PREFIX "signf" ||
+    identifier == CPROVER_PREFIX "signd" ||
+    identifier == CPROVER_PREFIX "signld" ||
+    identifier == "__builtin_signbit" || identifier == "__builtin_signbitf" ||
+    identifier == "__builtin_signbitl" || identifier == "__inline_signbitf" ||
+    identifier == "__inline_signbitd" || identifier == "__inline_signbitl")
   {
     if(expr.arguments().size()!=1)
     {

From 5d17b248e829f86ac9481aca2d92b44cf2d559c3 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 13 Mar 2026 15:27:27 +0000
Subject: [PATCH 4/4] C library: add __ssp_real_fread model for FreeBSD SSP

On FreeBSD, _FORTIFY_SOURCE uses the SSP __ssp_redirect mechanism
which redirects fread to an inline wrapper that calls __ssp_real_fread
(the actual implementation). Add a library model for __ssp_real_fread
that delegates to fread so that CBMC can properly constrain its return
value.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 src/ansi-c/library/stdio.c | 23 ++++++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index c99f7780207..b3908323bd9 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -528,7 +528,7 @@ __CPROVER_HIDE:;
 char __VERIFIER_nondet_char(void);
 size_t __VERIFIER_nondet_size_t(void);
 
-size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
+size_t __CPROVER_fread(void *ptr, size_t size, size_t nitems, FILE *stream)
 {
 __CPROVER_HIDE:;
   size_t bytes_read = __VERIFIER_nondet_size_t();
@@ -545,8 +545,8 @@ __CPROVER_HIDE:;
   }
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
-  __CPROVER_assert(__CPROVER_get_must(stream, "open"),
-                   "fread file must be open");
+  __CPROVER_assert(
+    __CPROVER_get_must(stream, "open"), "fread file must be open");
 #endif
 
   for(size_t i = 0; i < bytes_read && i < upper_bound; i++)
@@ -557,6 +557,23 @@ __CPROVER_HIDE:;
   return bytes_read / size;
 }
 
+#ifdef __FreeBSD__
+// FreeBSD asm-renames fread to __ssp_protected_fread, which then invokes fread;
+// to make this work, a symbol __ssp_real_fread is introduced that in turn is
+// asm-renamed to fread.
+size_t __ssp_real_fread(void *ptr, size_t size, size_t nitems, FILE *stream)
+{
+__CPROVER_HIDE:;
+  return __CPROVER_fread(ptr, size, nitems, stream);
+}
+#endif
+
+size_t fread(void *ptr, size_t size, size_t nitems, FILE *stream)
+{
+__CPROVER_HIDE:;
+  return __CPROVER_fread(ptr, size, nitems, stream);
+}
+
 /* FUNCTION: __fread_chk */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED