C library: model __builtin_powi{,f,l}

These GCC built-ins are modelled by implementing pow{,f,l} specialised
to integral exponents (where multiple failure cases cannot occur).

Author: tautschnig

regression/cbmc-library/__builtin_powi-01/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <math.h>
+
+double __builtin_powi(double, int);
+
+int main()
+{
+  double four = __builtin_powi(2.0, 2);
+  assert(four > 3.999 && four < 4.345);
+  return 0;
+}

regression/cbmc-library/__builtin_powi-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/__builtin_powif-01/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <math.h>
+
+float __builtin_powif(float, int);
+
+int main()
+{
+  float four = __builtin_powif(2.0f, 2);
+  assert(four > 3.999f && four < 4.345f);
+  return 0;
+}

regression/cbmc-library/__builtin_powif-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/__builtin_powil-01/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <math.h>
+
+long double __builtin_powil(long double, int);
+
+int main()
+{
+  long double four = __builtin_powil(2.0l, 2);
+  assert(four > 3.999l && four < 4.345l);
+  return 0;
+}

regression/cbmc-library/__builtin_powil-01/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--float-overflow-check --nan-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring