diff --git a/share/libc/math.h b/share/libc/math.h
index ad38d9f68cd5cd254ea592173b18e38b6cffed3f..c2d52a34583abaf8f755901ca0563625092cb106 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -467,7 +467,7 @@ extern float sinf(float x);
*/
extern long double sinl(long double x);
-/* Note: the specs of tan/tanf/tanl below assume that, for a finite x,
+/* Note: the specs of tan/tanf below assume that, for a finite x,
* the result is always finite. This is _not_ guaranteed by the standard,
* but testing with the GNU libc, plus some mathematical arguments
* (see https://stackoverflow.com/questions/67482420) indicate that,
@@ -527,26 +527,7 @@ extern float tanf(float x);
/*@
assigns errno, \result \from x;
- behavior zero:
- assumes zero_arg: \is_finite(x) && x == 0.;
- assigns \result \from x;
- ensures zero_res: \is_finite(\result) && \result == x;
- ensures no_error: errno == \old(errno);
- behavior finite_non_zero:
- assumes finite_arg: \is_finite(x) && x != 0.;
- ensures finite_result: \is_finite(\result);
- ensures maybe_error: errno == \old(errno) || errno == ERANGE;
- behavior infinity:
- assumes infinite_arg: \is_infinite(x);
- ensures nan_result: \is_NaN(\result);
- ensures errno_set: errno == EDOM;
- behavior nan:
- assumes nan_arg: \is_NaN(x);
- assigns \result \from x;
- ensures nan_result: \is_NaN(\result);
- ensures no_error: errno == \old(errno);
- complete behaviors;
- disjoint behaviors;
+ ensures maybe_error: errno == \old(errno) || errno == EDOM || errno == ERANGE;
*/
extern long double tanl(long double x);
diff --git a/src/plugins/report/tests/report/oracle/csv.csv b/src/plugins/report/tests/report/oracle/csv.csv
index 45b8af5a1ea51d44df8e8796399002b6ff76ae2f..e4dc4df6f00008cade09bda50ddf0b94122d3d92 100644
--- a/src/plugins/report/tests/report/oracle/csv.csv
+++ b/src/plugins/report/tests/report/oracle/csv.csv
@@ -1,5 +1,5 @@
directory file line function property kind status property
-FRAMAC_SHARE/libc math.h 1226 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
+FRAMAC_SHARE/libc math.h 1207 pow precondition Unknown finite_logic_res: \is_finite(pow(x, y))
tests/report csv.c 11 main1 signed_overflow Unknown -2147483648 ≤ x * x
tests/report csv.c 11 main1 signed_overflow Unknown x * x ≤ 2147483647
tests/report csv.c 12 main1 index_bound Unknown 0 ≤ x
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 869dfb38a97c2c90cdd70c2e28efc7714afde126..eb9d1531fcfbd9c001b76a9946ccc398d95d516e 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2897,44 +2897,24 @@
--- 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' 'finite_result'
- ensures finite_result: \is_finite(\result)
- Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'finite_non_zero' 'maybe_error'
+[ Extern ] Post-condition 'maybe_error'
ensures
maybe_error:
- __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 33 ∨
+ __fc_errno ≡ 34
Unverifiable but considered Valid.
[ Extern ] Assigns (file share/libc/math.h, line 529)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'zero' nothing
- assigns \nothing;
- Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 529)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
[ Extern ] Froms (file share/libc/math.h, line 529)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'zero' (file share/libc/math.h, line 532)
- 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'
@@ -2949,7 +2929,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 538)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2969,7 +2949,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 583)
+[ Extern ] Froms (file share/libc/math.h, line 564)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -2989,7 +2969,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 609)
+[ Extern ] Froms (file share/libc/math.h, line 590)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3021,7 +3001,7 @@
[ Extern ] Post-condition for 'minus_infinity' 'no_error'
ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 652)
+[ Extern ] Assigns (file share/libc/math.h, line 633)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'minus_infinity' nothing
@@ -3030,16 +3010,16 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 652)
+[ Extern ] Froms (file share/libc/math.h, line 633)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 652)
+[ Extern ] Froms (file share/libc/math.h, line 633)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 675)
+[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 656)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 656)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 637)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3080,7 +3060,7 @@
[ Extern ] Post-condition for 'minus_infinity' 'no_error'
ensures no_error: __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 689)
+[ Extern ] Assigns (file share/libc/math.h, line 670)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
[ Extern ] Assigns for 'minus_infinity' nothing
@@ -3089,16 +3069,16 @@
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 689)
+[ Extern ] Froms (file share/libc/math.h, line 670)
assigns __fc_errno \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 689)
+[ Extern ] Froms (file share/libc/math.h, line 670)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 712)
+[ Extern ] Froms for 'minus_infinity' (file share/libc/math.h, line 693)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'normal' (file share/libc/math.h, line 693)
+[ Extern ] Froms for 'normal' (file share/libc/math.h, line 674)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3139,13 +3119,13 @@
[ Extern ] Post-condition for 'zero' 'zero_exp'
ensures zero_exp: *\old(exp) ≡ 0
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 737)
+[ Extern ] Assigns (file share/libc/math.h, line 718)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 737)
+[ Extern ] Froms (file share/libc/math.h, line 718)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 737)
+[ Extern ] Froms (file share/libc/math.h, line 718)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3183,13 +3163,13 @@
[ Extern ] Post-condition for 'zero' 'zero_exp'
ensures zero_exp: *\old(exp) ≡ 0
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 764)
+[ Extern ] Assigns (file share/libc/math.h, line 745)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 764)
+[ Extern ] Froms (file share/libc/math.h, line 745)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 764)
+[ Extern ] Froms (file share/libc/math.h, line 745)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3227,13 +3207,13 @@
[ Extern ] Post-condition for 'zero' 'zero_exp'
ensures zero_exp: *\old(exp) ≡ 0
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 791)
+[ Extern ] Assigns (file share/libc/math.h, line 772)
assigns \result, *exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 791)
+[ Extern ] Froms (file share/libc/math.h, line 772)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 791)
+[ Extern ] Froms (file share/libc/math.h, line 772)
assigns *exp \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3257,13 +3237,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 821)
+[ Extern ] Assigns (file share/libc/math.h, line 802)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 821)
+[ Extern ] Froms (file share/libc/math.h, line 802)
assigns __fc_errno \from x, exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 821)
+[ Extern ] Froms (file share/libc/math.h, line 802)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3281,13 +3261,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 841)
+[ Extern ] Assigns (file share/libc/math.h, line 822)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 841)
+[ Extern ] Froms (file share/libc/math.h, line 822)
assigns __fc_errno \from x, exp;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 841)
+[ Extern ] Froms (file share/libc/math.h, line 822)
assigns \result \from x, exp;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3307,7 +3287,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 867)
+[ Extern ] Froms (file share/libc/math.h, line 848)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3327,7 +3307,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 898)
+[ Extern ] Froms (file share/libc/math.h, line 879)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3347,7 +3327,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 929)
+[ Extern ] Froms (file share/libc/math.h, line 910)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3367,7 +3347,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 960)
+[ Extern ] Froms (file share/libc/math.h, line 941)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3387,7 +3367,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 991)
+[ Extern ] Froms (file share/libc/math.h, line 972)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3407,7 +3387,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1022)
+[ Extern ] Froms (file share/libc/math.h, line 1003)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3427,7 +3407,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1057)
+[ Extern ] Froms (file share/libc/math.h, line 1038)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3447,7 +3427,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1088)
+[ Extern ] Froms (file share/libc/math.h, line 1069)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3467,7 +3447,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1119)
+[ Extern ] Froms (file share/libc/math.h, line 1100)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3492,7 +3472,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1166)
+[ Extern ] Froms (file share/libc/math.h, line 1147)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3517,7 +3497,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1184)
+[ Extern ] Froms (file share/libc/math.h, line 1165)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3542,7 +3522,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1202)
+[ Extern ] Froms (file share/libc/math.h, line 1183)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3560,13 +3540,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 1224)
+[ Extern ] Assigns (file share/libc/math.h, line 1205)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1224)
+[ Extern ] Froms (file share/libc/math.h, line 1205)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1224)
+[ Extern ] Froms (file share/libc/math.h, line 1205)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3584,13 +3564,13 @@
ensures
__fc_errno: __fc_errno ≡ 34 ∨ __fc_errno ≡ \old(__fc_errno)
Unverifiable but considered Valid.
-[ Extern ] Assigns (file share/libc/math.h, line 1239)
+[ Extern ] Assigns (file share/libc/math.h, line 1220)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1239)
+[ Extern ] Froms (file share/libc/math.h, line 1220)
assigns __fc_errno \from x, y;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1239)
+[ Extern ] Froms (file share/libc/math.h, line 1220)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3622,7 +3602,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1260)
+[ Extern ] Froms (file share/libc/math.h, line 1241)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3648,7 +3628,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1289)
+[ Extern ] Froms (file share/libc/math.h, line 1270)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3671,7 +3651,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1318)
+[ Extern ] Froms (file share/libc/math.h, line 1299)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3688,7 +3668,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1358)
+[ Extern ] Froms (file share/libc/math.h, line 1339)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3705,7 +3685,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1375)
+[ Extern ] Froms (file share/libc/math.h, line 1356)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3722,7 +3702,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1392)
+[ Extern ] Froms (file share/libc/math.h, line 1373)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3739,7 +3719,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1409)
+[ Extern ] Froms (file share/libc/math.h, line 1390)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3756,7 +3736,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1426)
+[ Extern ] Froms (file share/libc/math.h, line 1407)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3773,7 +3753,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1443)
+[ Extern ] Froms (file share/libc/math.h, line 1424)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3790,7 +3770,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1476)
+[ Extern ] Froms (file share/libc/math.h, line 1457)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3807,7 +3787,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1493)
+[ Extern ] Froms (file share/libc/math.h, line 1474)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3824,7 +3804,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 1491)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3841,7 +3821,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1535)
+[ Extern ] Froms (file share/libc/math.h, line 1516)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3858,7 +3838,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1552)
+[ Extern ] Froms (file share/libc/math.h, line 1533)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3875,7 +3855,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1569)
+[ Extern ] Froms (file share/libc/math.h, line 1550)
assigns \result \from x;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3895,7 +3875,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1589)
+[ Extern ] Froms (file share/libc/math.h, line 1570)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3915,7 +3895,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1610)
+[ Extern ] Froms (file share/libc/math.h, line 1591)
assigns \result \from x, y;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3932,7 +3912,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1643)
+[ Extern ] Froms (file share/libc/math.h, line 1624)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3949,7 +3929,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1650)
+[ Extern ] Froms (file share/libc/math.h, line 1631)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3966,7 +3946,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1657)
+[ Extern ] Froms (file share/libc/math.h, line 1638)
assigns \result \from (indirect: *(tagp + (0 ..)));
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3986,7 +3966,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1687)
+[ Extern ] Froms (file share/libc/math.h, line 1668)
assigns \result \from f;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4012,7 +3992,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1700)
+[ Extern ] Froms (file share/libc/math.h, line 1681)
assigns \result \from d;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4035,7 +4015,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1727)
+[ Extern ] Froms (file share/libc/math.h, line 1708)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4052,7 +4032,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 1733)
+[ Extern ] Froms (file share/libc/math.h, line 1714)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -4414,9 +4394,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 193 Completely validated
+ 191 Completely validated
16 Locally validated
- 561 Considered valid
+ 556 Considered valid
56 To be validated
- 826 Total
+ 819 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index bf59c3d6baf304214026d562278211f402a72106..cb12a8c02f4c6735f093d2531f5b348a18e673c2 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3806,27 +3806,13 @@ extern double tan(double x);
*/
extern float tanf(float x);
-/*@ requires ¬(infinite_arg: \is_infinite(x));
- requires ¬(nan_arg: \is_NaN(x));
+/*@ ensures
+ maybe_error:
+ __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 33 ∨
+ __fc_errno ≡ 34;
assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
-
- behavior zero:
- assumes zero_arg: \is_finite(x) ∧ x ≡ 0.;
- ensures zero_res: \is_finite(\result) ∧ \result ≡ \old(x);
- ensures no_error: __fc_errno ≡ \old(__fc_errno);
- assigns \result;
- assigns \result \from x;
-
- behavior finite_non_zero:
- assumes finite_arg: \is_finite(x) ∧ x ≢ 0.;
- ensures finite_result: \is_finite(\result);
- ensures
- maybe_error: __fc_errno ≡ \old(__fc_errno) ∨ __fc_errno ≡ 34;
-
- complete behaviors finite_non_zero, zero;
- disjoint behaviors finite_non_zero, zero;
*/
extern long double tanl(long double x);
diff --git a/tests/libc/oracle/math_h.1.res.oracle b/tests/libc/oracle/math_h.1.res.oracle
index 7b044ea68c6299473004aae7f4040ab276e96016..39d3fa1f6ccd2cbf00633eb8fd81f53a21d85c5a 100644
--- a/tests/libc/oracle/math_h.1.res.oracle
+++ b/tests/libc/oracle/math_h.1.res.oracle
@@ -434,68 +434,32 @@
[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.
@@ -527,17 +491,9 @@
[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.
diff --git a/tests/libc/oracle/math_h.2.res.oracle b/tests/libc/oracle/math_h.2.res.oracle
index 2c5443e6086f72eadb95e0f251ae0cb3be6906b3..886f7eb4b1161f9d02d92c3e554d8d4b35032e5c 100644
--- a/tests/libc/oracle/math_h.2.res.oracle
+++ b/tests/libc/oracle/math_h.2.res.oracle
@@ -408,68 +408,32 @@
[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.