diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 02d4b53e0b88d1de3344dd38408a5e06a4b952bc..58fa3ec2dd566b8edb5a0745e91e3fe96a06b09d 100644
--- a/tests/idct/oracle/ieee_1180_1990.res.oracle
+++ b/tests/idct/oracle/ieee_1180_1990.res.oracle
@@ -2737,9 +2737,6 @@
[ Extern ] Post-condition for 'normal' 'positive_result'
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'infinite' 'result_plus_infinity'
- ensures result_plus_infinity: \is_plus_infinity(\result)
- Unverifiable but considered Valid.
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
@@ -2749,9 +2746,6 @@
[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 262)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'infinite' nothing
- assigns \nothing;
- Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
@@ -2767,9 +2761,6 @@
[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 262)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 258)
- assigns \result \from x;
- Unverifiable but considered Valid.
[ Extern ] Froms for 'normal' (file share/libc/math.h, line 254)
assigns \result \from x;
Unverifiable but considered Valid.
@@ -2779,9 +2770,6 @@
[ Valid ] Behavior 'domain_error'
behavior domain_error
by Frama-C kernel.
-[ Valid ] Behavior 'infinite'
- behavior infinite
- by Frama-C kernel.
[ Valid ] Behavior 'normal'
behavior normal
by Frama-C kernel.
@@ -2793,9 +2781,6 @@
[ Extern ] Post-condition for 'normal' 'positive_result'
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'infinite' 'result_plus_infinity'
- ensures result_plus_infinity: \is_plus_infinity(\result)
- Unverifiable but considered Valid.
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
@@ -2805,9 +2790,6 @@
[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 280)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'infinite' nothing
- assigns \nothing;
- Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
@@ -2823,9 +2805,6 @@
[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 280)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 276)
- assigns \result \from x;
- Unverifiable but considered Valid.
[ Extern ] Froms for 'normal' (file share/libc/math.h, line 272)
assigns \result \from x;
Unverifiable but considered Valid.
@@ -2835,9 +2814,6 @@
[ Valid ] Behavior 'domain_error'
behavior domain_error
by Frama-C kernel.
-[ Valid ] Behavior 'infinite'
- behavior infinite
- by Frama-C kernel.
[ Valid ] Behavior 'normal'
behavior normal
by Frama-C kernel.
@@ -2849,9 +2825,6 @@
[ Extern ] Post-condition for 'normal' 'positive_result'
ensures positive_result: \is_finite(\result) ∧ \result ≥ 0
Unverifiable but considered Valid.
-[ Extern ] Post-condition for 'infinite' 'result_plus_infinity'
- ensures result_plus_infinity: \is_plus_infinity(\result)
- Unverifiable but considered Valid.
[ Extern ] Post-condition for 'domain_error' 'errno_set'
ensures errno_set: __fc_errno ≡ 1
Unverifiable but considered Valid.
@@ -2861,9 +2834,6 @@
[ Extern ] Assigns for 'domain_error' (file share/libc/math.h, line 298)
assigns __fc_errno, \result;
Unverifiable but considered Valid.
-[ Extern ] Assigns for 'infinite' nothing
- assigns \nothing;
- Unverifiable but considered Valid.
[ Extern ] Assigns for 'normal' nothing
assigns \nothing;
Unverifiable but considered Valid.
@@ -2879,9 +2849,6 @@
[ Extern ] Froms for 'domain_error' (file share/libc/math.h, line 298)
assigns \result \from x;
Unverifiable but considered Valid.
-[ Extern ] Froms for 'infinite' (file share/libc/math.h, line 294)
- assigns \result \from x;
- Unverifiable but considered Valid.
[ Extern ] Froms for 'normal' (file share/libc/math.h, line 290)
assigns \result \from x;
Unverifiable but considered Valid.
@@ -2891,9 +2858,6 @@
[ Valid ] Behavior 'domain_error'
behavior domain_error
by Frama-C kernel.
-[ Valid ] Behavior 'infinite'
- behavior infinite
- by Frama-C kernel.
[ Valid ] Behavior 'normal'
behavior normal
by Frama-C kernel.
@@ -4002,9 +3966,9 @@
--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
- 175 Completely validated
+ 172 Completely validated
16 Locally validated
- 462 Considered valid
+ 453 Considered valid
56 To be validated
- 709 Total
+ 697 Total
--------------------------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 5ba9d6cd179e271e66d7029f2bbe88fa4b466efe..2b13a5643826ada46649dddada194eee794b8059 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing tests/libc/fc_libc.c (with preprocessing)
+[kernel] :0: Warning: unnamed requires
[kernel] share/libc/sys/socket.h:451: Warning:
clause with '\initialized' must contain name 'initialization'
[eva] Analyzing a complete application starting at main
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index fd785f066330f5aec494ac26657707f3754da401..e2d81b03714012574e289c69104651ce08f99819 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -2969,7 +2969,8 @@ extern float sinf(float x);
*/
extern long double sinl(long double x);
-/*@ assigns __fc_errno, \result;
+/*@ requires ¬(is_plus_infinity: \is_plus_infinity(x));
+ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
@@ -2979,12 +2980,6 @@ extern long double sinl(long double x);
assigns \result;
assigns \result \from x;
- behavior infinite:
- assumes is_plus_infinity: \is_plus_infinity(x);
- ensures result_plus_infinity: \is_plus_infinity(\result);
- assigns \result;
- assigns \result \from x;
-
behavior domain_error:
assumes
out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1);
@@ -2993,11 +2988,12 @@ extern long double sinl(long double x);
assigns __fc_errno \from x;
assigns \result \from x;
- disjoint behaviors domain_error, infinite, normal;
+ disjoint behaviors domain_error, normal;
*/
extern double acosh(double x);
-/*@ assigns __fc_errno, \result;
+/*@ requires ¬(is_plus_infinity: \is_plus_infinity(x));
+ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
@@ -3007,12 +3003,6 @@ extern double acosh(double x);
assigns \result;
assigns \result \from x;
- behavior infinite:
- assumes is_plus_infinity: \is_plus_infinity(x);
- ensures result_plus_infinity: \is_plus_infinity(\result);
- assigns \result;
- assigns \result \from x;
-
behavior domain_error:
assumes
out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1);
@@ -3021,11 +3011,12 @@ extern double acosh(double x);
assigns __fc_errno \from x;
assigns \result \from x;
- disjoint behaviors domain_error, infinite, normal;
+ disjoint behaviors domain_error, normal;
*/
extern float acoshf(float x);
-/*@ assigns __fc_errno, \result;
+/*@ requires ¬(is_plus_infinity: \is_plus_infinity(x));
+ assigns __fc_errno, \result;
assigns __fc_errno \from x;
assigns \result \from x;
@@ -3035,12 +3026,6 @@ extern float acoshf(float x);
assigns \result;
assigns \result \from x;
- behavior infinite:
- assumes is_plus_infinity: \is_plus_infinity(x);
- ensures result_plus_infinity: \is_plus_infinity(\result);
- assigns \result;
- assigns \result \from x;
-
behavior domain_error:
assumes
out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1);
@@ -3049,7 +3034,7 @@ extern float acoshf(float x);
assigns __fc_errno \from x;
assigns \result \from x;
- disjoint behaviors domain_error, infinite, normal;
+ disjoint behaviors domain_error, normal;
*/
extern long double acoshl(long double x);