diff --git a/share/libc/math.h b/share/libc/math.h
index 25c122cd2ed7a047e97c86c3be4566de0ba72acb..9aa74f2eb4796faba61253669b7d567493a19041 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -653,16 +653,131 @@ extern double expm1(double x);
extern float expm1f(float x);
extern long double expm1l(long double x);
-extern double frexp(double value, int *exp);
-extern float frexpf(float value, int *exp);
-extern long double frexpl(long double value, int *exp);
+/*@
+ requires valid_exp: \valid(exp);
+ assigns \result, *exp \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_nonzero: x != 0.0;
+ ensures finite_result: \is_finite(\result);
+ ensures bounded_result: 0.5 <= \result < 1.0;
+ ensures initialization:exp: \initialized(exp);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x) || \is_minus_infinity(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures result_same_infinite: \result == x;
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures zero_result: \result == 0.0;
+ ensures initialization:exp: \initialized(exp);
+ ensures zero_exp: *exp == 0;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
+extern double frexp(double x, int *exp);
+
+/*@
+ requires valid_exp: \valid(exp);
+ assigns \result, *exp \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_nonzero: x != 0.0;
+ ensures finite_result: \is_finite(\result);
+ ensures bounded_result: 0.5 <= \result < 1.0;
+ ensures initialization:exp: \initialized(exp);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x) || \is_minus_infinity(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures result_same_infinite: \result == x;
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures zero_result: \result == x;
+ ensures initialization:exp: \initialized(exp);
+ ensures zero_exp: *exp == 0;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
+extern float frexpf(float x, int *exp);
+
+/*@
+ requires valid_exp: \valid(exp);
+ assigns \result, *exp \from x;
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_nonzero: x != 0.0;
+ ensures finite_result: \is_finite(\result);
+ ensures bounded_result: 0.5 <= \result < 1.0;
+ ensures initialization:exp: \initialized(exp);
+ behavior infinite:
+ assumes infinite_arg: \is_plus_infinity(x) || \is_minus_infinity(x);
+ ensures infinite_result: \is_infinite(\result);
+ ensures result_same_infinite: \result == x;
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures zero_result: \result == x;
+ ensures initialization:exp: \initialized(exp);
+ ensures zero_exp: *exp == 0;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
+extern long double frexpl(long double x, int *exp);
extern int ilogb(double x);
extern int ilogbf(float x);
extern int ilogbl(long double x);
+/*@
+ assigns errno, \result \from x, exp;
+ behavior normal:
+ assumes finite_logic_res: \is_finite((double)(x * pow(2.0d, (double)exp)));
+ ensures finite_result: \is_finite(\result);
+ ensures errno: errno == ERANGE || errno == \old(errno); //ERANGE if underflow
+ behavior overflow_not_nan:
+ assumes not_nan_arg: !\is_NaN(x);
+ assumes infinite_logic_res: !\is_finite((double)(x * pow(2.0d, (double)exp)));
+ ensures infinite_result: \is_infinite(\result);
+ ensures errno: errno == ERANGE || errno == \old(errno);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
extern double ldexp(double x, int exp);
+
+/*@
+ assigns errno, \result \from x, exp;
+ behavior normal:
+ assumes finite_logic_res: \is_finite((float)(x * pow(2.0f, (float)exp)));
+ ensures finite_result: \is_finite(\result);
+ ensures errno: errno == ERANGE || errno == \old(errno); //ERANGE if underflow
+ behavior overflow_not_nan:
+ assumes not_nan_arg: !\is_NaN(x);
+ assumes infinite_logic_res: !\is_finite((float)(x * pow(2.0f, (float)exp)));
+ ensures infinite_result: \is_infinite(\result);
+ ensures errno: errno == ERANGE || errno == \old(errno);
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ complete behaviors;
+ disjoint behaviors;
+*/
extern float ldexpf(float x, int 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..3dbfbfd16ccfb3a21384371ad0801258278b0a90 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 1147 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..c03bc0130e505d8cf9b19639ed38eb75b901253e 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2961,6 +2961,186 @@
behavior underflow
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'frexp'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition for 'normal' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'normal' 'bounded_result'
+ ensures bounded_result: 0.5 ≤ \result < 1.0
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'normal' 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'zero_result'
+ ensures zero_result: \result ≡ 0.0
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'zero_exp'
+ ensures zero_exp: *\old(exp) ≡ 0
+ 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 x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 658)
+ assigns *exp \from x;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Valid ] Behavior 'normal'
+ behavior normal
+ by Frama-C kernel.
+[ Valid ] Behavior 'zero'
+ behavior zero
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'frexpf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition for 'normal' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'normal' 'bounded_result'
+ ensures bounded_result: 0.5 ≤ \result < 1.0
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'normal' 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'zero_result'
+ ensures zero_result: \result ≡ \old(x)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'zero_exp'
+ ensures zero_exp: *\old(exp) ≡ 0
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 685)
+ assigns \result, *exp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 685)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 685)
+ assigns *exp \from x;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Valid ] Behavior 'normal'
+ behavior normal
+ by Frama-C kernel.
+[ Valid ] Behavior 'zero'
+ behavior zero
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'frexpl'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition for 'normal' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'normal' 'bounded_result'
+ ensures bounded_result: 0.5 ≤ \result < 1.0
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'normal' 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'zero_result'
+ ensures zero_result: \result ≡ \old(x)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'initialization,exp'
+ ensures initialization: exp: \initialized(\old(exp))
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'zero_exp'
+ ensures zero_exp: *\old(exp) ≡ 0
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 712)
+ assigns \result, *exp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 712)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 712)
+ assigns *exp \from x;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Valid ] Behavior 'normal'
+ behavior normal
+ by Frama-C kernel.
+[ Valid ] Behavior 'zero'
+ behavior zero
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ldexp'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition '__fc_errno'
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 742)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 742)
+ assigns __fc_errno \from x, exp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 742)
+ assigns \result \from x, exp;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'ldexpf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition '__fc_errno'
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 762)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 762)
+ assigns __fc_errno \from x, exp;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 762)
+ assigns \result \from x, exp;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'log'
--------------------------------------------------------------------------------
@@ -2974,7 +3154,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 788)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2994,7 +3174,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 819)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3014,7 +3194,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 850)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3034,7 +3214,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 881)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3054,7 +3234,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 912)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3074,7 +3254,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 943)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3094,7 +3274,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 978)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3114,7 +3294,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 1009)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3134,7 +3314,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 1040)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3159,7 +3339,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 1087)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3184,7 +3364,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 1105)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3209,7 +3389,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 1123)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3227,13 +3407,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 1145)
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 1145)
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 1145)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3251,13 +3431,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 1160)
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 1160)
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 1160)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3289,7 +3469,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 1181)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3315,7 +3495,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 1210)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3338,7 +3518,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 1239)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3355,7 +3535,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 1279)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3372,7 +3552,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 1296)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3389,7 +3569,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 1313)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3406,7 +3586,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 1330)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3423,7 +3603,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 1347)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3440,7 +3620,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 1364)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3457,7 +3637,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 1397)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3474,7 +3654,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 1414)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3491,7 +3671,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 1431)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3508,7 +3688,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 1456)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3525,7 +3705,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 1473)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3542,7 +3722,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 1490)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3562,7 +3742,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 1510)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3582,7 +3762,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 1531)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3599,7 +3779,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 1564)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3616,7 +3796,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 1571)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3633,7 +3813,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 1578)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3653,7 +3833,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 1608)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3679,7 +3859,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 1621)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3702,7 +3882,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 1648)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3719,7 +3899,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 1654)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4081,9 +4261,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 173 Completely validated
+ 184 Completely validated
16 Locally validated
- 488 Considered valid
+ 528 Considered valid
56 To be validated
- 733 Total
+ 784 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/math_h.c b/tests/libc/math_h.c
index b88b61298587fe81bc0644190254c9237d4625d7..1c8cc1b985d07963b8277e5bc7b39d8183305c7d 100644
--- a/tests/libc/math_h.c
+++ b/tests/libc/math_h.c
@@ -24,30 +24,62 @@ const double large = 1e38;
const double huge_val = HUGE_VAL;
const float huge_valf = HUGE_VALF;
const long double huge_vall = HUGE_VALL;
-#endif
const float infinity = INFINITY;
+#endif
const double fp_ilogb0 = FP_ILOGB0;
const double fp_ilogbnan = FP_ILOGBNAN;
+volatile int int_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)
-#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)
+// tests functions with 2 arguments, where the first one changes,
+// but the second one is fixed by the caller.
+// suffix prevents redeclaring variables with the same name
+#define TEST_VAL2_FST_CONST(type,f,cst,snd_arg,suffix) type f##_##cst##suffix = f(cst,snd_arg)
+#define TEST_FUN2_FST_CONSTS(type,f,prefix,snd_arg,suffix) \
+ TEST_VAL2_FST_CONST(type,f,prefix##pi,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,prefix##half_pi,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,prefix##e,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,zero,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,minus_zero,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,one,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,minus_one,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,large,snd_arg,suffix); \
+ TEST_VAL2_FST_CONST(type,f,prefix##top,snd_arg,suffix)
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_);
+ int exponent;
+ TEST_FUN2_FST_CONSTS(double,frexp,,&exponent,);
+ TEST_FUN2_FST_CONSTS(float,frexpf,f_,&exponent,);
+ TEST_FUN2_FST_CONSTS(long double,frexpl,ld_,&exponent,);
+ TEST_FUN2_FST_CONSTS(double,ldexp,,10,);
+ TEST_FUN2_FST_CONSTS(float,ldexpf,f_,10,);
+ //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,10,);
+ TEST_FUN2_FST_CONSTS(double,ldexp,,0,_zero);
+ TEST_FUN2_FST_CONSTS(float,ldexpf,f_,0,_zero);
+ //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,0,_zero);
+ TEST_FUN2_FST_CONSTS(double,ldexp,,-5,_minus5);
+ TEST_FUN2_FST_CONSTS(float,ldexpf,f_,-5,_minus5);
+ //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,-5,_minus5);
+ TEST_FUN2_FST_CONSTS(double,ldexp,,100000,_huge);
+ TEST_FUN2_FST_CONSTS(float,ldexpf,f_,100000,_huge);
+ //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,100000,_huge);
#ifdef NONFINITE
int r;
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e52007ddeeca10602d81f5e6517071ed5aa43d5f..483efb112ac3b086e079422c67dff159473513fe 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 (421)
==============================
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,21 +112,21 @@
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);
- 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);
+ lcong48 (0 call); ldexp (0 call); ldexpf (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);
pthread_mutex_destroy (0 call); pthread_mutex_init (0 call);
pthread_mutex_lock (0 call); pthread_mutex_unlock (0 call);
pthread_mutexattr_destroy (0 call); pthread_mutexattr_init (0 call);
@@ -194,7 +195,7 @@
Goto = 99
Assignment = 466
Exit point = 84
- Function = 501
+ Function = 506
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..cc1ba0226d8f8f21f7e64a86f789fc99fa06b3c1 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3081,6 +3081,112 @@ extern double exp(double x);
*/
extern float expf(float x);
+/*@ requires valid_exp: \valid(exp);
+ requires
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
+ assigns \result, *exp;
+ assigns \result \from x;
+ assigns *exp \from x;
+
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_nonzero: x ≢ 0.0;
+ ensures finite_result: \is_finite(\result);
+ ensures bounded_result: 0.5 ≤ \result < 1.0;
+ ensures initialization: exp: \initialized(\old(exp));
+
+ behavior zero:
+ assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures zero_result: \result ≡ 0.0;
+ ensures initialization: exp: \initialized(\old(exp));
+ ensures zero_exp: *\old(exp) ≡ 0;
+
+ complete behaviors zero, normal;
+ disjoint behaviors zero, normal;
+ */
+extern double frexp(double x, int *exp);
+
+/*@ requires valid_exp: \valid(exp);
+ requires
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
+ assigns \result, *exp;
+ assigns \result \from x;
+ assigns *exp \from x;
+
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_nonzero: x ≢ 0.0;
+ ensures finite_result: \is_finite(\result);
+ ensures bounded_result: 0.5 ≤ \result < 1.0;
+ ensures initialization: exp: \initialized(\old(exp));
+
+ behavior zero:
+ assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures zero_result: \result ≡ \old(x);
+ ensures initialization: exp: \initialized(\old(exp));
+ ensures zero_exp: *\old(exp) ≡ 0;
+
+ complete behaviors zero, normal;
+ disjoint behaviors zero, normal;
+ */
+extern float frexpf(float x, int *exp);
+
+/*@ requires valid_exp: \valid(exp);
+ requires
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
+ assigns \result, *exp;
+ assigns \result \from x;
+ assigns *exp \from x;
+
+ behavior normal:
+ assumes finite_arg: \is_finite(x);
+ assumes arg_nonzero: x ≢ 0.0;
+ ensures finite_result: \is_finite(\result);
+ ensures bounded_result: 0.5 ≤ \result < 1.0;
+ ensures initialization: exp: \initialized(\old(exp));
+
+ behavior zero:
+ assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures zero_result: \result ≡ \old(x);
+ ensures initialization: exp: \initialized(\old(exp));
+ ensures zero_exp: *\old(exp) ≡ 0;
+
+ complete behaviors zero, normal;
+ disjoint behaviors zero, normal;
+ */
+extern long double frexpl(long double x, int *exp);
+
+/*@ requires
+ finite_logic_res:
+ \is_finite((double)(x * pow((double)2.0d, (double)exp)));
+ ensures finite_result: \is_finite(\result);
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno);
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from x, exp;
+ assigns \result \from x, exp;
+ */
+extern double ldexp(double x, int exp);
+
+/*@ requires
+ finite_logic_res:
+ \is_finite((float)(x *
+ pow((double)((float)2.0f), (double)((float)exp))));
+ ensures finite_result: \is_finite(\result);
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno);
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from x, exp;
+ assigns \result \from x, exp;
+ */
+extern float ldexpf(float 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..098f41b2d50485bb9e2598d9aba1d05d10190ce3 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -29,256 +29,722 @@
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:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:61: Call to builtin atan
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: Call to builtin atanf
+[eva] tests/libc/math_h.c:62: 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:63.
[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:63.
[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:63.
[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:63.
[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:63.
[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:63.
[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:63.
[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:63.
[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:63.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:64.
[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:65.
[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:65.
[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:65.
[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:65.
[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:65.
[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:65.
[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:65.
[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:65.
[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:65.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[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:66.
[eva] Done for function fabsl
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:68.
+[eva] tests/libc/math_h.c:68:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:69.
+[eva] tests/libc/math_h.c:69:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:70.
+[eva] tests/libc/math_h.c:70:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] using specification for function ldexp
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:71.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] using specification for function ldexpf
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:72.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:74.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:75.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:77.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:78.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:80.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:81.
+[eva] Done for function ldexpf
[eva] computing for function __finite <- main.
- Called from tests/libc/math_h.c:54.
+ Called from tests/libc/math_h.c:86.
[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:87: 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:88.
[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:88.
[eva] Done for function __finite
-[eva] tests/libc/math_h.c:57: assertion got status valid.
+[eva] tests/libc/math_h.c:89: 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:90.
[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:90.
[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:59: assertion got status valid.
+[eva] tests/libc/math_h.c:91: 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:92.
[eva] Done for function __finite
[eva] computing for function __finite <- main.
- Called from tests/libc/math_h.c:60.
+ Called from tests/libc/math_h.c:92.
[eva] Done for function __finite
-[eva] tests/libc/math_h.c:61: assertion got status valid.
+[eva] tests/libc/math_h.c:93: assertion got status valid.
[eva] computing for function __finitef <- main.
- Called from tests/libc/math_h.c:62.
+ Called from tests/libc/math_h.c:94.
[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:63: assertion got status valid.
+[eva] tests/libc/math_h.c:95: assertion got status valid.
[eva] computing for function __finitef <- main.
- Called from tests/libc/math_h.c:64.
+ Called from tests/libc/math_h.c:96.
[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:65: assertion got status valid.
+[eva] tests/libc/math_h.c:97: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
atan_pi ∈ {1.26262725568}
atan_half_pi ∈ {1.00388482185}
atan_e ∈ {1.21828290502}
@@ -333,5 +799,105 @@
fabsl_minus_one ∈ [-inf .. inf]
fabsl_large ∈ [-inf .. inf]
fabsl_ld_top ∈ [-inf .. inf] ∪ {NaN}
+ exponent ∈ [--..--]
+ frexp_pi ∈ [0.5 .. 1.]
+ frexp_half_pi ∈ [0.5 .. 1.]
+ frexp_e ∈ [0.5 .. 1.]
+ frexp_zero ∈ [-0. .. 0.]
+ frexp_minus_zero ∈ [-0. .. 0.]
+ frexp_one ∈ [0.5 .. 1.]
+ frexp_minus_one ∈ [0.5 .. 1.]
+ frexp_large ∈ [0.5 .. 1.]
+ frexp_top ∈ [-inf .. inf] ∪ {NaN}
+ frexpf_f_pi ∈ [0.5 .. 0.999999940395]
+ frexpf_f_half_pi ∈ [0.5 .. 0.999999940395]
+ frexpf_f_e ∈ [0.5 .. 0.999999940395]
+ frexpf_zero ∈ [-0. .. 0.]
+ frexpf_minus_zero ∈ [-0. .. 0.]
+ frexpf_one ∈ [0.5 .. 0.999999940395]
+ frexpf_minus_one ∈ [0.5 .. 0.999999940395]
+ frexpf_large ∈ [0.5 .. 0.999999940395]
+ frexpf_f_top ∈ [-inf .. inf] ∪ {NaN}
+ frexpl_ld_pi ∈ [-inf .. inf]
+ frexpl_ld_half_pi ∈ [-inf .. inf]
+ frexpl_ld_e ∈ [-inf .. inf]
+ frexpl_zero ∈ [-inf .. inf]
+ frexpl_minus_zero ∈ [-inf .. inf]
+ frexpl_one ∈ [-inf .. inf]
+ frexpl_minus_one ∈ [-inf .. inf]
+ frexpl_large ∈ [-inf .. inf]
+ frexpl_ld_top ∈ [-inf .. inf] ∪ {NaN}
+ ldexp_pi ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_half_pi ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_e ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_minus_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_one ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_minus_one ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_large ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_top ∈ [-inf .. inf] ∪ {NaN}
+ ldexpf_f_pi ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_half_pi ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_e ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_minus_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_one ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_minus_one ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_large ∈ [-inf .. inf]
+ ldexpf_f_top ∈ [-inf .. inf] ∪ {NaN}
+ ldexp_pi_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_half_pi_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_e_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_zero_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_minus_zero_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_one_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_minus_one_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_large_zero ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_top_zero ∈ [-inf .. inf] ∪ {NaN}
+ ldexpf_f_pi_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_half_pi_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_e_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_zero_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_minus_zero_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_one_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_minus_one_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_large_zero ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_top_zero ∈ [-inf .. inf] ∪ {NaN}
+ ldexp_pi_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_half_pi_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_e_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_zero_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_minus_zero_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_one_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_minus_one_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_large_minus5 ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
+ ldexp_top_minus5 ∈ [-inf .. inf] ∪ {NaN}
+ ldexpf_f_pi_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_half_pi_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_e_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_zero_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_minus_zero_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_one_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_minus_one_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_large_minus5 ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ ldexpf_f_top_minus5 ∈ [-inf .. inf] ∪ {NaN}
+ ldexp_pi_huge ∈ [-inf .. inf]
+ ldexp_half_pi_huge ∈ [-inf .. inf]
+ ldexp_e_huge ∈ [-inf .. inf]
+ ldexp_zero_huge ∈ [-inf .. inf]
+ ldexp_minus_zero_huge ∈ [-inf .. inf]
+ ldexp_one_huge ∈ [-inf .. inf]
+ ldexp_minus_one_huge ∈ [-inf .. inf]
+ ldexp_large_huge ∈ [-inf .. inf]
+ ldexp_top_huge ∈ [-inf .. inf] ∪ {NaN}
+ ldexpf_f_pi_huge ∈ [-inf .. inf]
+ ldexpf_f_half_pi_huge ∈ [-inf .. inf]
+ ldexpf_f_e_huge ∈ [-inf .. inf]
+ ldexpf_zero_huge ∈ [-inf .. inf]
+ ldexpf_minus_zero_huge ∈ [-inf .. inf]
+ ldexpf_one_huge ∈ [-inf .. inf]
+ ldexpf_minus_one_huge ∈ [-inf .. inf]
+ ldexpf_large_huge ∈ [-inf .. inf]
+ ldexpf_f_top_huge ∈ [-inf .. inf] ∪ {NaN}
r ∈ {0}
__retres ∈ {0}