From 511408fa530b6d22bb126eb99fc991d4bf66a9ac Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 11 May 2021 17:33:30 +0200
Subject: [PATCH] update test oracles
---
.../report/tests/report/oracle/csv.csv | 2 +-
tests/idct/oracle/ieee_1180_1990.res.oracle | 287 +++-
tests/libc/oracle/fc_libc.0.res.oracle | 27 +-
tests/libc/oracle/fc_libc.1.res.oracle | 75 ++
tests/libc/oracle/math_h.0.res.oracle | 719 ++++++++++
tests/libc/oracle/math_h.1.res.oracle | 1110 +++++++++++++++
tests/libc/oracle/math_h.2.res.oracle | 1188 +++++++++++++++++
tests/libc/oracle/math_h.res.oracle | 903 -------------
8 files changed, 3321 insertions(+), 990 deletions(-)
create mode 100644 tests/libc/oracle/math_h.0.res.oracle
create mode 100644 tests/libc/oracle/math_h.1.res.oracle
create mode 100644 tests/libc/oracle/math_h.2.res.oracle
delete mode 100644 tests/libc/oracle/math_h.res.oracle
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 3dbfbfd16cc..78639540067 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 1221 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 2596ed249ed..0bfa1f9130f 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2807,6 +2807,147 @@
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' 'result_not_nan'
+ ensures result_not_nan: ¬\is_NaN(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'finite_non_zero' 'maybe_error'
+ ensures maybe_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 471)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'finite_non_zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 471)
+ assigns __fc_errno \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 471)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'finite_non_zero' (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 474)
+ 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' 'result_not_nan'
+ ensures result_not_nan: ¬\is_NaN(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'finite_non_zero' 'maybe_error'
+ ensures maybe_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 497)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'finite_non_zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 497)
+ assigns __fc_errno \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 497)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'finite_non_zero' (file share/libc/math.h, line 505)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'zero' (file share/libc/math.h, line 500)
+ 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 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' 'result_not_nan'
+ ensures result_not_nan: ¬\is_NaN(\result)
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'finite_non_zero' 'maybe_error'
+ ensures maybe_error: __fc_errno ≡ \old(__fc_errno)
+ Unverifiable but considered Valid.
+[ Extern ] Assigns (file share/libc/math.h, line 523)
+ assigns __fc_errno, \result;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'finite_non_zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Assigns for 'zero' nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 523)
+ assigns __fc_errno \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 523)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'finite_non_zero' (file share/libc/math.h, line 531)
+ assigns \result \from x;
+ Unverifiable but considered Valid.
+[ Extern ] Froms for 'zero' (file share/libc/math.h, line 526)
+ 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 'acosh'
--------------------------------------------------------------------------------
@@ -2820,7 +2961,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 552)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2840,7 +2981,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 578)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2860,7 +3001,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 604)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2892,7 +3033,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 647)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'minus_infinity' nothing
@@ -2901,16 +3042,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 647)
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 647)
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 670)
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 651)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2951,7 +3092,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 684)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'minus_infinity' nothing
@@ -2960,16 +3101,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 684)
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 684)
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 707)
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 688)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3010,13 +3151,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 732)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 658)
+[ Extern ] Froms (file share/libc/math.h, line 732)
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 732)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3054,13 +3195,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 759)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 685)
+[ Extern ] Froms (file share/libc/math.h, line 759)
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 759)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3098,13 +3239,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 786)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 712)
+[ Extern ] Froms (file share/libc/math.h, line 786)
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 786)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3128,13 +3269,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 816)
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 816)
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 816)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3152,13 +3293,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 836)
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 836)
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 836)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3178,7 +3319,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 862)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3198,7 +3339,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 893)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3218,7 +3359,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 924)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3238,7 +3379,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 955)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3258,7 +3399,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 986)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3278,7 +3419,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 1017)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3298,7 +3439,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 1052)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3318,7 +3459,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 1083)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3338,7 +3479,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 1114)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3363,7 +3504,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 1161)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3388,7 +3529,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 1179)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3413,7 +3554,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 1197)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3431,13 +3572,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 1219)
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 1219)
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 1219)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3455,13 +3596,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 1234)
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 1234)
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 1234)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3493,7 +3634,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 1255)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3519,7 +3660,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 1284)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3542,7 +3683,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 1313)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3559,7 +3700,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 1353)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3576,7 +3717,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 1370)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3593,7 +3734,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 1387)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3610,7 +3751,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 1404)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3627,7 +3768,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 1421)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3644,7 +3785,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 1438)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3661,7 +3802,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 1471)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3678,7 +3819,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 1488)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3695,7 +3836,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 1505)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3712,7 +3853,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 1530)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3729,7 +3870,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 1547)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3746,7 +3887,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 1564)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3766,7 +3907,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 1584)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3786,7 +3927,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 1605)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3803,7 +3944,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 1638)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3820,7 +3961,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 1645)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3837,7 +3978,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 1652)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3857,7 +3998,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 1682)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3883,7 +4024,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 1695)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3906,7 +4047,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 1722)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3923,7 +4064,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 1728)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4285,9 +4426,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 184 Completely validated
+ 193 Completely validated
16 Locally validated
- 534 Considered valid
+ 567 Considered valid
56 To be validated
- 790 Total
+ 832 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index e78d1082652..52ea02c4ae3 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 6bc8c7e7ed6..abbb75a19d6 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3758,6 +3758,81 @@ extern float sinf(float x);
*/
extern long double sinl(long double x);
+/*@ requires ¬(infinite_arg: \is_infinite(x));
+ requires ¬(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 result_not_nan: ¬\is_NaN(\result);
+ ensures maybe_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
+ assigns \result \from x;
+
+ complete behaviors finite_non_zero, zero;
+ disjoint behaviors finite_non_zero, zero;
+ */
+extern double tan(double x);
+
+/*@ requires ¬(infinite_arg: \is_infinite(x));
+ requires ¬(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 result_not_nan: ¬\is_NaN(\result);
+ ensures maybe_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
+ assigns \result \from x;
+
+ complete behaviors finite_non_zero, zero;
+ disjoint behaviors finite_non_zero, zero;
+ */
+extern float tanf(float x);
+
+/*@ requires ¬(infinite_arg: \is_infinite(x));
+ requires ¬(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 result_not_nan: ¬\is_NaN(\result);
+ ensures maybe_error: __fc_errno ≡ \old(__fc_errno);
+ assigns \result;
+ assigns \result \from x;
+
+ complete behaviors finite_non_zero, zero;
+ disjoint behaviors finite_non_zero, zero;
+ */
+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 00000000000..6270a1a96a9
--- /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 00000000000..7b044ea68c6
--- /dev/null
+++ b/tests/libc/oracle/math_h.1.res.oracle
@@ -0,0 +1,1110 @@
+[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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[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:alarm] tests/libc/math_h.c:88: Warning:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[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 ¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tan: no state left, precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tan: no state left, precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: no state left, precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanf
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva:alarm] tests/libc/math_h.c:88: Warning:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status invalid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: no state left, precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 ¬(nan_arg: \is_NaN(x)) 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 00000000000..2c5443e6086
--- /dev/null
+++ b/tests/libc/oracle/math_h.2.res.oracle
@@ -0,0 +1,1188 @@
+[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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tan: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanf: precondition ¬(nan_arg: \is_NaN(x)) 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] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[eva] Done for function tanl
+[eva] computing for function tanl <- main.
+ Called from tests/libc/math_h.c:88.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status valid.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[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:alarm] tests/libc/math_h.c:88: Warning:
+ function tanl: precondition ¬(infinite_arg: \is_infinite(x)) got status unknown.
+[eva] tests/libc/math_h.c:88:
+ function tanl: precondition ¬(nan_arg: \is_NaN(x)) got status valid.
+[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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:90:
+ function frexp: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:91:
+ function frexpf: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status valid.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 ¬(infinite_arg:
+ \is_plus_infinity(x) ∨
+ \is_minus_infinity(x)) got status unknown.
+[eva] tests/libc/math_h.c:92:
+ function frexpl: precondition ¬(nan_arg: \is_NaN(x)) 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 098f41b2d50..00000000000
--- 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}
--
GitLab