diff --git a/share/libc/math.h b/share/libc/math.h
index 25c122cd2ed7a047e97c86c3be4566de0ba72acb..0a8d71de4ceb1c8ea74ebccbc61fe6858046cb8e 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -653,16 +653,44 @@ extern double expm1(double x);
extern float expm1f(float x);
extern long double expm1l(long double x);
+/*@
+ requires valid_exp: \valid(exp);
+ assigns \result, *exp \from value;
+ ensures initialization:exp:\initialized(exp);
+ */
extern double frexp(double value, int *exp);
+
+/*@
+ requires valid_exp: \valid(exp);
+ assigns \result, *exp \from value;
+ ensures initialization:exp:\initialized(exp);
+ */
extern float frexpf(float value, int *exp);
+
+/*@
+ requires valid_exp: \valid(exp);
+ assigns \result, *exp \from value;
+ ensures initialization:exp:\initialized(exp);
+ */
extern long double frexpl(long double value, int *exp);
extern int ilogb(double x);
extern int ilogbf(float x);
extern int ilogbl(long double x);
+/*@
+ assigns \result \from x, exp;
+ */
extern double ldexp(double x, int exp);
+
+/*@
+ assigns \result \from x, exp;
+ */
extern float ldexpf(float x, int exp);
+
+/*@
+ assigns \result \from x, exp;
+ */
extern long double ldexpl(long double x, int exp);
/*@
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 7b609dc39a328eb5284ad2ae82207be1a2b7ec44..1e9a8265515c3aa92a47492e6880ea0f79d3e966 100644
--- a/src/plugins/report/tests/report/oracle/csv.csv
+++ b/src/plugins/report/tests/report/oracle/csv.csv
@@ -1,5 +1,5 @@
directory file line function property kind status property
-FRAMAC_SHARE/libc math.h 1032 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc math.h 1060 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
tests/report csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x
tests/report csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647
tests/report csv.c 12 main1 index_bound Unknown 0 ≤ x
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 236b5f91450558595cd5c4d24239700a18dbe80a..485554170a27d7145d18855fe7261023f0939334 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2961,6 +2961,108 @@
behavior underflow
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'frexp'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 658)
+ assigns \result, *exp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 658)
+ assigns \result \from value;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 658)
+ assigns *exp \from value;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'frexpf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 665)
+ assigns \result, *exp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 665)
+ assigns \result \from value;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 665)
+ assigns *exp \from value;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'frexpl'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 672)
+ assigns \result, *exp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 672)
+ assigns \result \from value;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 672)
+ assigns *exp \from value;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ldexp'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 682)
+ assigns \result \from x, exp;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ldexpf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 687)
+ assigns \result \from x, exp;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ldexpl'
+--------------------------------------------------------------------------------
+
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 692)
+ assigns \result \from x, exp;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'log'
--------------------------------------------------------------------------------
@@ -2974,7 +3076,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 673)
+[ Extern ] Froms (file share/libc/math.h, line 701)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2994,7 +3096,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 704)
+[ Extern ] Froms (file share/libc/math.h, line 732)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3014,7 +3116,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 735)
+[ Extern ] Froms (file share/libc/math.h, line 763)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3034,7 +3136,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 766)
+[ Extern ] Froms (file share/libc/math.h, line 794)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3054,7 +3156,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 797)
+[ Extern ] Froms (file share/libc/math.h, line 825)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3074,7 +3176,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 828)
+[ Extern ] Froms (file share/libc/math.h, line 856)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3094,7 +3196,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 863)
+[ Extern ] Froms (file share/libc/math.h, line 891)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3114,7 +3216,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 894)
+[ Extern ] Froms (file share/libc/math.h, line 922)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3134,7 +3236,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 925)
+[ Extern ] Froms (file share/libc/math.h, line 953)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3159,7 +3261,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 972)
+[ Extern ] Froms (file share/libc/math.h, line 1000)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3184,7 +3286,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 990)
+[ Extern ] Froms (file share/libc/math.h, line 1018)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3209,7 +3311,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1008)
+[ Extern ] Froms (file share/libc/math.h, line 1036)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3227,13 +3329,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 1030)
+[ Extern ] Assigns (file share/libc/math.h, line 1058)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1030)
+[ Extern ] Froms (file share/libc/math.h, line 1058)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1030)
+[ Extern ] Froms (file share/libc/math.h, line 1058)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3251,13 +3353,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 1045)
+[ Extern ] Assigns (file share/libc/math.h, line 1073)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1045)
+[ Extern ] Froms (file share/libc/math.h, line 1073)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1045)
+[ Extern ] Froms (file share/libc/math.h, line 1073)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3289,7 +3391,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1066)
+[ Extern ] Froms (file share/libc/math.h, line 1094)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3315,7 +3417,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1095)
+[ Extern ] Froms (file share/libc/math.h, line 1123)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3338,7 +3440,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1124)
+[ Extern ] Froms (file share/libc/math.h, line 1152)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3355,7 +3457,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1164)
+[ Extern ] Froms (file share/libc/math.h, line 1192)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3372,7 +3474,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1181)
+[ Extern ] Froms (file share/libc/math.h, line 1209)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3389,7 +3491,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1198)
+[ Extern ] Froms (file share/libc/math.h, line 1226)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3406,7 +3508,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1215)
+[ Extern ] Froms (file share/libc/math.h, line 1243)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3423,7 +3525,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1232)
+[ Extern ] Froms (file share/libc/math.h, line 1260)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3440,7 +3542,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1249)
+[ Extern ] Froms (file share/libc/math.h, line 1277)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3457,7 +3559,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1282)
+[ Extern ] Froms (file share/libc/math.h, line 1310)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3474,7 +3576,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1299)
+[ Extern ] Froms (file share/libc/math.h, line 1327)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3491,7 +3593,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1316)
+[ Extern ] Froms (file share/libc/math.h, line 1344)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3508,7 +3610,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1341)
+[ Extern ] Froms (file share/libc/math.h, line 1369)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3525,7 +3627,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1358)
+[ Extern ] Froms (file share/libc/math.h, line 1386)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3542,7 +3644,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1375)
+[ Extern ] Froms (file share/libc/math.h, line 1403)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3562,7 +3664,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1395)
+[ Extern ] Froms (file share/libc/math.h, line 1423)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3582,7 +3684,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1416)
+[ Extern ] Froms (file share/libc/math.h, line 1444)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3599,7 +3701,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1449)
+[ Extern ] Froms (file share/libc/math.h, line 1477)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3616,7 +3718,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1456)
+[ Extern ] Froms (file share/libc/math.h, line 1484)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3633,7 +3735,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1463)
+[ Extern ] Froms (file share/libc/math.h, line 1491)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3653,7 +3755,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1493)
+[ Extern ] Froms (file share/libc/math.h, line 1521)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3679,7 +3781,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1506)
+[ Extern ] Froms (file share/libc/math.h, line 1534)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3702,7 +3804,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1533)
+[ Extern ] Froms (file share/libc/math.h, line 1561)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3719,7 +3821,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1539)
+[ Extern ] Froms (file share/libc/math.h, line 1567)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4081,9 +4183,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 173 Completely validated
+ 179 Completely validated
16 Locally validated
- 488 Considered valid
+ 506 Considered valid
56 To be validated
- 733 Total
+ 757 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/math_h.c b/tests/libc/math_h.c
index b88b61298587fe81bc0644190254c9237d4625d7..fce13dd4be3afe37ab6e4e42fcc670d77a16251f 100644
--- a/tests/libc/math_h.c
+++ b/tests/libc/math_h.c
@@ -28,26 +28,28 @@ const long double huge_vall = HUGE_VALL;
const float infinity = INFINITY;
const double fp_ilogb0 = FP_ILOGB0;
const double fp_ilogbnan = FP_ILOGBNAN;
+volatile int int_top;
-#define TEST_VAL(type,f,c) type f##_##c = f(c)
-#define TEST_FUN(type,f,prefix) \
- TEST_VAL(type,f,prefix##pi); \
- TEST_VAL(type,f,prefix##half_pi); \
- TEST_VAL(type,f,prefix##e); \
- TEST_VAL(type,f,zero); \
- TEST_VAL(type,f,minus_zero); \
- TEST_VAL(type,f,one); \
- TEST_VAL(type,f,minus_one); \
- TEST_VAL(type,f,large); \
- TEST_VAL(type,f,prefix##top)
+#define TEST_VAL_CONST(type,f,cst) type f##_##cst = f(cst)
+#define TEST_FUN_CONSTS(type,f,prefix) \
+ TEST_VAL_CONST(type,f,prefix##pi); \
+ TEST_VAL_CONST(type,f,prefix##half_pi); \
+ TEST_VAL_CONST(type,f,prefix##e); \
+ TEST_VAL_CONST(type,f,zero); \
+ TEST_VAL_CONST(type,f,minus_zero); \
+ TEST_VAL_CONST(type,f,one); \
+ TEST_VAL_CONST(type,f,minus_one); \
+ TEST_VAL_CONST(type,f,large); \
+ TEST_VAL_CONST(type,f,prefix##top)
+void test_simple_specs(void);
int main() {
- TEST_FUN(double,atan,);
- TEST_FUN(float,atanf,f_);
- TEST_FUN(long double,atanl,ld_);
- TEST_FUN(double,fabs,);
- TEST_FUN(float,fabsf,f_);
- TEST_FUN(long double,fabsl,ld_);
+ TEST_FUN_CONSTS(double,atan,);
+ TEST_FUN_CONSTS(float,atanf,f_);
+ TEST_FUN_CONSTS(long double,atanl,ld_);
+ TEST_FUN_CONSTS(double,fabs,);
+ TEST_FUN_CONSTS(float,fabsf,f_);
+ TEST_FUN_CONSTS(long double,fabsl,ld_);
#ifdef NONFINITE
int r;
@@ -64,4 +66,20 @@ int main() {
r = isfinite(NAN);
//@ assert !r;
#endif
+
+ test_simple_specs();
+}
+
+#define TEST_VAL_VAR(type,fn,...) type res_##fn = fn(__VA_ARGS__)
+
+#define TEST_FUN_VAR(fn,...) \
+ TEST_VAL_VAR(double,fn,__VA_ARGS__); \
+ TEST_VAL_VAR(float,fn##f,__VA_ARGS__); \
+ TEST_VAL_VAR(long double,fn##l,__VA_ARGS__);
+
+void test_simple_specs() {
+ int exponent;
+ TEST_FUN_VAR(frexp, ld_top, &exponent);
+ TEST_FUN_VAR(ldexp, ld_top, int_top);
+ //@ assert \initialized(&exponent);
}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e52007ddeeca10602d81f5e6517071ed5aa43d5f..85f41d33f45af8ea4c374d85454a046c7a92f5ab 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -41,7 +41,7 @@
wcscpy (0 call); wcsdup (0 call); wcslen (3 calls); wcsncat (0 call);
wcsncpy (0 call); wmemcpy (1 call); wmemset (0 call);
- Specified-only functions (416)
+ Specified-only functions (422)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -95,8 +95,9 @@
flockfile (0 call); floor (0 call); floorf (0 call); floorl (0 call);
fmod (0 call); fmodf (0 call); fopen (0 call); fork (0 call);
fputc (0 call); fputs (0 call); fread (0 call); free (1 call);
- freeaddrinfo (0 call); freopen (0 call); fseek (0 call); fseeko (0 call);
- fsetpos (0 call); ftell (0 call); ftello (0 call); ftrylockfile (0 call);
+ freeaddrinfo (0 call); freopen (0 call); frexp (0 call); frexpf (0 call);
+ frexpl (0 call); fseek (0 call); fseeko (0 call); fsetpos (0 call);
+ ftell (0 call); ftello (0 call); ftrylockfile (0 call);
funlockfile (0 call); fwrite (0 call); gai_strerror (0 call); getc (0 call);
getc_unlocked (0 call); getchar (0 call); getchar_unlocked (0 call);
getcwd (0 call); getegid (0 call); geteuid (0 call); getgid (0 call);
@@ -111,18 +112,19 @@
iconv_open (0 call); inet_addr (2 calls); inet_ntoa (0 call);
inet_ntop (0 call); inet_pton (0 call); isascii (0 call); isatty (0 call);
jrand48 (0 call); kill (0 call); killpg (0 call); labs (0 call);
- lcong48 (0 call); ldiv (0 call); listen (0 call); llabs (0 call);
- lldiv (0 call); localtime (0 call); log (0 call); log10 (0 call);
- log10f (0 call); log10l (0 call); log2 (0 call); log2f (0 call);
- log2l (0 call); logf (0 call); logl (0 call); longjmp (0 call);
- lrand48 (0 call); lseek (0 call); lstat (0 call); makedev (0 call);
- malloc (10 calls); mblen (0 call); mbstowcs (0 call); mbtowc (0 call);
- mkdir (0 call); mkfifo (0 call); mknod (0 call); mkstemp (0 call);
- mktime (0 call); mrand48 (0 call); nan (0 call); nanf (0 call);
- nanl (0 call); nanosleep (0 call); nrand48 (0 call); ntohl (0 call);
- ntohs (0 call); open (0 call); openat (0 call); opendir (0 call);
- openlog (0 call); pathconf (0 call); pclose (0 call); perror (0 call);
- pipe (0 call); poll (0 call); popen (0 call); pow (0 call); powf (0 call);
+ lcong48 (0 call); ldexp (0 call); ldexpf (0 call); ldexpl (0 call);
+ ldiv (0 call); listen (0 call); llabs (0 call); lldiv (0 call);
+ localtime (0 call); log (0 call); log10 (0 call); log10f (0 call);
+ log10l (0 call); log2 (0 call); log2f (0 call); log2l (0 call);
+ logf (0 call); logl (0 call); longjmp (0 call); lrand48 (0 call);
+ lseek (0 call); lstat (0 call); makedev (0 call); malloc (10 calls);
+ mblen (0 call); mbstowcs (0 call); mbtowc (0 call); mkdir (0 call);
+ mkfifo (0 call); mknod (0 call); mkstemp (0 call); mktime (0 call);
+ mrand48 (0 call); nan (0 call); nanf (0 call); nanl (0 call);
+ nanosleep (0 call); nrand48 (0 call); ntohl (0 call); ntohs (0 call);
+ open (0 call); openat (0 call); opendir (0 call); openlog (0 call);
+ pathconf (0 call); pclose (0 call); perror (0 call); pipe (0 call);
+ poll (0 call); popen (0 call); pow (0 call); powf (0 call);
pthread_cond_broadcast (0 call); pthread_cond_destroy (0 call);
pthread_cond_init (0 call); pthread_cond_wait (0 call);
pthread_create (0 call); pthread_join (0 call);
@@ -194,7 +196,7 @@
Goto = 99
Assignment = 466
Exit point = 84
- Function = 501
+ Function = 507
Function call = 98
Pointer dereferencing = 161
Cyclomatic complexity = 299
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6c0be414fd6dc9145f3e6106aa51a3ac0c2448ea..3e8d34f0021861d4ed8e5a9295f46be82cc56d47 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3081,6 +3081,42 @@ extern double exp(double x);
*/
extern float expf(float x);
+/*@ requires valid_exp: \valid(exp);
+ ensures initialization: exp: \initialized(\old(exp));
+ assigns \result, *exp;
+ assigns \result \from value;
+ assigns *exp \from value;
+ */
+extern double frexp(double value, int *exp);
+
+/*@ requires valid_exp: \valid(exp);
+ ensures initialization: exp: \initialized(\old(exp));
+ assigns \result, *exp;
+ assigns \result \from value;
+ assigns *exp \from value;
+ */
+extern float frexpf(float value, int *exp);
+
+/*@ requires valid_exp: \valid(exp);
+ ensures initialization: exp: \initialized(\old(exp));
+ assigns \result, *exp;
+ assigns \result \from value;
+ assigns *exp \from value;
+ */
+extern long double frexpl(long double value, int *exp);
+
+/*@ assigns \result;
+ assigns \result \from x, exp; */
+extern double ldexp(double x, int exp);
+
+/*@ assigns \result;
+ assigns \result \from x, exp; */
+extern float ldexpf(float x, int exp);
+
+/*@ assigns \result;
+ assigns \result \from x, exp; */
+extern long double ldexpl(long double x, int exp);
+
/*@ requires finite_arg: \is_finite(x);
requires arg_positive: x > 0;
ensures finite_result: \is_finite(\result);
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
index 3f3ed25684677cafeb46616a83e637e1f039b2d2..0ad6df6695db04c25b6e97b2df5bec2f90317567 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -29,255 +29,299 @@
infinity ∈ {inf}
fp_ilogb0 ∈ {-2147483648.}
fp_ilogbnan ∈ {-2147483648.}
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:45: Call to builtin atan
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
-[eva] tests/libc/math_h.c:46: Call to builtin atanf
+ int_top ∈ [--..--]
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:47: Call to builtin atan
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
+[eva] tests/libc/math_h.c:48: Call to builtin atanf
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] using specification for function atanl
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function atanl <- main.
- Called from tests/libc/math_h.c:47.
+ Called from tests/libc/math_h.c:49.
[eva] Done for function atanl
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] using specification for function fabs
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabs <- main.
- Called from tests/libc/math_h.c:48.
+ Called from tests/libc/math_h.c:50.
[eva] Done for function fabs
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] using specification for function fabsf
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsf <- main.
- Called from tests/libc/math_h.c:49.
+ Called from tests/libc/math_h.c:51.
[eva] Done for function fabsf
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] using specification for function fabsl
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function fabsl <- main.
- Called from tests/libc/math_h.c:50.
+ Called from tests/libc/math_h.c:52.
[eva] Done for function fabsl
[eva] computing for function __finite <- main.
- Called from tests/libc/math_h.c:54.
+ Called from tests/libc/math_h.c:56.
[eva] using specification for function __finite
[eva] Done for function __finite
-[eva] tests/libc/math_h.c:55: assertion got status valid.
+[eva] tests/libc/math_h.c:57: assertion got status valid.
[eva] computing for function __finite <- main.
- Called from tests/libc/math_h.c:56.
+ Called from tests/libc/math_h.c:58.
[eva] Done for function __finite
[eva] computing for function __finite <- main.
- Called from tests/libc/math_h.c:56.
+ Called from tests/libc/math_h.c:58.
[eva] Done for function __finite
-[eva] tests/libc/math_h.c:57: assertion got status valid.
+[eva] tests/libc/math_h.c:59: assertion got status valid.
[eva] computing for function __finitef <- main.
- Called from tests/libc/math_h.c:58.
+ Called from tests/libc/math_h.c:60.
[eva] using specification for function __finitef
[eva] Done for function __finitef
[eva] computing for function __finitef <- main.
- Called from tests/libc/math_h.c:58.
+ Called from tests/libc/math_h.c:60.
[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:59: assertion got status valid.
+[eva] tests/libc/math_h.c:61: assertion got status valid.
[eva] computing for function __finite <- main.
- Called from tests/libc/math_h.c:60.
+ Called from tests/libc/math_h.c:62.
[eva] Done for function __finite
[eva] computing for function __finite <- main.
- Called from tests/libc/math_h.c:60.
-[eva] Done for function __finite
-[eva] tests/libc/math_h.c:61: assertion got status valid.
-[eva] computing for function __finitef <- main.
Called from tests/libc/math_h.c:62.
-[eva] Done for function __finitef
+[eva] Done for function __finite
[eva] tests/libc/math_h.c:63: assertion got status valid.
[eva] computing for function __finitef <- main.
Called from tests/libc/math_h.c:64.
[eva] Done for function __finitef
[eva] tests/libc/math_h.c:65: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:66.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:67: assertion got status valid.
+[eva] computing for function test_simple_specs <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] computing for function frexp <- test_simple_specs <- main.
+ Called from tests/libc/math_h.c:82.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:82:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- test_simple_specs <- main.
+ Called from tests/libc/math_h.c:82.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:82:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpl <- test_simple_specs <- main.
+ Called from tests/libc/math_h.c:82.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:82:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function ldexp <- test_simple_specs <- main.
+ Called from tests/libc/math_h.c:83.
+[eva] using specification for function ldexp
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- test_simple_specs <- main.
+ Called from tests/libc/math_h.c:83.
+[eva] using specification for function ldexpf
+[eva] Done for function ldexpf
+[eva] computing for function ldexpl <- test_simple_specs <- main.
+ Called from tests/libc/math_h.c:83.
+[eva] using specification for function ldexpl
+[eva] Done for function ldexpl
+[eva] tests/libc/math_h.c:84: assertion got status valid.
+[eva] Recording results for test_simple_specs
+[eva] Done for function test_simple_specs
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function test_simple_specs:
+ exponent ∈ [--..--]
+ res_frexp ∈ [-inf .. inf] ∪ {NaN}
+ res_frexpf ∈ [-inf .. inf] ∪ {NaN}
+ res_frexpl ∈ [-inf .. inf] ∪ {NaN}
+ res_ldexp ∈ [-inf .. inf] ∪ {NaN}
+ res_ldexpf ∈ [-inf .. inf] ∪ {NaN}
+ res_ldexpl ∈ [-inf .. inf] ∪ {NaN}
[eva:final-states] Values at end of function main:
atan_pi ∈ {1.26262725568}
atan_half_pi ∈ {1.00388482185}