diff --git a/share/libc/math.h b/share/libc/math.h
index 750ce95085e5b7d9bd78df21e884213802f579eb..10229ad2ec85d98a834f04d16d6f01f5bc7e3046 100644
--- a/share/libc/math.h
+++ b/share/libc/math.h
@@ -702,8 +702,30 @@ extern double fma(double x, double y, double z);
extern float fmaf(float x, float y, float z);
extern long double fmal(long double x, long double y, long double z);
+/*@
+ assigns \result \from f;
+ behavior finite:
+ assumes isfinite_f: \is_finite(f);
+ ensures nonzero_result: \result > 0 || \result < 0;
+ behavior nonfinite:
+ assumes nonfinite_f: !\is_finite(f);
+ ensures zero_result: \result == 0;
+ complete behaviors;
+ disjoint behaviors;
+*/
extern int __finitef(float f);
+/*@
+ assigns \result \from d;
+ behavior finite:
+ assumes isfinite_d: \is_finite(d);
+ ensures nonzero_result: \result > 0 || \result < 0;
+ behavior nonfinite:
+ assumes nonfinite_d: !\is_finite(d);
+ ensures zero_result: \result == 0;
+ complete behaviors;
+ disjoint behaviors;
+*/
extern int __finite(double d);
# define isfinite(x) \
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index ee5c88ae7ff10e6c5521fff4e848a3745f07d258..6be9aa2345755e88b527f989d55cdacf4734fe1a 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -3561,6 +3561,58 @@
default behavior
by Frama-C kernel.
+--------------------------------------------------------------------------------
+--- Properties of Function '__finitef'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition for 'finite' 'nonzero_result'
+ ensures nonzero_result: \result > 0 ∨ \result < 0
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'nonfinite' 'zero_result'
+ ensures zero_result: \result ≡ 0
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 706)
+ assigns \result \from f;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Valid ] Behavior 'finite'
+ behavior finite
+ by Frama-C kernel.
+[ Valid ] Behavior 'nonfinite'
+ behavior nonfinite
+ by Frama-C kernel.
+
+--------------------------------------------------------------------------------
+--- Properties of Function '__finite'
+--------------------------------------------------------------------------------
+
+[ Extern ] Post-condition for 'finite' 'nonzero_result'
+ ensures nonzero_result: \result > 0 ∨ \result < 0
+ Unverifiable but considered Valid.
+[ Extern ] Post-condition for 'nonfinite' 'zero_result'
+ ensures zero_result: \result ≡ 0
+ Unverifiable but considered Valid.
+[ Extern ] Assigns nothing
+ assigns \nothing;
+ Unverifiable but considered Valid.
+[ Extern ] Froms (file share/libc/math.h, line 719)
+ assigns \result \from d;
+ Unverifiable but considered Valid.
+[ Valid ] Default behavior
+ default behavior
+ by Frama-C kernel.
+[ Valid ] Behavior 'finite'
+ behavior finite
+ by Frama-C kernel.
+[ Valid ] Behavior 'nonfinite'
+ behavior nonfinite
+ by Frama-C kernel.
+
--------------------------------------------------------------------------------
--- Properties of Function '__fc_infinity'
--------------------------------------------------------------------------------
@@ -3571,7 +3623,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 724)
+[ Extern ] Froms (file share/libc/math.h, line 746)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3588,7 +3640,7 @@
[ Extern ] Assigns nothing
assigns \nothing;
Unverifiable but considered Valid.
-[ Extern ] Froms (file share/libc/math.h, line 730)
+[ Extern ] Froms (file share/libc/math.h, line 752)
assigns \result \from \nothing;
Unverifiable but considered Valid.
[ Valid ] Default behavior
@@ -3950,9 +4002,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 169 Completely validated
+ 175 Completely validated
16 Locally validated
- 454 Considered valid
+ 462 Considered valid
56 To be validated
- 695 Total
+ 709 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/math_h.c b/tests/libc/math_h.c
index 1f732635d7643caa9b9bb02bdaae0d3950fbcff7..b88b61298587fe81bc0644190254c9237d4625d7 100644
--- a/tests/libc/math_h.c
+++ b/tests/libc/math_h.c
@@ -1,6 +1,6 @@
/* run.config
FILTER: sed -E -e '/atanf_/ s/([0-9][.][0-9]{6})[0-9]+/\1/g'
- STDOPT: #"-warn-special-float none" #"-cpp-extra-args=\"-DNONFINITE\""
+ STDOPT: #"-warn-special-float none" #"-cpp-extra-args=\"-DNONFINITE\"" #"-eva-slevel 4"
*/
#include <math.h>
const double pi = 3.14159265358979323846264338327950288;
@@ -48,4 +48,20 @@ int main() {
TEST_FUN(double,fabs,);
TEST_FUN(float,fabsf,f_);
TEST_FUN(long double,fabsl,ld_);
+
+#ifdef NONFINITE
+ int r;
+ r = isfinite(pi);
+ //@ assert r;
+ r = isfinite(large);
+ //@ assert r;
+ r = isfinite(0.0f);
+ //@ assert r;
+ r = isfinite(huge_val);
+ //@ assert !r;
+ r = isfinite(-INFINITY);
+ //@ assert !r;
+ r = isfinite(NAN);
+ //@ assert !r;
+#endif
}
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index 2b6422a8dd9ebfe3f4136ae9baa2db02e35c505e..f0d19dd5efcdf4900a7f4d174aa4463e22c395df 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -3390,6 +3390,20 @@ float fabsf(float x)
return_label: return __retres;
}
+/*@ assigns \result;
+ assigns \result \from f;
+
+ behavior finite:
+ assumes isfinite_f: \is_finite(f);
+ ensures nonzero_result: \result > 0 ∨ \result < 0;
+
+ behavior nonfinite:
+ assumes nonfinite_f: ¬\is_finite(f);
+ ensures zero_result: \result ≡ 0;
+
+ complete behaviors nonfinite, finite;
+ disjoint behaviors nonfinite, finite;
+ */
int __finitef(float f)
{
int __retres;
@@ -3402,6 +3416,20 @@ int __finitef(float f)
return __retres;
}
+/*@ assigns \result;
+ assigns \result \from d;
+
+ behavior finite:
+ assumes isfinite_d: \is_finite(d);
+ ensures nonzero_result: \result > 0 ∨ \result < 0;
+
+ behavior nonfinite:
+ assumes nonfinite_d: ¬\is_finite(d);
+ ensures zero_result: \result ≡ 0;
+
+ complete behaviors nonfinite, finite;
+ disjoint behaviors nonfinite, finite;
+ */
int __finite(double d)
{
int __retres;
diff --git a/tests/libc/oracle/math_h.res.oracle b/tests/libc/oracle/math_h.res.oracle
index 5c82e6d555400766e3b3344eb6978de25494ce5f..fa3503020a02b12db820f3c973b3e78ca640f169 100644
--- a/tests/libc/oracle/math_h.res.oracle
+++ b/tests/libc/oracle/math_h.res.oracle
@@ -267,6 +267,41 @@
[eva:alarm] tests/libc/math_h.c:50: Warning:
function fabsl: precondition 'finite_arg' got status unknown.
[eva] Done for function fabsl
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:54.
+[eva] using specification for function __finite
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:55: assertion got status valid.
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:56.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:56.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:57: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:58.
+[eva] using specification for function __finitef
+[eva] Done for function __finitef
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:58.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:59: assertion got status valid.
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:60.
+[eva] Done for function __finite
+[eva] computing for function __finite <- main.
+ Called from tests/libc/math_h.c:60.
+[eva] Done for function __finite
+[eva] tests/libc/math_h.c:61: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:62.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:63: assertion got status valid.
+[eva] computing for function __finitef <- main.
+ Called from tests/libc/math_h.c:64.
+[eva] Done for function __finitef
+[eva] tests/libc/math_h.c:65: assertion got status valid.
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -325,4 +360,5 @@
fabsl_minus_one ∈ [-inf .. inf]
fabsl_large ∈ [-inf .. inf]
fabsl_ld_top ∈ [-inf .. inf]
+ r ∈ {0}
__retres ∈ {0}