C library: add exp, log, pow models

The implementation follows Nicol N. Schraudolph: "A Fast, Compact
Approximation of the Exponential Function," Neural Computation 11(4),
1999 and its discussion in
https://martin.ankerl.com/2007/10/04/optimized-pow-approximation-for-java-and-c-c/.
We use lower and upper bounds to retain soundness.

Author: tautschnig

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

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

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

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

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

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

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

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

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

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