Merge pull request #7906 from tautschnig/features/math-library

kroening · web-flow · commit 0ec6a1e0ca92 · 2023-10-27T13:19:56.000+01:00
C library: add exp, log, pow models
diff --git a/regression/cbmc-library/exp-01/main.c b/regression/cbmc-library/exp-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  double e = exp(1.0);
+  assert(e > 2.713 && e < 2.886);
+  return 0;
+}
diff --git a/regression/cbmc-library/exp-01/test.desc b/regression/cbmc-library/exp-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/exp2-01/main.c b/regression/cbmc-library/exp2-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  double two = exp2(1.0);
+  assert(two > 1.999 && two < 2.001);
+  return 0;
+}
diff --git a/regression/cbmc-library/exp2-01/test.desc b/regression/cbmc-library/exp2-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/exp2f-01/main.c b/regression/cbmc-library/exp2f-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float two = exp2f(1.0f);
+  assert(two > 1.999f && two < 2.001f);
+  return 0;
+}
diff --git a/regression/cbmc-library/exp2f-01/test.desc b/regression/cbmc-library/exp2f-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/exp2l-01/main.c b/regression/cbmc-library/exp2l-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  long double two = exp2l(1.0l);
+  assert(two > 1.999l && two < 2.001l);
+  return 0;
+}
diff --git a/regression/cbmc-library/exp2l-01/test.desc b/regression/cbmc-library/exp2l-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/expf-01/main.c b/regression/cbmc-library/expf-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float e = expf(1.0f);
+  assert(e > 2.713f && e < 2.886f);
+  return 0;
+}
diff --git a/regression/cbmc-library/expf-01/test.desc b/regression/cbmc-library/expf-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/expl-01/main.c b/regression/cbmc-library/expl-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  long double e = expl(1.0l);
+  assert(e > 2.713l && e < 2.886l);
+  return 0;
+}
diff --git a/regression/cbmc-library/expl-01/test.desc b/regression/cbmc-library/expl-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/log-01/main.c b/regression/cbmc-library/log-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  double one = log(M_E);
+  assert(one > 0.942 && one < 1.002);
+  return 0;
+}
diff --git a/regression/cbmc-library/log-01/test.desc b/regression/cbmc-library/log-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/logf-01/main.c b/regression/cbmc-library/logf-01/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+#ifdef _WIN32
+#  define _USE_MATH_DEFINES
+#endif
+#include <math.h>
+
+int main()
+{
+  float one = logf(M_E);
+  assert(one > 0.942f && one < 1.002f);
+  return 0;
+}
diff --git a/regression/cbmc-library/logf-01/test.desc b/regression/cbmc-library/logf-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/logl-01/main.c b/regression/cbmc-library/logl-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 = logl(M_E);
+  assert(one > 0.942l && one < 1.002l);
+  return 0;
+}
diff --git a/regression/cbmc-library/logl-01/test.desc b/regression/cbmc-library/logl-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
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  double four = pow(2.0, 2.0);
+  assert(four > 3.999 && four < 4.345);
+  return 0;
+}
diff --git a/regression/cbmc-library/pow-01/test.desc b/regression/cbmc-library/pow-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/powf-01/main.c b/regression/cbmc-library/powf-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float four = powf(2.0f, 2.0f);
+  assert(four > 3.999f && four < 4.345f);
+  return 0;
+}
diff --git a/regression/cbmc-library/powf-01/test.desc b/regression/cbmc-library/powf-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/powl-01/main.c b/regression/cbmc-library/powl-01/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  long double four = pow(2.0l, 2.0l);
+  assert(four > 3.999l && four < 4.345l);
+  return 0;
+}
diff --git a/regression/cbmc-library/powl-01/test.desc b/regression/cbmc-library/powl-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
diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh
