diff --git a/share/libc/math.h b/share/libc/math.h
index 9aa74f2eb4796faba61253669b7d567493a19041..c2d52a34583abaf8f755901ca0563625092cb106 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -467,8 +467,68 @@ extern float sinf(float x);
*/
extern long double sinl(long double x);
+/* Note: the specs of tan/tanf below assume that, for a finite x,
+ * the result is always finite. This is _not_ guaranteed by the standard,
+ * but testing with the GNU libc, plus some mathematical arguments
+ * (see https://stackoverflow.com/questions/67482420) indicate that,
+ * in practice, the result is _never_ infinite.
+ * If you know of any implementations in which a finite argument
+ * produces an infinite result, please inform us.
+ */
+/*@
+ assigns errno, \result \from x;
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ assigns \result \from x;
+ ensures zero_res: \is_finite(\result) && \result == x;
+ ensures no_error: errno == \old(errno);
+ behavior finite_non_zero:
+ assumes finite_arg: \is_finite(x) && x != 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures maybe_error: errno == \old(errno) || errno == ERANGE;
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
+*/
extern double tan(double x);
+
+/*@
+ assigns errno, \result \from x;
+ behavior zero:
+ assumes zero_arg: \is_finite(x) && x == 0.;
+ assigns \result \from x;
+ ensures zero_res: \is_finite(\result) && \result == x;
+ ensures no_error: errno == \old(errno);
+ behavior finite_non_zero:
+ assumes finite_arg: \is_finite(x) && x != 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures maybe_error: errno == \old(errno) || errno == ERANGE;
+ behavior infinity:
+ assumes infinite_arg: \is_infinite(x);
+ ensures nan_result: \is_NaN(\result);
+ ensures errno_set: errno == EDOM;
+ behavior nan:
+ assumes nan_arg: \is_NaN(x);
+ assigns \result \from x;
+ ensures nan_result: \is_NaN(\result);
+ ensures no_error: errno == \old(errno);
+ complete behaviors;
+ disjoint behaviors;
+*/
extern float tanf(float x);
+
+/*@
+ assigns errno, \result \from x;
+ ensures maybe_error: errno == \old(errno) || errno == EDOM || errno == ERANGE;
+*/
extern long double tanl(long double x);
/*@
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 3dbfbfd16ccfb3a21384371ad0801258278b0a90..e4dc4df6f00008cade09bda50ddf0b94122d3d92 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 1147 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc math.h 1207 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 2596ed249ede591884191af9e518229af9617054..eb9d1531fcfbd9c001b76a9946ccc398d95d516e 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2807,6 +2807,115 @@
default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function 'tan'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition for 'zero' 'zero_res'
+ ensures zero_res: \is_finite(\result) ∧ \result ≡ \old(x)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'finite_non_zero' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'finite_non_zero' 'maybe_error'
+ ensures
+ maybe_error:
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 479)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 479)
+ assigns __fc_errno \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 479)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'zero' (file share/libc/math.h, line 482)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Valid ] Behavior 'finite_non_zero'
+ behavior finite_non_zero
+ by Frama-C kernel.
+[ Valid ] Behavior 'zero'
+ behavior zero
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'tanf'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition for 'zero' 'zero_res'
+ ensures zero_res: \is_finite(\result) ∧ \result ≡ \old(x)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'zero' 'no_error'
+ ensures no_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'finite_non_zero' 'finite_result'
+ ensures finite_result: \is_finite(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'finite_non_zero' 'maybe_error'
+ ensures
+ maybe_error:
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 504)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 504)
+ assigns __fc_errno \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 504)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'zero' (file share/libc/math.h, line 507)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Valid ] Behavior 'finite_non_zero'
+ behavior finite_non_zero
+ by Frama-C kernel.
+[ Valid ] Behavior 'zero'
+ behavior zero
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function 'tanl'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition 'maybe_error'
+ ensures
+ maybe_error:
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 33 ∨
+ __fc_errno ≡ 34
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 529)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 529)
+ assigns __fc_errno \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 529)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function 'acosh'
--------------------------------------------------------------------------------
@@ -2820,7 +2929,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 478)
+[ Extern ] Froms (file share/libc/math.h, line 538)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2840,7 +2949,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 504)
+[ Extern ] Froms (file share/libc/math.h, line 564)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2860,7 +2969,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 530)
+[ Extern ] Froms (file share/libc/math.h, line 590)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2892,7 +3001,7 @@
[ Extern ] Post-condition for 'minus_infinity' 'no_error'
ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 573)
+[ Extern ] Assigns (file share/libc/math.h, line 633)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'minus_infinity' nothing
@@ -2901,16 +3010,16 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 573)
+[ Extern ] Froms (file share/libc/math.h, line 633)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 573)
+[ Extern ] Froms (file share/libc/math.h, line 633)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 596)
+[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 656)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 577)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 637)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2951,7 +3060,7 @@
[ Extern ] Post-condition for 'minus_infinity' 'no_error'
ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 610)
+[ Extern ] Assigns (file share/libc/math.h, line 670)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'minus_infinity' nothing
@@ -2960,16 +3069,16 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 610)
+[ Extern ] Froms (file share/libc/math.h, line 670)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 610)
+[ Extern ] Froms (file share/libc/math.h, line 670)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 633)
+[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 693)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 614)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 674)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3010,13 +3119,13 @@
[ 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)
+[ Extern ] Assigns (file share/libc/math.h, line 718)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 658)
+[ Extern ] Froms (file share/libc/math.h, line 718)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 658)
+[ Extern ] Froms (file share/libc/math.h, line 718)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3054,13 +3163,13 @@
[ 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)
+[ Extern ] Assigns (file share/libc/math.h, line 745)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 685)
+[ Extern ] Froms (file share/libc/math.h, line 745)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 685)
+[ Extern ] Froms (file share/libc/math.h, line 745)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3098,13 +3207,13 @@
[ 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)
+[ Extern ] Assigns (file share/libc/math.h, line 772)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 712)
+[ Extern ] Froms (file share/libc/math.h, line 772)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 712)
+[ Extern ] Froms (file share/libc/math.h, line 772)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3128,13 +3237,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 742)
+[ Extern ] Assigns (file share/libc/math.h, line 802)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 742)
+[ Extern ] Froms (file share/libc/math.h, line 802)
assigns __fc_errno \from x, exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 742)
+[ Extern ] Froms (file share/libc/math.h, line 802)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3152,13 +3261,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 762)
+[ Extern ] Assigns (file share/libc/math.h, line 822)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 762)
+[ Extern ] Froms (file share/libc/math.h, line 822)
assigns __fc_errno \from x, exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 762)
+[ Extern ] Froms (file share/libc/math.h, line 822)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3178,7 +3287,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 788)
+[ Extern ] Froms (file share/libc/math.h, line 848)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3198,7 +3307,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 819)
+[ Extern ] Froms (file share/libc/math.h, line 879)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3218,7 +3327,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 850)
+[ Extern ] Froms (file share/libc/math.h, line 910)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3238,7 +3347,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 881)
+[ Extern ] Froms (file share/libc/math.h, line 941)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3258,7 +3367,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 912)
+[ Extern ] Froms (file share/libc/math.h, line 972)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3278,7 +3387,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 943)
+[ Extern ] Froms (file share/libc/math.h, line 1003)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3298,7 +3407,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 978)
+[ Extern ] Froms (file share/libc/math.h, line 1038)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3318,7 +3427,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1009)
+[ Extern ] Froms (file share/libc/math.h, line 1069)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3338,7 +3447,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1040)
+[ Extern ] Froms (file share/libc/math.h, line 1100)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3363,7 +3472,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1087)
+[ Extern ] Froms (file share/libc/math.h, line 1147)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3388,7 +3497,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1105)
+[ Extern ] Froms (file share/libc/math.h, line 1165)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3413,7 +3522,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 1183)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3431,13 +3540,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 1145)
+[ Extern ] Assigns (file share/libc/math.h, line 1205)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1145)
+[ Extern ] Froms (file share/libc/math.h, line 1205)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1145)
+[ Extern ] Froms (file share/libc/math.h, line 1205)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3455,13 +3564,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 1160)
+[ Extern ] Assigns (file share/libc/math.h, line 1220)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1160)
+[ Extern ] Froms (file share/libc/math.h, line 1220)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1160)
+[ Extern ] Froms (file share/libc/math.h, line 1220)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3493,7 +3602,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 1241)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3519,7 +3628,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1210)
+[ Extern ] Froms (file share/libc/math.h, line 1270)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3542,7 +3651,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1239)
+[ Extern ] Froms (file share/libc/math.h, line 1299)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3559,7 +3668,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1279)
+[ Extern ] Froms (file share/libc/math.h, line 1339)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3576,7 +3685,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1296)
+[ Extern ] Froms (file share/libc/math.h, line 1356)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3593,7 +3702,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1313)
+[ Extern ] Froms (file share/libc/math.h, line 1373)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3610,7 +3719,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1330)
+[ Extern ] Froms (file share/libc/math.h, line 1390)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3627,7 +3736,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1347)
+[ Extern ] Froms (file share/libc/math.h, line 1407)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3644,7 +3753,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1364)
+[ Extern ] Froms (file share/libc/math.h, line 1424)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3661,7 +3770,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1397)
+[ Extern ] Froms (file share/libc/math.h, line 1457)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3678,7 +3787,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1414)
+[ Extern ] Froms (file share/libc/math.h, line 1474)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3695,7 +3804,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1431)
+[ Extern ] Froms (file share/libc/math.h, line 1491)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3712,7 +3821,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 1516)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3729,7 +3838,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1473)
+[ Extern ] Froms (file share/libc/math.h, line 1533)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3746,7 +3855,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1490)
+[ Extern ] Froms (file share/libc/math.h, line 1550)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3766,7 +3875,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1510)
+[ Extern ] Froms (file share/libc/math.h, line 1570)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3786,7 +3895,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1531)
+[ Extern ] Froms (file share/libc/math.h, line 1591)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3803,7 +3912,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1564)
+[ Extern ] Froms (file share/libc/math.h, line 1624)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3820,7 +3929,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1571)
+[ Extern ] Froms (file share/libc/math.h, line 1631)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3837,7 +3946,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1578)
+[ Extern ] Froms (file share/libc/math.h, line 1638)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3857,7 +3966,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1608)
+[ Extern ] Froms (file share/libc/math.h, line 1668)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3883,7 +3992,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1621)
+[ Extern ] Froms (file share/libc/math.h, line 1681)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3906,7 +4015,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1648)
+[ Extern ] Froms (file share/libc/math.h, line 1708)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3923,7 +4032,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1654)
+[ Extern ] Froms (file share/libc/math.h, line 1714)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4285,9 +4394,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 184 Completely validated
+ 191 Completely validated
16 Locally validated
- 534 Considered valid
+ 556 Considered valid
56 To be validated
- 790 Total
+ 819 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/math_h.c b/tests/libc/math_h.c
index 1c8cc1b985d07963b8277e5bc7b39d8183305c7d..bfd5ec4f929a9cb30bd81c72ce5aa580c609d2bf 100644
--- a/tests/libc/math_h.c
+++ b/tests/libc/math_h.c
@@ -1,6 +1,8 @@
/* run.config
FILTER: sed -E -e '/atanf_/ s/([0-9][.][0-9]{6})[0-9]+/\1/g'
STDOPT: #"-warn-special-float none" #"-cpp-extra-args=\"-DNONFINITE\"" #"-eva-slevel 4"
+ STDOPT: #"-warn-special-float nan" #"-cpp-extra-args=\"-DNONFINITE -DNONAN\"" #"-eva-slevel 4"
+ STDOPT: #"-eva-slevel 4"
*/
#include <math.h>
const double pi = 3.14159265358979323846264338327950288;
@@ -21,16 +23,22 @@ const double one = 1.0;
const double minus_one = -1.0;
const double large = 1e38;
#ifdef NONFINITE
-const double huge_val = HUGE_VAL;
-const float huge_valf = HUGE_VALF;
-const long double huge_vall = HUGE_VALL;
+const float f_pos_inf = HUGE_VALF;
+const double pos_inf = HUGE_VAL;
+const long double ld_pos_inf = HUGE_VALL;
+const float f_neg_inf = -HUGE_VALF;
+const double neg_inf = -HUGE_VAL;
+const long double ld_neg_inf = -HUGE_VALL;
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)
+volatile int nondet;
+
+#define TEST_VAL_CONST(type,f,cst) \
+ if (nondet) { 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); \
@@ -45,25 +53,39 @@ volatile int int_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); \
+#define TEST_VAL2_FST_CONST(type,f,cst,snd_arg,suffix) \
+ if (nondet) { 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)
+#ifdef NONFINITE
+#define TEST_FUN_NONFINITE(type,f,prefix) \
+ TEST_VAL_CONST(type,f,prefix##pos_inf); \
+ TEST_VAL_CONST(type,f,prefix##neg_inf)
+#else
+#define TEST_FUN_NONFINITE(type,f,prefix)
+#endif
+
+#define TEST_FUN_ALL_PREC(fun) \
+ TEST_FUN_CONSTS(double,fun,); \
+ TEST_FUN_CONSTS(float,fun ## f,f_); \
+ TEST_FUN_CONSTS(long double,fun ## l,ld_); \
+ TEST_FUN_NONFINITE(double,fun,); \
+ TEST_FUN_NONFINITE(float,fun ## f,f_); \
+ TEST_FUN_NONFINITE(long double,fun ## l,ld_)
+
int main() {
- 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_);
+ TEST_FUN_ALL_PREC(atan);
+ TEST_FUN_ALL_PREC(fabs);
+ TEST_FUN_ALL_PREC(tan);
int exponent;
TEST_FUN2_FST_CONSTS(double,frexp,,&exponent,);
TEST_FUN2_FST_CONSTS(float,frexpf,f_,&exponent,);
@@ -77,9 +99,9 @@ int main() {
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);
+ TEST_FUN2_FST_CONSTS(double,ldexp,,100000,_pos_inf);
+ TEST_FUN2_FST_CONSTS(float,ldexpf,f_,100000,_pos_inf);
+ //TEST_FUN2_FST_CONSTS(long double,ldexpl,ld_,100000,_pos_inf);
#ifdef NONFINITE
int r;
@@ -89,11 +111,13 @@ int main() {
//@ assert r;
r = isfinite(0.0f);
//@ assert r;
- r = isfinite(huge_val);
+ r = isfinite(pos_inf);
//@ assert !r;
r = isfinite(-INFINITY);
//@ assert !r;
+#ifndef NONAN
r = isfinite(NAN);
+#endif
//@ assert !r;
#endif
}
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e78d1082652406952488171029bc8f3bcd957daf..52ea02c4ae31933fef4f719db82c1493a10b18a3 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -46,7 +46,7 @@
wcslen (3 calls); wcsncat (0 call); wcsncpy (0 call); wmemcpy (1 call);
wmemset (0 call);
- Specified-only functions (423)
+ Specified-only functions (426)
==============================
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);
@@ -163,17 +163,18 @@
strtok (0 call); strtok_r (0 call); strtol (0 call); strtold (0 call);
strtoll (0 call); strtoul (0 call); strtoull (0 call); strxfrm (0 call);
sync (0 call); sysconf (0 call); syslog (0 call); system (0 call);
- tcflush (0 call); tcgetattr (0 call); tcsetattr (0 call); time (0 call);
- times (0 call); tmpfile (0 call); tmpnam (0 call); trunc (0 call);
- truncf (0 call); truncl (0 call); ttyname (0 call); tzset (0 call);
- umask (0 call); uname (0 call); ungetc (0 call); unlink (0 call);
- usleep (0 call); utimes (0 call); vfprintf (0 call); vfscanf (0 call);
- vprintf (0 call); vscanf (0 call); vsnprintf (0 call); vsprintf (0 call);
- vsyslog (0 call); wait (0 call); waitpid (0 call); wcscasecmp (0 call);
- wcschr (0 call); wcscmp (0 call); wcscspn (0 call); wcslcat (0 call);
- wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call);
- wcsspn (0 call); wcsstr (0 call); wcstombs (0 call); wctomb (0 call);
- wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call); write (0 call);
+ tan (0 call); tanf (0 call); tanl (0 call); tcflush (0 call);
+ tcgetattr (0 call); tcsetattr (0 call); time (0 call); times (0 call);
+ tmpfile (0 call); tmpnam (0 call); trunc (0 call); truncf (0 call);
+ truncl (0 call); ttyname (0 call); tzset (0 call); umask (0 call);
+ uname (0 call); ungetc (0 call); unlink (0 call); usleep (0 call);
+ utimes (0 call); vfprintf (0 call); vfscanf (0 call); vprintf (0 call);
+ vscanf (0 call); vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call);
+ wait (0 call); waitpid (0 call); wcscasecmp (0 call); wcschr (0 call);
+ wcscmp (0 call); wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call);
+ wcsncmp (0 call); wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call);
+ wcsstr (0 call); wcstombs (0 call); wctomb (0 call); wmemchr (0 call);
+ wmemcmp (0 call); wmemmove (0 call); write (0 call);
Undefined and unspecified functions (1)
=======================================
@@ -202,7 +203,7 @@
Goto = 112
Assignment = 618
Exit point = 99
- Function = 523
+ Function = 526
Function call = 141
Pointer dereferencing = 249
Cyclomatic complexity = 369
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 6bc8c7e7ed63a16dde73c5e20be6b47b952ab5ce..1cf9de7928fa9e8efe8d3e4a9bb357bdf0a8e2b3 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3758,6 +3758,64 @@ extern float sinf(float x);
*/
extern long double sinl(long double x);
+/*@ requires not_infinity: ¬(infinite_arg: \is_infinite(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from x;
+ assigns \result \from x;
+
+ behavior zero:
+ assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
+ ensures zero_res: \is_finite(\result) ∧ \result ≡ \old(x);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
+ assigns \result \from x;
+
+ behavior finite_non_zero:
+ assumes finite_arg: \is_finite(x) ∧ x ≢ 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures
+ maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34;
+
+ complete behaviors finite_non_zero, zero;
+ disjoint behaviors finite_non_zero, zero;
+ */
+extern double tan(double x);
+
+/*@ requires not_infinity: ¬(infinite_arg: \is_infinite(x));
+ requires not_nan: ¬(nan_arg: \is_NaN(x));
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from x;
+ assigns \result \from x;
+
+ behavior zero:
+ assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
+ ensures zero_res: \is_finite(\result) ∧ \result ≡ \old(x);
+ ensures no_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
+ assigns \result \from x;
+
+ behavior finite_non_zero:
+ assumes finite_arg: \is_finite(x) ∧ x ≢ 0.;
+ ensures finite_result: \is_finite(\result);
+ ensures
+ maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34;
+
+ complete behaviors finite_non_zero, zero;
+ disjoint behaviors finite_non_zero, zero;
+ */
+extern float tanf(float x);
+
+/*@ ensures
+ maybe_error:
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 33 ∨
+ __fc_errno ≡ 34;
+ assigns __fc_errno, \result;
+ assigns __fc_errno \from x;
+ assigns \result \from x;
+ */
+extern long double tanl(long double x);
+
/*@ requires in_domain: \is_finite(x) ∧ x ≥ 1;
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0;
ensures no_error: __fc_errno ≡ \old(__fc_errno);
diff --git a/tests/libc/oracle/math_h.0.res.oracle b/tests/libc/oracle/math_h.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..6270a1a96a98be26db438a332ddd1f738ebc5a9c
--- /dev/null
+++ b/tests/libc/oracle/math_h.0.res.oracle
@@ -0,0 +1,719 @@
+[kernel] Parsing tests/libc/math_h.c (with preprocessing)
+[kernel:parser:decimal-float] tests/libc/math_h.c:8: Warning:
+ Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ pi ∈ {3.14159265359}
+ half_pi ∈ {1.57079632679}
+ e ∈ {2.71828182846}
+ top ∈ [--..--]
+ f_pi ∈ {3.14159274101}
+ f_half_pi ∈ {1.57079637051}
+ f_e ∈ {2.71828174591}
+ f_top ∈ [--..--]
+ ld_pi ∈ [3.14159265359 .. 3.14159265359]
+ ld_half_pi ∈ [1.57079632679 .. 1.57079632679]
+ ld_e ∈ {2.71828182846}
+ ld_top ∈ [--..--]
+ zero ∈ {0}
+ minus_zero ∈ {-0.}
+ one ∈ {1.}
+ minus_one ∈ {-1.}
+ large ∈ {1e+38}
+ f_pos_inf ∈ {inf}
+ pos_inf ∈ {inf}
+ ld_pos_inf ∈ {inf}
+ f_neg_inf ∈ {-inf}
+ neg_inf ∈ {-inf}
+ ld_neg_inf ∈ {-inf}
+ infinity ∈ {inf}
+ fp_ilogb0 ∈ {-2147483648.}
+ fp_ilogbnan ∈ {-2147483648.}
+ int_top ∈ [--..--]
+ nondet ∈ [--..--]
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] using specification for function atanl
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] Done for function atanl
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabs
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsf
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsl
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] Done for function fabsl
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tan
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanf
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanl
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ 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:90.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:91.
+[eva] tests/libc/math_h.c:91:
+ 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:92.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:92.
+[eva] tests/libc/math_h.c:92:
+ 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:93.
+[eva] using specification for function ldexp
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] using specification for function ldexpf
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] Done for function ldexpf
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:108.
+[eva] using specification for function __finite
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:109: assertion got status valid.
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:111: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:112.
+[eva] using specification for function __finitef
+[eva] Done for function __finitef
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:112.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:113: assertion got status valid.
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:115: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:116.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:117: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:119.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:121: 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 ∈ [--..--]
+ exponent ∈ [--..--] or UNINITIALIZED
+ r ∈ {0}
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/math_h.1.res.oracle b/tests/libc/oracle/math_h.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a2d2aea1a03b92001e491fd95188438caf24580c
--- /dev/null
+++ b/tests/libc/oracle/math_h.1.res.oracle
@@ -0,0 +1,1171 @@
+[kernel] Parsing tests/libc/math_h.c (with preprocessing)
+[kernel:parser:decimal-float] tests/libc/math_h.c:8: Warning:
+ Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ pi ∈ {3.14159265359}
+ half_pi ∈ {1.57079632679}
+ e ∈ {2.71828182846}
+ top ∈ [--..--]
+ f_pi ∈ {3.14159274101}
+ f_half_pi ∈ {1.57079637051}
+ f_e ∈ {2.71828174591}
+ f_top ∈ [--..--]
+ ld_pi ∈ [3.14159265359 .. 3.14159265359]
+ ld_half_pi ∈ [1.57079632679 .. 1.57079632679]
+ ld_e ∈ {2.71828182846}
+ ld_top ∈ [--..--]
+ zero ∈ {0}
+ minus_zero ∈ {-0.}
+ one ∈ {1.}
+ minus_one ∈ {-1.}
+ large ∈ {1e+38}
+ f_pos_inf ∈ {inf}
+ pos_inf ∈ {inf}
+ ld_pos_inf ∈ {inf}
+ f_neg_inf ∈ {-inf}
+ neg_inf ∈ {-inf}
+ ld_neg_inf ∈ {-inf}
+ infinity ∈ {inf}
+ fp_ilogb0 ∈ {-2147483648.}
+ fp_ilogbnan ∈ {-2147483648.}
+ int_top ∈ [--..--]
+ nondet ∈ [--..--]
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva:alarm] tests/libc/math_h.c:86: Warning:
+ function atan: precondition 'number_arg' got status unknown.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva:alarm] tests/libc/math_h.c:86: Warning:
+ function atanf: precondition 'number_arg' got status unknown.
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] using specification for function atanl
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva:alarm] tests/libc/math_h.c:86: Warning:
+ NaN long double value. assert ¬\is_NaN(ld_top);
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabs
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva:alarm] tests/libc/math_h.c:87: Warning:
+ NaN double value. assert ¬\is_NaN(top);
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsf
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva:alarm] tests/libc/math_h.c:87: Warning:
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsl
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva:alarm] tests/libc/math_h.c:87: Warning:
+ NaN long double value. assert ¬\is_NaN(ld_top);
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'not_nan' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'not_nan' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'not_nan' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tan
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ NaN double value. assert ¬\is_NaN(top);
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tan: precondition 'not_infinity' got status unknown.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanf
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tanf: precondition 'not_infinity' got status unknown.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanl
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ NaN long double value. assert ¬\is_NaN(ld_top);
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tan: precondition 'not_infinity' got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tan: no state left, precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tan: precondition 'not_infinity' got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tan: no state left, precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tanf: precondition 'not_infinity' got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: no state left, precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tanf: precondition 'not_infinity' got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: no state left, precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva:alarm] tests/libc/math_h.c:90: Warning:
+ NaN double value. assert ¬\is_NaN(top);
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva:alarm] tests/libc/math_h.c:91: Warning:
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva:alarm] tests/libc/math_h.c:92: Warning:
+ NaN long double value. assert ¬\is_NaN(ld_top);
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] using specification for function ldexp
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:93: Warning:
+ NaN double value. assert ¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] using specification for function ldexpf
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:94: Warning:
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:96: Warning:
+ NaN double value. assert ¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:97: Warning:
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:99: Warning:
+ NaN double value. assert ¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:100: Warning:
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ NaN double value. assert ¬\is_NaN(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva] tests/libc/math_h.c:102:
+ function ldexp: precondition 'not_nan' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ NaN float value. assert ¬\is_NaN(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva] tests/libc/math_h.c:103:
+ function ldexpf: precondition 'not_nan' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:108.
+[eva] using specification for function __finite
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:109: assertion got status valid.
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:110.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:111: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:112.
+[eva] using specification for function __finitef
+[eva] Done for function __finitef
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:112.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:113: assertion got status valid.
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:114.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:115: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:116.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:117: assertion got status valid.
+[eva] tests/libc/math_h.c:121: assertion got status valid.
+[eva] Recording results for main
+[eva] done for function main
+[scope:rm_asserts] removing 1 assertion(s)
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
+ exponent ∈ [--..--] or UNINITIALIZED
+ r ∈ {0}
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/math_h.2.res.oracle b/tests/libc/oracle/math_h.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..2caf779ac2d3dbe01b4529a7926554c84e3dbe36
--- /dev/null
+++ b/tests/libc/oracle/math_h.2.res.oracle
@@ -0,0 +1,1098 @@
+[kernel] Parsing tests/libc/math_h.c (with preprocessing)
+[kernel:parser:decimal-float] tests/libc/math_h.c:8: Warning:
+ Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
+ (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ pi ∈ {3.14159265359}
+ half_pi ∈ {1.57079632679}
+ e ∈ {2.71828182846}
+ top ∈ [--..--]
+ f_pi ∈ {3.14159274101}
+ f_half_pi ∈ {1.57079637051}
+ f_e ∈ {2.71828174591}
+ f_top ∈ [--..--]
+ ld_pi ∈ [3.14159265359 .. 3.14159265359]
+ ld_half_pi ∈ [1.57079632679 .. 1.57079632679]
+ ld_e ∈ {2.71828182846}
+ ld_top ∈ [--..--]
+ zero ∈ {0}
+ minus_zero ∈ {-0.}
+ one ∈ {1.}
+ minus_one ∈ {-1.}
+ large ∈ {1e+38}
+ fp_ilogb0 ∈ {-2147483648.}
+ fp_ilogbnan ∈ {-2147483648.}
+ int_top ∈ [--..--]
+ nondet ∈ [--..--]
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva] tests/libc/math_h.c:86:
+ function atan: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atan
+[eva:alarm] tests/libc/math_h.c:86: Warning:
+ function atan: precondition 'number_arg' got status unknown.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva] tests/libc/math_h.c:86:
+ function atanf: precondition 'number_arg' got status valid.
+[eva] tests/libc/math_h.c:86: Call to builtin atanf
+[eva:alarm] tests/libc/math_h.c:86: Warning:
+ function atanf: precondition 'number_arg' got status unknown.
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] using specification for function atanl
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva:alarm] tests/libc/math_h.c:86: Warning:
+ non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function atanl <- main.
+ Called from tests/libc/math_h.c:86.
+[eva] tests/libc/math_h.c:86:
+ function atanl: precondition 'number_arg' got status valid.
+[eva] Done for function atanl
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabs
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva:alarm] tests/libc/math_h.c:87: Warning:
+ non-finite double value. assert \is_finite(top);
+[eva] computing for function fabs <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabs: precondition 'finite_arg' got status valid.
+[eva] Done for function fabs
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsf
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva:alarm] tests/libc/math_h.c:87: Warning:
+ non-finite float value. assert \is_finite(f_top);
+[eva] computing for function fabsf <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsf: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsf
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] using specification for function fabsl
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva] tests/libc/math_h.c:87:
+ function fabsl: precondition 'finite_arg' got status valid.
+[eva] Done for function fabsl
+[eva:alarm] tests/libc/math_h.c:87: Warning:
+ non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function fabsl <- main.
+ Called from tests/libc/math_h.c:87.
+[eva:alarm] tests/libc/math_h.c:87: Warning:
+ function fabsl: precondition 'finite_arg' got status unknown.
+[eva] Done for function fabsl
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tan
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ non-finite double value. assert \is_finite(top);
+[eva] computing for function tan <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition 'not_nan' got status valid.
+[eva] Done for function tan
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanf
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ non-finite float value. assert \is_finite(f_top);
+[eva] computing for function tanf <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_infinity' got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition 'not_nan' got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] using specification for function tanl
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] Done for function tanl
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] using specification for function frexp
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva:alarm] tests/libc/math_h.c:90: Warning:
+ non-finite double value. assert \is_finite(top);
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition 'not_nan' got status valid.
+[eva] Done for function frexp
+[eva] computing for function frexp <- main.
+ Called from tests/libc/math_h.c:90.
+[eva] Done for function frexp
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] using specification for function frexpf
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva:alarm] tests/libc/math_h.c:91: Warning:
+ non-finite float value. assert \is_finite(f_top);
+[eva] computing for function frexpf <- main.
+ Called from tests/libc/math_h.c:91.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition 'not_nan' got status valid.
+[eva] Done for function frexpf
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] using specification for function frexpl
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_infinite' got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva:alarm] tests/libc/math_h.c:92: Warning:
+ non-finite long double value. assert \is_finite(ld_top);
+[eva] computing for function frexpl <- main.
+ Called from tests/libc/math_h.c:92.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'valid_exp' got status valid.
+[eva:alarm] tests/libc/math_h.c:92: Warning:
+ function frexpl: precondition 'not_infinite' got status unknown.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition 'not_nan' got status valid.
+[eva] Done for function frexpl
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] using specification for function ldexp
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva] tests/libc/math_h.c:93:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:93: Warning:
+ non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:93.
+[eva:alarm] tests/libc/math_h.c:93: Warning:
+ function ldexp: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] using specification for function ldexpf
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva] tests/libc/math_h.c:94:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva:alarm] tests/libc/math_h.c:94: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:94: Warning:
+ non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:94.
+[eva:alarm] tests/libc/math_h.c:94: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:96: Warning:
+ non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:96.
+[eva] tests/libc/math_h.c:96:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:97: Warning:
+ non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:97.
+[eva] tests/libc/math_h.c:97:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:99: Warning:
+ non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:99.
+[eva] tests/libc/math_h.c:99:
+ function ldexp: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:100: Warning:
+ non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:100.
+[eva] tests/libc/math_h.c:100:
+ function ldexpf: precondition 'finite_logic_res' got status valid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexp
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ non-finite double value. assert \is_finite(top);
+[eva] computing for function ldexp <- main.
+ Called from tests/libc/math_h.c:102.
+[eva:alarm] tests/libc/math_h.c:102: Warning:
+ function ldexp: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexp
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status invalid.
+[eva] Done for function ldexpf
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ non-finite float value. assert \is_finite(f_top);
+[eva] computing for function ldexpf <- main.
+ Called from tests/libc/math_h.c:103.
+[eva:alarm] tests/libc/math_h.c:103: Warning:
+ function ldexpf: precondition 'finite_logic_res' got status unknown.
+[eva] Done for function ldexpf
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main:
+ __fc_errno ∈ [--..--]
+ exponent ∈ [--..--] or UNINITIALIZED
+ __retres ∈ {0}
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
deleted file mode 100644
index 098f41b2d50485bb9e2598d9aba1d05d10190ce3..0000000000000000000000000000000000000000
--- a/tests/libc/oracle/math_h.res.oracle
+++ /dev/null
@@ -1,903 +0,0 @@
-[kernel] Parsing tests/libc/math_h.c (with preprocessing)
-[kernel:parser:decimal-float] tests/libc/math_h.c:6: Warning:
- Floating-point constant 3.14159265358979323846264338327950288 is not represented exactly. Will use 0x1.921fb54442d18p1.
- (warn-once: no further messages from category 'parser:decimal-float' will be emitted)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- pi ∈ {3.14159265359}
- half_pi ∈ {1.57079632679}
- e ∈ {2.71828182846}
- top ∈ [--..--]
- f_pi ∈ {3.14159274101}
- f_half_pi ∈ {1.57079637051}
- f_e ∈ {2.71828174591}
- f_top ∈ [--..--]
- ld_pi ∈ [3.14159265359 .. 3.14159265359]
- ld_half_pi ∈ [1.57079632679 .. 1.57079632679]
- ld_e ∈ {2.71828182846}
- ld_top ∈ [--..--]
- zero ∈ {0}
- minus_zero ∈ {-0.}
- one ∈ {1.}
- minus_one ∈ {-1.}
- large ∈ {1e+38}
- huge_val ∈ {inf}
- huge_valf ∈ {inf}
- huge_vall ∈ {inf}
- infinity ∈ {inf}
- fp_ilogb0 ∈ {-2147483648.}
- fp_ilogbnan ∈ {-2147483648.}
- 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: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:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
- 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:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
- 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:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
- 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:63.
-[eva] Done for function atanl
-[eva] computing for function atanl <- main.
- 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: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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabs <- main.
- 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:64.
-[eva] Done for function fabs
-[eva] computing for function fabsf <- main.
- 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:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
- 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:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
- 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:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
- 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:65.
-[eva] Done for function fabsf
-[eva] computing for function fabsf <- main.
- 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: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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:66.
-[eva] Done for function fabsl
-[eva] computing for function fabsl <- main.
- 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:86.
-[eva] using specification for function __finite
-[eva] Done for function __finite
-[eva] tests/libc/math_h.c:87: assertion got status valid.
-[eva] computing for function __finite <- main.
- 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:88.
-[eva] Done for function __finite
-[eva] tests/libc/math_h.c:89: assertion got status valid.
-[eva] computing for function __finitef <- main.
- 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:90.
-[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:91: assertion got status valid.
-[eva] computing for function __finite <- main.
- 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:92.
-[eva] Done for function __finite
-[eva] tests/libc/math_h.c:93: assertion got status valid.
-[eva] computing for function __finitef <- main.
- Called from tests/libc/math_h.c:94.
-[eva] Done for function __finitef
-[eva] tests/libc/math_h.c:95: assertion got status valid.
-[eva] computing for function __finitef <- main.
- Called from tests/libc/math_h.c:96.
-[eva] Done for function __finitef
-[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}
- atan_zero ∈ {0}
- atan_minus_zero ∈ {-0.}
- atan_one ∈ {0.785398163397}
- atan_minus_one ∈ {-0.785398163397}
- atan_large ∈ {1.57079632679}
- atan_top ∈ [-1.57079632679 .. 1.57079632679] ∪ {NaN}
- atanf_f_pi ∈ {1.262627}
- atanf_f_half_pi ∈ {1.003884}
- atanf_f_e ∈ {1.218282}
- atanf_zero ∈ {0}
- atanf_minus_zero ∈ {-0.}
- atanf_one ∈ {0.785398}
- atanf_minus_one ∈ {-0.785398}
- atanf_large ∈ {1.570796}
- atanf_f_top ∈ [-1.570796 .. 1.570796] ∪ {NaN}
- atanl_ld_pi ∈ [-inf .. inf]
- atanl_ld_half_pi ∈ [-inf .. inf]
- atanl_ld_e ∈ [-inf .. inf]
- atanl_zero ∈ [-inf .. inf]
- atanl_minus_zero ∈ [-inf .. inf]
- atanl_one ∈ [-inf .. inf]
- atanl_minus_one ∈ [-inf .. inf]
- atanl_large ∈ [-inf .. inf]
- atanl_ld_top ∈ [-inf .. inf] ∪ {NaN}
- fabs_pi ∈ {3.14159265359}
- fabs_half_pi ∈ {1.57079632679}
- fabs_e ∈ {2.71828182846}
- fabs_zero ∈ [-0. .. 0.]
- fabs_minus_zero ∈ [-0. .. 0.]
- fabs_one ∈ {1.}
- fabs_minus_one ∈ {1.}
- fabs_large ∈ {1e+38}
- fabs_top ∈ [-0. .. inf] ∪ {NaN}
- fabsf_f_pi ∈ {3.14159274101}
- fabsf_f_half_pi ∈ {1.57079637051}
- fabsf_f_e ∈ {2.71828174591}
- fabsf_zero ∈ [-0. .. 0.]
- fabsf_minus_zero ∈ [-0. .. 0.]
- fabsf_one ∈ {1.}
- fabsf_minus_one ∈ {1.}
- fabsf_large ∈ {9.99999968029e+37}
- fabsf_f_top ∈ [-0. .. inf] ∪ {NaN}
- fabsl_ld_pi ∈ [-inf .. inf]
- fabsl_ld_half_pi ∈ [-inf .. inf]
- fabsl_ld_e ∈ [-inf .. inf]
- fabsl_zero ∈ [-inf .. inf]
- fabsl_minus_zero ∈ [-inf .. inf]
- fabsl_one ∈ [-inf .. inf]
- 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}