From 63d46c739f5b087ef7c88149dcef5d89348150e4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 14 Jan 2020 10:31:38 +0100
Subject: [PATCH] [Eva] Adds a test of the subdivide annotation and of
subdivision by function.
---
tests/value/nonlin.c | 17 +++++++++-
tests/value/oracle/nonlin.res.oracle | 50 ++++++++++++++++++++++++----
2 files changed, 59 insertions(+), 8 deletions(-)
diff --git a/tests/value/nonlin.c b/tests/value/nonlin.c
index 173929f555a..7395d9b0d4b 100644
--- a/tests/value/nonlin.c
+++ b/tests/value/nonlin.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-eva-subdivide-non-linear 14 -eva-msg-key nonlin"
+ STDOPT: +"-eva-subdivide-non-linear 14 -eva-subdivide-non-linear-function=local_subdivide:32 -eva-msg-key nonlin"
*/
#include "__fc_builtin.h"
@@ -103,10 +103,25 @@ void subdivide_reduced_value () {
int r = t1[i] - t2[i];
}
+/* Tests local subdivision via option -eva-subdivide-non-linear-function
+ and annotations subdivide. */
+void local_subdivide () {
+ int x = Frama_C_interval(-10, 10);
+ int y = Frama_C_interval(-10, 10);
+ /*@ subdivide 0; */
+ int imprecise = x*x - 2*x*y + y*y; // No subdivision: [-400..400]
+ /*@ subdivide 14; */
+ int more_precise = x*x - 2*x*y + y*y; // Some subdivisions: [-48..400]
+ int even_more_precise = x*x - 2*x*y + y*y; // Local subdivision: [-16..400]
+ /*@ subdivide 100; */
+ int precise = x*x - 2*x*y + y*y; // Maximal subdivision: [0..400]
+}
+
void main () {
subdivide_integer ();
subdivide_pointer ();
subdivide_several_variables ();
if (v) subdivide_table ();
subdivide_reduced_value ();
+ local_subdivide ();
}
diff --git a/tests/value/oracle/nonlin.res.oracle b/tests/value/oracle/nonlin.res.oracle
index 14387a41a7e..ca1b870962d 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:107.
+ Called from tests/value/nonlin.c:121.
[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:108.
+ Called from tests/value/nonlin.c:122.
[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:109.
+ Called from tests/value/nonlin.c:123.
[eva] computing for function Frama_C_interval <- subdivide_several_variables <-
main.
Called from tests/value/nonlin.c:51.
@@ -117,7 +117,7 @@
[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:110.
+ 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:
@@ -126,7 +126,7 @@
[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:111.
+ 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:
@@ -135,9 +135,36 @@
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.
+[eva] computing for function Frama_C_interval <- local_subdivide <- main.
+ Called from tests/value/nonlin.c:109.
+[eva] tests/value/nonlin.c:109:
+ 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:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva:nonlin] tests/value/nonlin.c:114:
+ 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: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
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function local_subdivide:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ [-10..10]
+ y ∈ [-10..10]
+ imprecise ∈ [-400..400]
+ more_precise ∈ [-48..400]
+ even_more_precise ∈ [-16..400]
+ precise ∈ [0..400]
[eva:final-states] Values at end of function subdivide_integer:
z ∈ [-32768..28523]
k ∈ [-2..1118367364]
@@ -180,11 +207,13 @@
NON TERMINATING FUNCTION
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
+[from] Computing for function local_subdivide
+[from] Computing for function Frama_C_interval <-local_subdivide
+[from] Done for function Frama_C_interval
+[from] Done for function local_subdivide
[from] Computing for function subdivide_integer
[from] Done for function subdivide_integer
[from] Computing for function subdivide_pointer
-[from] Computing for function Frama_C_interval <-subdivide_pointer
-[from] Done for function Frama_C_interval
[from] Done for function subdivide_pointer
[from] Computing for function subdivide_reduced_value
[from] Done for function subdivide_reduced_value
@@ -200,6 +229,8 @@
[from] Function Frama_C_interval:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
\result FROM Frama_C_entropy_source; min; max
+[from] Function local_subdivide:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function subdivide_integer:
NO EFFECTS
[from] Function subdivide_pointer:
@@ -213,6 +244,11 @@
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function local_subdivide:
+ Frama_C_entropy_source; x; y; imprecise; more_precise; even_more_precise;
+ precise
+[inout] Inputs for function local_subdivide:
+ Frama_C_entropy_source
[inout] Out (internal) for function subdivide_integer:
z; k; l; x; p; i1; i2; r; t[0..100]; idx
[inout] Inputs for function subdivide_integer:
--
GitLab