Merge pull request #8192 from tautschnig/features/builtin_pow

C library: model __builtin_powi{,f,l}

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

regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc

@@ -3,7 +3,7 @@ main.c
 --pointer-check _ --no-malloc-may-fail --verbosity 9
 ^EXIT=0$
 ^SIGNAL=0$
-Quick filter\: 6.* out of 67 candidates were filtered out\.
+Quick filter\: [1-9]\d* out of 67 candidates were filtered out\.
 ^\[main.pointer\_dereference.\d+\] .* SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --