From d7f4c82e51a609ea6997e404cdc10d8a78bd530a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 13 Feb 2020 15:46:08 +0100
Subject: [PATCH] [Eva] Tests the file tests/nonlin.c with the option
-warn-special-float none.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Previous commits have introduced the new runs (and oracles) without this option.
This commit only contains the changes due to this option:
- no alarms for non-finite floating-point values.
- in the function [around_zeros], no reduction of the variable [f] as the
division by 0 simply computes ∞.
- volatile floating-point variables have a value in [-∞..∞] ∪ NaN.
---
tests/float/nonlin.c | 4 ++--
tests/float/oracle/nonlin.2.res.oracle | 30 ++++++--------------------
tests/float/oracle/nonlin.5.res.oracle | 30 ++++++--------------------
3 files changed, 16 insertions(+), 48 deletions(-)
diff --git a/tests/float/nonlin.c b/tests/float/nonlin.c
index 76a1baafa01..926e4c6571e 100644
--- a/tests/float/nonlin.c
+++ b/tests/float/nonlin.c
@@ -1,10 +1,10 @@
/* run.config*
OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 0
OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=double" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 0
OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
- OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10
+ OPT: -eva-msg-key nonlin -slevel 30 -eva @EVA_CONFIG@ -cpp-extra-args="-DFLOAT=float" -float-hex -journal-disable -eva-subdivide-non-linear 10 -warn-special-float none
*/
#include "__fc_builtin.h"
diff --git a/tests/float/oracle/nonlin.2.res.oracle b/tests/float/oracle/nonlin.2.res.oracle
index 702ae9ed864..116cdb8b400 100644
--- a/tests/float/oracle/nonlin.2.res.oracle
+++ b/tests/float/oracle/nonlin.2.res.oracle
@@ -204,8 +204,6 @@
[eva] Done for function other
[eva] computing for function split_alarm <- main.
Called from tests/float/nonlin.c:109.
-[eva:alarm] tests/float/nonlin.c:76: Warning:
- non-finite float value. assert \is_finite(v);
[eva:nonlin] tests/float/nonlin.c:77:
non-linear '(double)ff * (double)ff', lv 'ff'
[eva:nonlin] tests/float/nonlin.c:77: subdividing on ff
@@ -213,10 +211,6 @@
[eva] Done for function split_alarm
[eva] computing for function norm <- main.
Called from tests/float/nonlin.c:110.
-[eva:alarm] tests/float/nonlin.c:81: Warning:
- non-finite float value. assert \is_finite(v);
-[eva:alarm] tests/float/nonlin.c:82: Warning:
- non-finite float value. assert \is_finite(v);
[eva:nonlin] tests/float/nonlin.c:83:
non-linear '(double)v1 * (double)v1', lv 'v1'
[eva:nonlin] tests/float/nonlin.c:83:
@@ -227,16 +221,9 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:111.
-[eva:alarm] tests/float/nonlin.c:89: Warning:
- non-finite float value.
- assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
[eva] tests/float/nonlin.c:89:
Assigning imprecise value to a_0.
The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning:
- non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning:
- non-finite float value. assert \is_finite((float)(a_0 + a_0));
[eva] tests/float/nonlin.c:90:
Assigning imprecise value to f.
The imprecision originates from Arithmetic
@@ -255,9 +242,6 @@
[eva:nonlin] tests/float/nonlin.c:103:
non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
[eva:nonlin] tests/float/nonlin.c:103: subdividing on f
-[eva:alarm] tests/float/nonlin.c:103: Warning:
- non-finite float value.
- assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
[eva] Recording results for around_zeros
[eva] Done for function around_zeros
[eva] Recording results for main
@@ -270,8 +254,8 @@
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149}
- f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
- res ∈ {-0x1.0000000000000p0}
+ f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
+ res ∈ [-0x1.0000000000000p0 .. inf]
[eva:final-states] Values at end of function garbled:
a_0 ∈
{{ garbled mix of &{x_0}
@@ -286,9 +270,9 @@
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffffffffffp2]
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
[eva:final-states] Values at end of function norm:
- v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
- v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
- square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+ v1 ∈ [-inf .. inf] ∪ {NaN}
+ v2 ∈ [-inf .. inf] ∪ {NaN}
+ square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.714fffffffff7p1 .. 0x1.71c0000000003p1]
@@ -304,8 +288,8 @@
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
[eva:final-states] Values at end of function split_alarm:
- ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
- d_0 ∈ [0x1.0000020000030p-256 .. 0x1.dcd64ffffffffp29]
+ ff ∈ [-inf .. inf] ∪ {NaN}
+ d_0 ∈ [0x0.0000000000000p0 .. 0x1.dcd64ffffffffp29] ∪ {NaN}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
diff --git a/tests/float/oracle/nonlin.5.res.oracle b/tests/float/oracle/nonlin.5.res.oracle
index 3f173370a07..e041a4b9edf 100644
--- a/tests/float/oracle/nonlin.5.res.oracle
+++ b/tests/float/oracle/nonlin.5.res.oracle
@@ -204,8 +204,6 @@
[eva] Done for function other
[eva] computing for function split_alarm <- main.
Called from tests/float/nonlin.c:109.
-[eva:alarm] tests/float/nonlin.c:76: Warning:
- non-finite float value. assert \is_finite(v);
[eva:nonlin] tests/float/nonlin.c:77:
non-linear '(double)ff * (double)ff', lv 'ff'
[eva:nonlin] tests/float/nonlin.c:77: subdividing on ff
@@ -213,10 +211,6 @@
[eva] Done for function split_alarm
[eva] computing for function norm <- main.
Called from tests/float/nonlin.c:110.
-[eva:alarm] tests/float/nonlin.c:81: Warning:
- non-finite float value. assert \is_finite(v);
-[eva:alarm] tests/float/nonlin.c:82: Warning:
- non-finite float value. assert \is_finite(v);
[eva:nonlin] tests/float/nonlin.c:83:
non-linear '(double)v1 * (double)v1', lv 'v1'
[eva:nonlin] tests/float/nonlin.c:83:
@@ -227,16 +221,9 @@
[eva] Done for function norm
[eva] computing for function garbled <- main.
Called from tests/float/nonlin.c:111.
-[eva:alarm] tests/float/nonlin.c:89: Warning:
- non-finite float value.
- assert \is_finite((float)((int)(&x_0 + (int)(&x_0))));
[eva] tests/float/nonlin.c:89:
Assigning imprecise value to a_0.
The imprecision originates from Arithmetic {tests/float/nonlin.c:89}
-[eva:alarm] tests/float/nonlin.c:90: Warning:
- non-finite float value. assert \is_finite(a_0);
-[eva:alarm] tests/float/nonlin.c:90: Warning:
- non-finite float value. assert \is_finite((float)(a_0 + a_0));
[eva] tests/float/nonlin.c:90:
Assigning imprecise value to f.
The imprecision originates from Arithmetic
@@ -255,9 +242,6 @@
[eva:nonlin] tests/float/nonlin.c:103:
non-linear 'f1 / (((f + f) - f) - f1)', lv 'f1'
[eva:nonlin] tests/float/nonlin.c:103: subdividing on f
-[eva:alarm] tests/float/nonlin.c:103: Warning:
- non-finite float value.
- assert \is_finite((float)(f1 / (float)((float)((float)(f + f) - f) - f1)));
[eva] Recording results for around_zeros
[eva] Done for function around_zeros
[eva] Recording results for main
@@ -270,8 +254,8 @@
[eva:final-states] Values at end of function around_zeros:
Frama_C_entropy_source ∈ [--..--]
f1 ∈ {0x1.0000000000000p-149}
- f ∈ [-0x0.0000000000000p0 .. 0x0.0000000000000p0]
- res ∈ {-0x1.0000000000000p0}
+ f ∈ [-0x0.0000000000000p0 .. 0x1.0000000000000p-149]
+ res ∈ [-0x1.0000000000000p0 .. inf]
[eva:final-states] Values at end of function garbled:
a_0 ∈
{{ garbled mix of &{x_0}
@@ -286,9 +270,9 @@
r2 ∈ [0x1.4000000000000p2 .. 0x1.c0fffe0000000p2]
d ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
[eva:final-states] Values at end of function norm:
- v1 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
- v2 ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
- square ∈ [-0x0.0000000000000p0 .. 0x1.fffffc0000020p256]
+ v1 ∈ [-inf .. inf] ∪ {NaN}
+ v2 ∈ [-inf .. inf] ∪ {NaN}
+ square ∈ [-0x0.0000000000000p0 .. inf] ∪ {NaN}
[eva:final-states] Values at end of function other:
Frama_C_entropy_source ∈ [--..--]
i ∈ [-0x1.714fee0000000p1 .. 0x1.71c0040000000p1]
@@ -304,8 +288,8 @@
rbits1 ∈ {0; 1; 2}
rbits2 ∈ {0; 1}
[eva:final-states] Values at end of function split_alarm:
- ff ∈ [-0x1.fffffe0000000p127 .. 0x1.fffffe0000000p127]
- d_0 ∈ [0x1.0000020000030p-256 .. 0x1.dcd64ffffffffp29]
+ ff ∈ [-inf .. inf] ∪ {NaN}
+ d_0 ∈ [0x0.0000000000000p0 .. 0x1.dcd64ffffffffp29] ∪ {NaN}
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
a ∈ [0x1.4000000000000p2 .. 0x1.c000000000000p2]
--
GitLab