diff --git a/share/libc/math.h b/share/libc/math.h
index 6ae90331c2e87b965357c3ab315858a8558aae2b..ff2ef56a2db3aacb58d304f6e818caae62869885 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -61,6 +61,9 @@ typedef double double_t;
 #define FP_SUBNORMAL 3
 #define FP_NORMAL 4
 
+#define FP_ILOGB0 __FC_INT_MIN
+#define FP_ILOGBNAN __FC_INT_MIN
+
 #include "float.h" // for DBL_MIN and FLT_MIN
 
 /*@
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index c44a659ed70c59996a52187b9e77c2f1e8253048..4a8fc2e347b0524ed2dd3a46002026834a250e5d 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	522	pow	precondition	Unknown	finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc	math.h	525	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 9cd3bd3d041d28f969185ef6d728ca3a37f273f3..73d8292ef2d19481c245a9c711c673355dc5f816 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2291,7 +2291,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 67)
+[ Extern  ] Froms (file share/libc/math.h, line 70)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2335,7 +2335,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 91)
+[ Extern  ] Froms (file share/libc/math.h, line 94)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2367,28 +2367,28 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 128)
+[ Extern  ] Assigns (file share/libc/math.h, line 131)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 135)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 138)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 128)
+[ Extern  ] Froms (file share/libc/math.h, line 131)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 128)
+[ Extern  ] Froms (file share/libc/math.h, line 131)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 135)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 138)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 135)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 138)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 131)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 134)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2411,28 +2411,28 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 142)
+[ Extern  ] Assigns (file share/libc/math.h, line 145)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 149)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 152)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 142)
+[ Extern  ] Froms (file share/libc/math.h, line 145)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 142)
+[ Extern  ] Froms (file share/libc/math.h, line 145)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 149)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 152)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 149)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 152)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 145)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 148)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2455,28 +2455,28 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 156)
+[ Extern  ] Assigns (file share/libc/math.h, line 159)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 163)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 166)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 156)
+[ Extern  ] Froms (file share/libc/math.h, line 159)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 156)
+[ Extern  ] Froms (file share/libc/math.h, line 159)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 163)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 166)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 163)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 166)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 159)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 162)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2499,28 +2499,28 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 170)
+[ Extern  ] Assigns (file share/libc/math.h, line 173)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 177)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 180)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 170)
+[ Extern  ] Froms (file share/libc/math.h, line 173)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 170)
+[ Extern  ] Froms (file share/libc/math.h, line 173)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 177)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 180)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 177)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 180)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 173)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 176)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2543,28 +2543,28 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 184)
+[ Extern  ] Assigns (file share/libc/math.h, line 187)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 191)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 194)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 184)
+[ Extern  ] Froms (file share/libc/math.h, line 187)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 184)
+[ Extern  ] Froms (file share/libc/math.h, line 187)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 191)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 194)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 191)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 194)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 187)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 190)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2587,28 +2587,28 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 198)
+[ Extern  ] Assigns (file share/libc/math.h, line 201)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 205)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 208)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 198)
+[ Extern  ] Froms (file share/libc/math.h, line 201)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 198)
+[ Extern  ] Froms (file share/libc/math.h, line 201)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 205)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 208)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 205)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 208)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 201)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 204)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2634,7 +2634,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 212)
+[ Extern  ] Froms (file share/libc/math.h, line 215)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2654,7 +2654,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 219)
+[ Extern  ] Froms (file share/libc/math.h, line 222)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2674,7 +2674,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 226)
+[ Extern  ] Froms (file share/libc/math.h, line 229)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2691,7 +2691,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 234)
+[ Extern  ] Froms (file share/libc/math.h, line 237)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2708,7 +2708,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 241)
+[ Extern  ] Froms (file share/libc/math.h, line 244)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2731,7 +2731,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 249)
+[ Extern  ] Froms (file share/libc/math.h, line 252)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2751,7 +2751,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 256)
+[ Extern  ] Froms (file share/libc/math.h, line 259)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2771,7 +2771,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 263)
+[ Extern  ] Froms (file share/libc/math.h, line 266)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2791,7 +2791,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 270)
+[ Extern  ] Froms (file share/libc/math.h, line 273)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2811,7 +2811,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 277)
+[ Extern  ] Froms (file share/libc/math.h, line 280)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2831,7 +2831,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 284)
+[ Extern  ] Froms (file share/libc/math.h, line 287)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2851,10 +2851,10 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 295)
+[ Extern  ] Assigns (file share/libc/math.h, line 298)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 306)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 309)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'infinite' nothing
@@ -2863,22 +2863,22 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 295)
+[ Extern  ] Froms (file share/libc/math.h, line 298)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 295)
+[ Extern  ] Froms (file share/libc/math.h, line 298)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 306)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 309)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 306)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 309)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 302)
+[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 305)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 298)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 301)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2907,10 +2907,10 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 313)
+[ Extern  ] Assigns (file share/libc/math.h, line 316)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 324)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 327)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'infinite' nothing
@@ -2919,22 +2919,22 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 313)
+[ Extern  ] Froms (file share/libc/math.h, line 316)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 313)
+[ Extern  ] Froms (file share/libc/math.h, line 316)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 324)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 327)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 324)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 327)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 320)
+[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 323)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 316)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 319)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -2963,10 +2963,10 @@
 [ Extern  ] Post-condition for 'domain_error' 'errno_set'
             ensures errno_set: __fc_errno ≡ 1
             Unverifiable but considered Valid.
-[ Extern  ] Assigns (file share/libc/math.h, line 331)
+[ Extern  ] Assigns (file share/libc/math.h, line 334)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
-[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 342)
+[ Extern  ] Assigns for 'domain_error' (file share/libc/math.h, line 345)
             assigns __fc_errno, \result;
             Unverifiable but considered Valid.
 [ Extern  ] Assigns for 'infinite' nothing
@@ -2975,22 +2975,22 @@
 [ Extern  ] Assigns for 'normal' nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 331)
+[ Extern  ] Froms (file share/libc/math.h, line 334)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 331)
+[ Extern  ] Froms (file share/libc/math.h, line 334)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 342)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 345)
             assigns __fc_errno \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 342)
+[ Extern  ] Froms for 'domain_error' (file share/libc/math.h, line 345)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 338)
+[ Extern  ] Froms for 'infinite' (file share/libc/math.h, line 341)
             assigns \result \from x;
             Unverifiable but considered Valid.
-[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 334)
+[ Extern  ] Froms for 'normal' (file share/libc/math.h, line 337)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3019,7 +3019,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 370)
+[ Extern  ] Froms (file share/libc/math.h, line 373)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3039,7 +3039,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 378)
+[ Extern  ] Froms (file share/libc/math.h, line 381)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3056,7 +3056,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 408)
+[ Extern  ] Froms (file share/libc/math.h, line 411)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3073,7 +3073,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 415)
+[ Extern  ] Froms (file share/libc/math.h, line 418)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3090,7 +3090,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 422)
+[ Extern  ] Froms (file share/libc/math.h, line 425)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3107,7 +3107,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 429)
+[ Extern  ] Froms (file share/libc/math.h, line 432)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3124,7 +3124,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 436)
+[ Extern  ] Froms (file share/libc/math.h, line 439)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3141,7 +3141,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 443)
+[ Extern  ] Froms (file share/libc/math.h, line 446)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3158,7 +3158,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 454)
+[ Extern  ] Froms (file share/libc/math.h, line 457)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3175,7 +3175,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 461)
+[ Extern  ] Froms (file share/libc/math.h, line 464)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3192,7 +3192,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 468)
+[ Extern  ] Froms (file share/libc/math.h, line 471)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3217,7 +3217,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 494)
+[ Extern  ] Froms (file share/libc/math.h, line 497)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3242,7 +3242,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 502)
+[ Extern  ] Froms (file share/libc/math.h, line 505)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3267,7 +3267,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 510)
+[ Extern  ] Froms (file share/libc/math.h, line 513)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3284,7 +3284,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 523)
+[ Extern  ] Froms (file share/libc/math.h, line 526)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3301,7 +3301,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 533)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3330,7 +3330,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 539)
+[ Extern  ] Froms (file share/libc/math.h, line 542)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3353,7 +3353,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 548)
+[ Extern  ] Froms (file share/libc/math.h, line 551)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3373,7 +3373,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 557)
+[ Extern  ] Froms (file share/libc/math.h, line 560)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3390,7 +3390,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 580)
+[ Extern  ] Froms (file share/libc/math.h, line 583)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3407,7 +3407,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 586)
+[ Extern  ] Froms (file share/libc/math.h, line 589)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3424,7 +3424,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 593)
+[ Extern  ] Froms (file share/libc/math.h, line 596)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3441,7 +3441,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 599)
+[ Extern  ] Froms (file share/libc/math.h, line 602)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3458,7 +3458,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 605)
+[ Extern  ] Froms (file share/libc/math.h, line 608)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3475,7 +3475,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 611)
+[ Extern  ] Froms (file share/libc/math.h, line 614)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3492,7 +3492,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 633)
+[ Extern  ] Froms (file share/libc/math.h, line 636)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3509,7 +3509,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 639)
+[ Extern  ] Froms (file share/libc/math.h, line 642)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3526,7 +3526,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 645)
+[ Extern  ] Froms (file share/libc/math.h, line 648)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3543,7 +3543,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 659)
+[ Extern  ] Froms (file share/libc/math.h, line 662)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3560,7 +3560,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 665)
+[ Extern  ] Froms (file share/libc/math.h, line 668)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3577,7 +3577,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 671)
+[ Extern  ] Froms (file share/libc/math.h, line 674)
             assigns \result \from x;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3594,7 +3594,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 678)
+[ Extern  ] Froms (file share/libc/math.h, line 681)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3611,7 +3611,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 685)
+[ Extern  ] Froms (file share/libc/math.h, line 688)
             assigns \result \from x, y;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3628,7 +3628,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 706)
+[ Extern  ] Froms (file share/libc/math.h, line 709)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3645,7 +3645,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 713)
+[ Extern  ] Froms (file share/libc/math.h, line 716)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3662,7 +3662,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 720)
+[ Extern  ] Froms (file share/libc/math.h, line 723)
             assigns \result \from (indirect: *(tagp + (0 ..)));
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3679,7 +3679,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 768)
+[ Extern  ] Froms (file share/libc/math.h, line 771)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
@@ -3696,7 +3696,7 @@
 [ Extern  ] Assigns nothing
             assigns \nothing;
             Unverifiable but considered Valid.
-[ Extern  ] Froms (file share/libc/math.h, line 774)
+[ Extern  ] Froms (file share/libc/math.h, line 777)
             assigns \result \from \nothing;
             Unverifiable but considered Valid.
 [  Valid  ] Default behavior
diff --git a/tests/libc/math_h.c b/tests/libc/math_h.c
index 06901268917023b9fc57f8a3872708c8836455ef..95ded2bf103805d967ffae4a1525e5a4bc828ae6 100644
--- a/tests/libc/math_h.c
+++ b/tests/libc/math_h.c
@@ -1,5 +1,7 @@
+/* run.config
+   STDOPT: #"-warn-special-float none" #"-cpp-extra-args=\"-DNONFINITE\""
+*/
 #include <math.h>
-
 const double pi = 3.14159265358979323846264338327950288;
 const double half_pi = 1.57079632679489661923132169163975144;
 const double e = 2.718281828459045090795598298427648842334747314453125;
@@ -17,6 +19,14 @@ const double minus_zero = -0.0;
 const double one = 1.0;
 const double minus_one = -1.0;
 const double large = 1e38;
+#ifdef NONFINITE
+const double huge_val = HUGE_VAL;
+const float huge_valf = HUGE_VALF;
+const long double huge_vall = HUGE_VALL;
+#endif
+const float infinity = INFINITY;
+const double fp_ilogb0 = FP_ILOGB0;
+const double fp_ilogbnan = FP_ILOGBNAN;
 
 #define TEST_VAL(type,f,c) type f##_##c = f(c)
 
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
index 3e49cb57de38e81d730fc90e4c4e8b1155f152ec..cf2aaaa418c7a222f1075e5c20d0b5d874d4c60a 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -1,5 +1,5 @@
 [kernel] Parsing tests/libc/math_h.c (with preprocessing)
-[kernel:parser:decimal-float] tests/libc/math_h.c:3: Warning: 
+[kernel:parser:decimal-float] tests/libc/math_h.c:5: 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
@@ -23,292 +23,286 @@
   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.}
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
+  Called from tests/libc/math_h.c:45.
 [eva] using specification for function atan
-[eva] tests/libc/math_h.c:35: 
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
+  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
+  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
+  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
+  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
+  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
+  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
+  Called from tests/libc/math_h.c:45.
+[eva] tests/libc/math_h.c:45: 
   function atan: precondition 'finite_arg' got status valid.
 [eva] Done for function atan
-[eva:alarm] tests/libc/math_h.c:35: Warning: 
-  non-finite double value. assert \is_finite(top);
 [eva] computing for function atan <- main.
-  Called from tests/libc/math_h.c:35.
-[eva] tests/libc/math_h.c:35: 
-  function atan: precondition 'finite_arg' got status valid.
+  Called from tests/libc/math_h.c:45.
+[eva:alarm] tests/libc/math_h.c:45: Warning: 
+  function atan: precondition 'finite_arg' got status unknown.
 [eva] Done for function atan
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
+  Called from tests/libc/math_h.c:46.
 [eva] using specification for function atanf
-[eva] tests/libc/math_h.c:36: 
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
+  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
+  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
+  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
+  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
+  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
+  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
+  Called from tests/libc/math_h.c:46.
+[eva] tests/libc/math_h.c:46: 
   function atanf: precondition 'finite_arg' got status valid.
 [eva] Done for function atanf
-[eva:alarm] tests/libc/math_h.c:36: Warning: 
-  non-finite float value. assert \is_finite(f_top);
 [eva] computing for function atanf <- main.
-  Called from tests/libc/math_h.c:36.
-[eva] tests/libc/math_h.c:36: 
-  function atanf: precondition 'finite_arg' got status valid.
+  Called from tests/libc/math_h.c:46.
+[eva:alarm] tests/libc/math_h.c:46: Warning: 
+  function atanf: precondition 'finite_arg' got status unknown.
 [eva] Done for function atanf
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
+  Called from tests/libc/math_h.c:47.
 [eva] using specification for function atanl
-[eva] tests/libc/math_h.c:37: 
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva] tests/libc/math_h.c:37: 
+  Called from tests/libc/math_h.c:47.
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva] tests/libc/math_h.c:37: 
+  Called from tests/libc/math_h.c:47.
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva] tests/libc/math_h.c:37: 
+  Called from tests/libc/math_h.c:47.
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva] tests/libc/math_h.c:37: 
+  Called from tests/libc/math_h.c:47.
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva] tests/libc/math_h.c:37: 
+  Called from tests/libc/math_h.c:47.
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva] tests/libc/math_h.c:37: 
+  Called from tests/libc/math_h.c:47.
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva] tests/libc/math_h.c:37: 
+  Called from tests/libc/math_h.c:47.
+[eva] tests/libc/math_h.c:47: 
   function atanl: precondition 'finite_arg' got status valid.
 [eva] Done for function atanl
-[eva:alarm] tests/libc/math_h.c:37: Warning: 
-  non-finite long double value. assert \is_finite(ld_top);
 [eva] computing for function atanl <- main.
-  Called from tests/libc/math_h.c:37.
-[eva:alarm] tests/libc/math_h.c:37: Warning: 
+  Called from tests/libc/math_h.c:47.
+[eva:alarm] tests/libc/math_h.c:47: Warning: 
   function atanl: precondition 'finite_arg' got status unknown.
 [eva] Done for function atanl
 [eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:38.
+  Called from tests/libc/math_h.c:48.
 [eva] using specification for function fabs
-[eva] tests/libc/math_h.c:38: 
+[eva] tests/libc/math_h.c:48: 
   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:38.
-[eva] tests/libc/math_h.c:38: 
+  Called from tests/libc/math_h.c:48.
+[eva] tests/libc/math_h.c:48: 
   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:38.
-[eva] tests/libc/math_h.c:38: 
+  Called from tests/libc/math_h.c:48.
+[eva] tests/libc/math_h.c:48: 
   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:38.
-[eva] tests/libc/math_h.c:38: 
+  Called from tests/libc/math_h.c:48.
+[eva] tests/libc/math_h.c:48: 
   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:38.
-[eva] tests/libc/math_h.c:38: 
+  Called from tests/libc/math_h.c:48.
+[eva] tests/libc/math_h.c:48: 
   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:38.
-[eva] tests/libc/math_h.c:38: 
+  Called from tests/libc/math_h.c:48.
+[eva] tests/libc/math_h.c:48: 
   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:38.
-[eva] tests/libc/math_h.c:38: 
+  Called from tests/libc/math_h.c:48.
+[eva] tests/libc/math_h.c:48: 
   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:38.
-[eva] tests/libc/math_h.c:38: 
+  Called from tests/libc/math_h.c:48.
+[eva] tests/libc/math_h.c:48: 
   function fabs: precondition 'finite_arg' got status valid.
 [eva] Done for function fabs
-[eva:alarm] tests/libc/math_h.c:38: Warning: 
-  non-finite double value. assert \is_finite(top);
 [eva] computing for function fabs <- main.
-  Called from tests/libc/math_h.c:38.
-[eva] tests/libc/math_h.c:38: 
-  function fabs: precondition 'finite_arg' got status valid.
+  Called from tests/libc/math_h.c:48.
+[eva:alarm] tests/libc/math_h.c:48: Warning: 
+  function fabs: precondition 'finite_arg' got status unknown.
 [eva] Done for function fabs
 [eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:39.
+  Called from tests/libc/math_h.c:49.
 [eva] using specification for function fabsf
-[eva] tests/libc/math_h.c:39: 
+[eva] tests/libc/math_h.c:49: 
   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:39.
-[eva] tests/libc/math_h.c:39: 
+  Called from tests/libc/math_h.c:49.
+[eva] tests/libc/math_h.c:49: 
   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:39.
-[eva] tests/libc/math_h.c:39: 
+  Called from tests/libc/math_h.c:49.
+[eva] tests/libc/math_h.c:49: 
   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:39.
-[eva] tests/libc/math_h.c:39: 
+  Called from tests/libc/math_h.c:49.
+[eva] tests/libc/math_h.c:49: 
   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:39.
-[eva] tests/libc/math_h.c:39: 
+  Called from tests/libc/math_h.c:49.
+[eva] tests/libc/math_h.c:49: 
   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:39.
-[eva] tests/libc/math_h.c:39: 
+  Called from tests/libc/math_h.c:49.
+[eva] tests/libc/math_h.c:49: 
   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:39.
-[eva] tests/libc/math_h.c:39: 
+  Called from tests/libc/math_h.c:49.
+[eva] tests/libc/math_h.c:49: 
   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:39.
-[eva] tests/libc/math_h.c:39: 
+  Called from tests/libc/math_h.c:49.
+[eva] tests/libc/math_h.c:49: 
   function fabsf: precondition 'finite_arg' got status valid.
 [eva] Done for function fabsf
-[eva:alarm] tests/libc/math_h.c:39: Warning: 
-  non-finite float value. assert \is_finite(f_top);
 [eva] computing for function fabsf <- main.
-  Called from tests/libc/math_h.c:39.
-[eva] tests/libc/math_h.c:39: 
-  function fabsf: precondition 'finite_arg' got status valid.
+  Called from tests/libc/math_h.c:49.
+[eva:alarm] tests/libc/math_h.c:49: Warning: 
+  function fabsf: precondition 'finite_arg' got status unknown.
 [eva] Done for function fabsf
 [eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:40.
+  Called from tests/libc/math_h.c:50.
 [eva] using specification for function fabsl
-[eva] tests/libc/math_h.c:40: 
+[eva] tests/libc/math_h.c:50: 
   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:40.
-[eva] tests/libc/math_h.c:40: 
+  Called from tests/libc/math_h.c:50.
+[eva] tests/libc/math_h.c:50: 
   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:40.
-[eva] tests/libc/math_h.c:40: 
+  Called from tests/libc/math_h.c:50.
+[eva] tests/libc/math_h.c:50: 
   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:40.
-[eva] tests/libc/math_h.c:40: 
+  Called from tests/libc/math_h.c:50.
+[eva] tests/libc/math_h.c:50: 
   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:40.
-[eva] tests/libc/math_h.c:40: 
+  Called from tests/libc/math_h.c:50.
+[eva] tests/libc/math_h.c:50: 
   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:40.
-[eva] tests/libc/math_h.c:40: 
+  Called from tests/libc/math_h.c:50.
+[eva] tests/libc/math_h.c:50: 
   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:40.
-[eva] tests/libc/math_h.c:40: 
+  Called from tests/libc/math_h.c:50.
+[eva] tests/libc/math_h.c:50: 
   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:40.
-[eva] tests/libc/math_h.c:40: 
+  Called from tests/libc/math_h.c:50.
+[eva] tests/libc/math_h.c:50: 
   function fabsl: precondition 'finite_arg' got status valid.
 [eva] Done for function fabsl
-[eva:alarm] tests/libc/math_h.c:40: Warning: 
-  non-finite long double value. assert \is_finite(ld_top);
 [eva] computing for function fabsl <- main.
-  Called from tests/libc/math_h.c:40.
-[eva:alarm] tests/libc/math_h.c:40: Warning: 
+  Called from tests/libc/math_h.c:50.
+[eva:alarm] tests/libc/math_h.c:50: Warning: 
   function fabsl: precondition 'finite_arg' got status unknown.
 [eva] Done for function fabsl
 [eva] Recording results for main