From 67f62369ecdeb96bd1921da8b190a6c3ddcfa852 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 11 Feb 2021 15:00:45 +0100
Subject: [PATCH] [kernel] Updates test oracles.
The behaviors leading to forbidden floating-point values are now removed, and
the negation of their assumes are added as preconditions.
---
tests/idct/oracle/ieee_1180_1990.res.oracle | 42 ++-------------------
tests/libc/oracle/fc_libc.0.res.oracle | 1 +
tests/libc/oracle/fc_libc.1.res.oracle | 33 +++++-----------
3 files changed, 13 insertions(+), 63 deletions(-)
diff --git a/tests/idct/oracle/ieee_1180_1990.res.oracle b/tests/idct/oracle/ieee_1180_1990.res.oracle
index 02d4b53e0b8..58fa3ec2dd5 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 5ba9d6cd179..2b13a564382 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 fd785f06633..e2d81b03714 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);
--
GitLab