diffblue · tautschnig · Jul 4, 2025 · Sep 29, 2023
@@ -63,6 +63,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
@@ -125,6 +126,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
@@ -190,6 +195,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/__builtin_fabs-01/main.c b/regression/cbmc-library/__builtin_fabs-01/main.c
diff --git a/regression/cbmc-library/__builtin_fabs-01/test.desc b/regression/cbmc-library/__builtin_fabs-01/test.desc
diff --git a/regression/cbmc-library/__builtin_fabsf-01/main.c b/regression/cbmc-library/__builtin_fabsf-01/main.c
diff --git a/regression/cbmc-library/__builtin_fabsf-01/test.desc b/regression/cbmc-library/__builtin_fabsf-01/test.desc
diff --git a/regression/cbmc-library/__builtin_fabsl-01/main.c b/regression/cbmc-library/__builtin_fabsl-01/main.c
diff --git a/regression/cbmc-library/__builtin_fabsl-01/test.desc b/regression/cbmc-library/__builtin_fabsl-01/test.desc
diff --git a/regression/cbmc-library/__builtin_huge_val-01/main.c b/regression/cbmc-library/__builtin_huge_val-01/main.c
diff --git a/regression/cbmc-library/__builtin_huge_val-01/test.desc b/regression/cbmc-library/__builtin_huge_val-01/test.desc
diff --git a/regression/cbmc-library/__builtin_huge_valf-01/main.c b/regression/cbmc-library/__builtin_huge_valf-01/main.c
diff --git a/regression/cbmc-library/__builtin_huge_valf-01/test.desc b/regression/cbmc-library/__builtin_huge_valf-01/test.desc
diff --git a/regression/cbmc-library/__builtin_huge_vall-01/main.c b/regression/cbmc-library/__builtin_huge_vall-01/main.c
diff --git a/regression/cbmc-library/__builtin_huge_vall-01/test.desc b/regression/cbmc-library/__builtin_huge_vall-01/test.desc
diff --git a/regression/cbmc-library/__builtin_inf-01/main.c b/regression/cbmc-library/__builtin_inf-01/main.c
diff --git a/regression/cbmc-library/__builtin_inf-01/test.desc b/regression/cbmc-library/__builtin_inf-01/test.desc
diff --git a/regression/cbmc-library/__builtin_inff-01/main.c b/regression/cbmc-library/__builtin_inff-01/main.c
diff --git a/regression/cbmc-library/__builtin_inff-01/test.desc b/regression/cbmc-library/__builtin_inff-01/test.desc
diff --git a/regression/cbmc-library/__builtin_infl-01/main.c b/regression/cbmc-library/__builtin_infl-01/main.c
diff --git a/regression/cbmc-library/__builtin_infl-01/test.desc b/regression/cbmc-library/__builtin_infl-01/test.desc
diff --git a/regression/cbmc-library/__builtin_isinf-01/main.c b/regression/cbmc-library/__builtin_isinf-01/main.c
diff --git a/regression/cbmc-library/__builtin_isinf-01/test.desc b/regression/cbmc-library/__builtin_isinf-01/test.desc
diff --git a/regression/cbmc-library/__builtin_isinff-01/main.c b/regression/cbmc-library/__builtin_isinff-01/main.c
diff --git a/regression/cbmc-library/__builtin_isinff-01/test.desc b/regression/cbmc-library/__builtin_isinff-01/test.desc
diff --git a/regression/cbmc-library/__builtin_isnan-01/main.c b/regression/cbmc-library/__builtin_isnan-01/main.c
diff --git a/regression/cbmc-library/__builtin_isnan-01/test.desc b/regression/cbmc-library/__builtin_isnan-01/test.desc
diff --git a/regression/cbmc-library/__builtin_isnanf-01/main.c b/regression/cbmc-library/__builtin_isnanf-01/main.c
diff --git a/regression/cbmc-library/__builtin_isnanf-01/test.desc b/regression/cbmc-library/__builtin_isnanf-01/test.desc
diff --git a/regression/cbmc-library/__fpclassify-01/main.c b/regression/cbmc-library/__fpclassify-01/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-01/main.c b/regression/cbmc-library/__isinf-01/main.c
diff --git a/regression/cbmc-library/__isinf-01/test.desc b/regression/cbmc-library/__isinf-01/test.desc
diff --git a/regression/cbmc-library/__isinff-01/main.c b/regression/cbmc-library/__isinff-01/main.c
diff --git a/regression/cbmc-library/__isinff-01/test.desc b/regression/cbmc-library/__isinff-01/test.desc