From 61a08a25bada4df42485acf841bae1b5b9a32b32 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 7 Feb 2020 09:14:01 +0100
Subject: [PATCH] [Eva] Updates an outdated comment in a test.
---
tests/value/nonlin.c | 8 ++--
tests/value/oracle/nonlin.res.oracle | 70 ++++++++++++++--------------
2 files changed, 38 insertions(+), 40 deletions(-)
diff --git a/tests/value/nonlin.c b/tests/value/nonlin.c
index 7395d9b0d4b..1a05ef68d31 100644
--- a/tests/value/nonlin.c
+++ b/tests/value/nonlin.c
@@ -54,11 +54,9 @@ void subdivide_several_variables () {
int z = Frama_C_interval(-10, 10);
/* A subdivision on each variable separately is more efficient here. */
int norm = x * x + y * y;
- /* Subdivide on x, then on y.
- This evaluation is currently imprecise as the subdivision is stopped when
- it seems not to improve the bounds of the result. Here however, the
- subdivision on x would improve the value of x*x, and the subdivision on y
- would then improve the value of the expression. */
+ /* Subdivide on x, then on y. Note that the subdivision on x does not improve
+ the result but only the value of x*x, while the later subdivision on y
+ improve the value of the result thanks to the reduced value of x*x. */
int mult = ((x*x)*y)*y;
/* A subdivision on both variables is more efficient here. */
int zero = x * y - y * x;
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index 1783b2b8ca0..de062d28c58 100644
--- a/tests/value/oracle/nonlin.res.oracle
+++ b/tests/value/oracle/nonlin.res.oracle
@@ -24,7 +24,7 @@
[31] ∈ {5}
[32..35] ∈ {0}
[eva] computing for function subdivide_integer <- main.
- Called from tests/value/nonlin.c:121.
+ Called from tests/value/nonlin.c:119.
[eva:nonlin] tests/value/nonlin.c:31:
non-linear '((int)z + 675) * ((int)z + 675)', lv 'z'
[eva:nonlin] tests/value/nonlin.c:31: subdividing on z
@@ -45,7 +45,7 @@
[eva] Recording results for subdivide_integer
[eva] Done for function subdivide_integer
[eva] computing for function subdivide_pointer <- main.
- Called from tests/value/nonlin.c:122.
+ Called from tests/value/nonlin.c:120.
[eva] computing for function Frama_C_interval <- subdivide_pointer <- main.
Called from tests/value/nonlin.c:12.
[eva] using specification for function Frama_C_interval
@@ -68,7 +68,7 @@
[eva] Recording results for subdivide_pointer
[eva] Done for function subdivide_pointer
[eva] computing for function subdivide_several_variables <- main.
- Called from tests/value/nonlin.c:123.
+ Called from tests/value/nonlin.c:121.
[eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main.
Called from tests/value/nonlin.c:51.
@@ -97,61 +97,61 @@
[eva:nonlin] tests/value/nonlin.c:56: non-linear 'y * y', lv 'y'
[eva:nonlin] tests/value/nonlin.c:56: subdividing on x
[eva:nonlin] tests/value/nonlin.c:56: subdividing on y
-[eva:nonlin] tests/value/nonlin.c:62: non-linear 'x * x', lv 'x'
-[eva:nonlin] tests/value/nonlin.c:62: non-linear '((x * x) * y) * y', lv 'y'
-[eva:nonlin] tests/value/nonlin.c:62: subdividing on x
-[eva:nonlin] tests/value/nonlin.c:62: subdividing on y
-[eva:nonlin] tests/value/nonlin.c:64: non-linear 'x * y - y * x', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:64: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:67:
+[eva:nonlin] tests/value/nonlin.c:60: non-linear 'x * x', lv 'x'
+[eva:nonlin] tests/value/nonlin.c:60: non-linear '((x * x) * y) * y', lv 'y'
+[eva:nonlin] tests/value/nonlin.c:60: subdividing on x
+[eva:nonlin] tests/value/nonlin.c:60: subdividing on y
+[eva:nonlin] tests/value/nonlin.c:62: non-linear 'x * y - y * x', lv 'y, x'
+[eva:nonlin] tests/value/nonlin.c:62: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:65:
non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:67: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:68:
+[eva:nonlin] tests/value/nonlin.c:65: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:66:
non-linear '(x * x + y * y) - (2 * x) * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:68: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:70:
+[eva:nonlin] tests/value/nonlin.c:66: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:68:
non-linear '(z * x + x * y) + y * z', lv 'z, y, x'
-[eva:nonlin] tests/value/nonlin.c:70: non-linear 'w * w', lv 'w'
-[eva:nonlin] tests/value/nonlin.c:70: subdividing on x, y, z
-[eva:nonlin] tests/value/nonlin.c:70: subdividing on w
+[eva:nonlin] tests/value/nonlin.c:68: non-linear 'w * w', lv 'w'
+[eva:nonlin] tests/value/nonlin.c:68: subdividing on x, y, z
+[eva:nonlin] tests/value/nonlin.c:68: subdividing on w
[eva] Recording results for subdivide_several_variables
[eva] Done for function subdivide_several_variables
[eva] computing for function subdivide_table <- main.
- Called from tests/value/nonlin.c:124.
-[eva] tests/value/nonlin.c:89: loop invariant got status valid.
-[eva] tests/value/nonlin.c:90: starting to merge loop iterations
-[eva:nonlin] tests/value/nonlin.c:91:
+ Called from tests/value/nonlin.c:122.
+[eva] tests/value/nonlin.c:87: loop invariant got status valid.
+[eva] tests/value/nonlin.c:88: starting to merge loop iterations
+[eva:nonlin] tests/value/nonlin.c:89:
non-linear '(4 + ((x >> 2) * 3 << 2)) + x % 4', lv 'x'
-[eva:nonlin] tests/value/nonlin.c:91: subdividing on x
+[eva:nonlin] tests/value/nonlin.c:89: subdividing on x
[eva] Recording results for subdivide_table
[eva] Done for function subdivide_table
[eva] computing for function subdivide_reduced_value <- main.
- Called from tests/value/nonlin.c:125.
-[eva:nonlin] tests/value/nonlin.c:103: non-linear 't1[i] - t2[i]', lv 'i'
-[eva:nonlin] tests/value/nonlin.c:103: subdividing on i
-[eva:alarm] tests/value/nonlin.c:103: Warning:
+ Called from tests/value/nonlin.c:123.
+[eva:nonlin] tests/value/nonlin.c:101: non-linear 't1[i] - t2[i]', lv 'i'
+[eva:nonlin] tests/value/nonlin.c:101: subdividing on i
+[eva:alarm] tests/value/nonlin.c:101: Warning:
accessing out of bounds index. assert 0 ≤ i;
-[eva:alarm] tests/value/nonlin.c:103: Warning:
+[eva:alarm] tests/value/nonlin.c:101: Warning:
accessing out of bounds index. assert i < 2;
[eva] Recording results for subdivide_reduced_value
[eva] Done for function subdivide_reduced_value
[eva] computing for function local_subdivide <- main.
- Called from tests/value/nonlin.c:126.
+ Called from tests/value/nonlin.c:124.
[eva] computing for function Frama_C_interval <- local_subdivide <- main.
- Called from tests/value/nonlin.c:109.
-[eva] tests/value/nonlin.c:109:
+ Called from tests/value/nonlin.c:107.
+[eva] tests/value/nonlin.c:107:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function Frama_C_interval <- local_subdivide <- main.
- Called from tests/value/nonlin.c:110.
-[eva] tests/value/nonlin.c:110:
+ Called from tests/value/nonlin.c:108.
+[eva] tests/value/nonlin.c:108:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva:nonlin] tests/value/nonlin.c:114:
+[eva:nonlin] tests/value/nonlin.c:112:
non-linear '(x * x - (2 * x) * y) + y * y', lv 'y, x'
-[eva:nonlin] tests/value/nonlin.c:114: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:112: subdividing on x, y
+[eva:nonlin] tests/value/nonlin.c:113: subdividing on x, y
[eva:nonlin] tests/value/nonlin.c:115: subdividing on x, y
-[eva:nonlin] tests/value/nonlin.c:117: subdividing on x, y
[eva] Recording results for local_subdivide
[eva] Done for function local_subdivide
[eva] Recording results for main
--
GitLab