Merge pull request #8195 from tautschnig/bugfixes/math-lib

tautschnig · web-flow · commit 9c7bccc4af40 · 2024-02-08T17:19:25.000+01:00
C library: additional floating-point functions and cleanup
diff --git a/regression/cbmc-library/feraiseexcept-01/main.c 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
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc-library/fma-01/main.c 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/log10-01/main.c 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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/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/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
+}
diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c
