From 9822b8ae323d96bf0256c12d2a9034f8ce2e305a Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Tue, 15 Dec 2020 10:07:30 +0100
Subject: [PATCH] [Libc] add specs for __finite and __finitef
---
share/libc/math.h | 22 ++++++++
tests/idct/oracle/ieee_1180_1990.res.oracle | 62 +++++++++++++++++++--
tests/libc/math_h.c | 18 +++++-
tests/libc/oracle/fc_libc.1.res.oracle | 28 ++++++++++
tests/libc/oracle/math_h.res.oracle | 36 ++++++++++++
5 files changed, 160 insertions(+), 6 deletions(-)
diff --git a/share/libc/math.h b/share/libc/math.h
index 750ce95085e..10229ad2ec8 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 ee5c88ae7ff..6be9aa23457 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 1f732635d76..b88b6129858 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 2b6422a8dd9..f0d19dd5efc 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 5c82e6d5554..fa3503020a0 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}
--
GitLab