C library: implement log2{,f,l} and log10{,f,l}

Follows the same approximation approach as previously taken for log (and
logf, logl).

Author: tautschnig

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;
+}

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

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;
+}

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

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;
+}

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

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;
+}

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

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;
+}

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

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;
+}

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