From cfe4beff89242aa20a6b44a131d32314c5995e31 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 3 Mar 2021 09:38:49 +0100
Subject: [PATCH] [Libc] fix and improve specification for frexp* and ldexp*
Due to the absence of a long double version of the pow() logic function,
and due to likely little demand for ldexpl, this function has not been
specified.
---
share/libc/math.h | 125 ++-
.../report/tests/report/oracle/csv.csv | 2 +-
tests/idct/oracle/ieee_1180_1990.res.oracle | 234 +++--
tests/libc/math_h.c | 50 +-
tests/libc/oracle/fc_libc.0.res.oracle | 35 +-
tests/libc/oracle/fc_libc.1.res.oracle | 110 ++-
tests/libc/oracle/math_h.res.oracle | 800 +++++++++++++++---
7 files changed, 1063 insertions(+), 293 deletions(-)
diff --git a/share/libc/math.h b/share/libc/math.h
index 0a8d71de4ce..9aa74f2eb47 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -655,42 +655,129 @@ 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);
+ 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 value;
- ensures initialization:exp:\initialized(exp);
- */
-extern float frexpf(float value, int *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 value;
- ensures initialization:exp:\initialized(exp);
- */
-extern long double frexpl(long double value, int *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 \result \from x, exp;
- */
+ 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 \result \from x, 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);
-/*@
- 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 1e9a8265515..3dbfbfd16cc 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 1060 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 485554170a2..c03bc0130e5 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2965,70 +2965,152 @@
--- Properties of Function 'frexp'
--------------------------------------------------------------------------------
-[ Extern ] Post-condition 'initialization,exp'
+[ 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 value;
+ assigns \result \from x;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 658)
- assigns *exp \from value;
+ 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 'initialization,exp'
+[ 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 ] Assigns (file share/libc/math.h, line 665)
+[ 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 665)
- assigns \result \from value;
+[ 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 665)
- assigns *exp \from value;
+[ 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 'initialization,exp'
+[ 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 ] Assigns (file share/libc/math.h, line 672)
+[ 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 672)
- assigns \result \from value;
+[ 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 672)
- assigns *exp \from value;
+[ 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 ] Assigns nothing
- assigns \nothing;
+[ 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 682)
+[ 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
@@ -3039,24 +3121,20 @@
--- Properties of Function 'ldexpf'
--------------------------------------------------------------------------------
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ Extern ] Post-condition 'finite_result'
+ ensures finite_result: \is_finite(\result)
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 687)
- assigns \result \from x, exp;
+[ Extern ] Post-condition '__fc_errno'
+ ensures
+ __fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Valid ] Default behavior
- default behavior
- by Frama-C kernel.
-
---------------------------------------------------------------------------------
---- Properties of Function 'ldexpl'
---------------------------------------------------------------------------------
-
-[ Extern ] Assigns nothing
- assigns \nothing;
+[ 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 692)
+[ Extern ] Froms (file share/libc/math.h, line 762)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3076,7 +3154,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 701)
+[ Extern ] Froms (file share/libc/math.h, line 788)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3096,7 +3174,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 732)
+[ Extern ] Froms (file share/libc/math.h, line 819)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3116,7 +3194,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 763)
+[ Extern ] Froms (file share/libc/math.h, line 850)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3136,7 +3214,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 794)
+[ Extern ] Froms (file share/libc/math.h, line 881)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3156,7 +3234,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 825)
+[ Extern ] Froms (file share/libc/math.h, line 912)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3176,7 +3254,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 856)
+[ Extern ] Froms (file share/libc/math.h, line 943)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3196,7 +3274,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 891)
+[ Extern ] Froms (file share/libc/math.h, line 978)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3216,7 +3294,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 922)
+[ Extern ] Froms (file share/libc/math.h, line 1009)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3236,7 +3314,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 953)
+[ Extern ] Froms (file share/libc/math.h, line 1040)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3261,7 +3339,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1000)
+[ Extern ] Froms (file share/libc/math.h, line 1087)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3286,7 +3364,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1018)
+[ Extern ] Froms (file share/libc/math.h, line 1105)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3311,7 +3389,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1036)
+[ Extern ] Froms (file share/libc/math.h, line 1123)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3329,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 1058)
+[ 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 1058)
+[ 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 1058)
+[ Extern ] Froms (file share/libc/math.h, line 1145)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3353,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 1073)
+[ 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 1073)
+[ 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 1073)
+[ Extern ] Froms (file share/libc/math.h, line 1160)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3391,7 +3469,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1094)
+[ Extern ] Froms (file share/libc/math.h, line 1181)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3417,7 +3495,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1123)
+[ Extern ] Froms (file share/libc/math.h, line 1210)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3440,7 +3518,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1152)
+[ Extern ] Froms (file share/libc/math.h, line 1239)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3457,7 +3535,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1192)
+[ Extern ] Froms (file share/libc/math.h, line 1279)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3474,7 +3552,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1209)
+[ Extern ] Froms (file share/libc/math.h, line 1296)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3491,7 +3569,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1226)
+[ Extern ] Froms (file share/libc/math.h, line 1313)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3508,7 +3586,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1243)
+[ Extern ] Froms (file share/libc/math.h, line 1330)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3525,7 +3603,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1260)
+[ Extern ] Froms (file share/libc/math.h, line 1347)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3542,7 +3620,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1277)
+[ Extern ] Froms (file share/libc/math.h, line 1364)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3559,7 +3637,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1310)
+[ Extern ] Froms (file share/libc/math.h, line 1397)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3576,7 +3654,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1327)
+[ Extern ] Froms (file share/libc/math.h, line 1414)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3593,7 +3671,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1344)
+[ Extern ] Froms (file share/libc/math.h, line 1431)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3610,7 +3688,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1369)
+[ Extern ] Froms (file share/libc/math.h, line 1456)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3627,7 +3705,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1386)
+[ Extern ] Froms (file share/libc/math.h, line 1473)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3644,7 +3722,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1403)
+[ Extern ] Froms (file share/libc/math.h, line 1490)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3664,7 +3742,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1423)
+[ Extern ] Froms (file share/libc/math.h, line 1510)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3684,7 +3762,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1444)
+[ Extern ] Froms (file share/libc/math.h, line 1531)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3701,7 +3779,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1477)
+[ Extern ] Froms (file share/libc/math.h, line 1564)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3718,7 +3796,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1484)
+[ Extern ] Froms (file share/libc/math.h, line 1571)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3735,7 +3813,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1491)
+[ Extern ] Froms (file share/libc/math.h, line 1578)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3755,7 +3833,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1521)
+[ Extern ] Froms (file share/libc/math.h, line 1608)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3781,7 +3859,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1534)
+[ Extern ] Froms (file share/libc/math.h, line 1621)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3804,7 +3882,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1561)
+[ Extern ] Froms (file share/libc/math.h, line 1648)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3821,7 +3899,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1567)
+[ Extern ] Froms (file share/libc/math.h, line 1654)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4183,9 +4261,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 179 Completely validated
+ 184 Completely validated
16 Locally validated
- 506 Considered valid
+ 528 Considered valid
56 To be validated
- 757 Total
+ 784 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/math_h.c b/tests/libc/math_h.c
index fce13dd4be3..1c8cc1b985d 100644
--- a/tests/libc/math_h.c
+++ b/tests/libc/math_h.c
@@ -24,8 +24,8 @@ 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;
@@ -42,7 +42,21 @@ volatile int int_top;
TEST_VAL_CONST(type,f,large); \
TEST_VAL_CONST(type,f,prefix##top)
-void test_simple_specs(void);
+// 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_CONSTS(double,atan,);
TEST_FUN_CONSTS(float,atanf,f_);
@@ -50,6 +64,22 @@ int main() {
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;
@@ -66,20 +96,4 @@ 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 85f41d33f45..483efb112ac 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 (422)
+ 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);
@@ -112,22 +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); 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);
+ 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);
@@ -196,7 +195,7 @@
Goto = 99
Assignment = 466
Exit point = 84
- Function = 507
+ 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 3e8d34f0021..cc1ba0226d8 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3082,41 +3082,111 @@ extern double exp(double x);
extern float expf(float x);
/*@ requires valid_exp: \valid(exp);
- ensures initialization: exp: \initialized(\old(exp));
+ requires
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
assigns \result, *exp;
- assigns \result \from value;
- assigns *exp \from value;
+ 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 value, int *exp);
+extern double frexp(double x, int *exp);
/*@ requires valid_exp: \valid(exp);
- ensures initialization: exp: \initialized(\old(exp));
+ requires
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
assigns \result, *exp;
- assigns \result \from value;
- assigns *exp \from value;
+ 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 value, int *exp);
+extern float frexpf(float x, int *exp);
/*@ requires valid_exp: \valid(exp);
- ensures initialization: exp: \initialized(\old(exp));
+ requires
+ ¬(infinite_arg: \is_plus_infinity(x) ∨ \is_minus_infinity(x));
+ requires ¬(nan_arg: \is_NaN(x));
assigns \result, *exp;
- assigns \result \from value;
- assigns *exp \from value;
+ 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 value, int *exp);
+extern long double frexpl(long double x, int *exp);
-/*@ assigns \result;
- assigns \result \from x, 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);
-/*@ assigns \result;
- assigns \result \from x, 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);
-/*@ 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 0ad6df6695d..098f41b2d50 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -30,299 +30,721 @@
fp_ilogb0 ∈ {-2147483648.}
fp_ilogbnan ∈ {-2147483648.}
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] 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:49.
+ 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:49.
+ 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:49.
+ 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:49.
+ 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:49.
+ 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:49.
+ 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:49.
+ 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:49.
+ 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:49.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:50.
+ 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:51.
+ 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:51.
+ 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:51.
+ 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:51.
+ 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:51.
+ 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:51.
+ 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:51.
+ 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:51.
+ 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:51.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:52.
+ 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:56.
+ 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:57: 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:58.
+ 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:58.
+ Called from tests/libc/math_h.c:88.
[eva] Done for function __finite
-[eva] tests/libc/math_h.c:59: 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:60.
+ 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:60.
+ Called from tests/libc/math_h.c:90.
[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:61: 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:62.
+ 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:62.
+ Called from tests/libc/math_h.c:92.
[eva] Done for function __finite
-[eva] tests/libc/math_h.c:63: 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:64.
+ Called from tests/libc/math_h.c:94.
[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:65: 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:66.
+ Called from tests/libc/math_h.c:96.
[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] 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 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:
+ __fc_errno ∈ [--..--]
atan_pi ∈ {1.26262725568}
atan_half_pi ∈ {1.00388482185}
atan_e ∈ {1.21828290502}
@@ -377,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}
--
GitLab