Skip to content

Commit 4cb0a63

Browse files
authored
Merge pull request #8192 from tautschnig/features/builtin_pow
C library: model __builtin_powi{,f,l}
2 parents 2d07351 + e26fc74 commit 4cb0a63

File tree

8 files changed

+419
-1
lines changed

8 files changed

+419
-1
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
#include <math.h>
3+
4+
double __builtin_powi(double, int);
5+
6+
int main()
7+
{
8+
double four = __builtin_powi(2.0, 2);
9+
assert(four > 3.999 && four < 4.345);
10+
return 0;
11+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--float-overflow-check --nan-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
#include <math.h>
3+
4+
float __builtin_powif(float, int);
5+
6+
int main()
7+
{
8+
float four = __builtin_powif(2.0f, 2);
9+
assert(four > 3.999f && four < 4.345f);
10+
return 0;
11+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--float-overflow-check --nan-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
#include <math.h>
3+
4+
long double __builtin_powil(long double, int);
5+
6+
int main()
7+
{
8+
long double four = __builtin_powil(2.0l, 2);
9+
assert(four > 3.999l && four < 4.345l);
10+
return 0;
11+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--float-overflow-check --nan-check
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

regression/goto-synthesizer/loop_contracts_synthesis_04/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--pointer-check _ --no-malloc-may-fail --verbosity 9
44
^EXIT=0$
55
^SIGNAL=0$
6-
Quick filter\: 6.* out of 67 candidates were filtered out\.
6+
Quick filter\: [1-9]\d* out of 67 candidates were filtered out\.
77
^\[main.pointer\_dereference.\d+\] .* SUCCESS$
88
^VERIFICATION SUCCESSFUL$
99
--

0 commit comments

Comments
 (0)