From c1f238c463d40fea86a48638e898bb06277c2431 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 19 Apr 2023 22:14:17 +0200
Subject: [PATCH] [Eva] Adds a test of splits according to the returning value
of a call.
---
.../oracle/partitioning-annots.0.res.oracle | 74 +++++++++++++++++--
.../oracle/partitioning-annots.3.res.oracle | 8 +-
.../oracle/partitioning-annots.4.res.oracle | 8 +-
.../partitioning-annots.0.res.oracle | 14 +++-
.../partitioning-annots.3.res.oracle | 2 +-
.../partitioning-annots.0.res.oracle | 2 +-
tests/value/partitioning-annots.c | 56 ++++++++++++++
7 files changed, 146 insertions(+), 18 deletions(-)
diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle
index ef583a47f12..aa52873360d 100644
--- a/tests/value/oracle/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle/partitioning-annots.0.res.oracle
@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function test_slevel <- main.
- Called from partitioning-annots.c:223.
-[eva] partitioning-annots.c:188: starting to merge loop iterations
-[eva] partitioning-annots.c:193: starting to merge loop iterations
+ Called from partitioning-annots.c:278.
+[eva] partitioning-annots.c:243: starting to merge loop iterations
+[eva] partitioning-annots.c:248: starting to merge loop iterations
[eva] Recording results for test_slevel
[eva] Done for function test_slevel
[eva] computing for function test_unroll <- main.
- Called from partitioning-annots.c:224.
+ Called from partitioning-annots.c:279.
[eva:loop-unroll:partial] partitioning-annots.c:26: loop not completely unrolled
[eva] partitioning-annots.c:26: starting to merge loop iterations
[eva:loop-unroll:partial] partitioning-annots.c:34: loop not completely unrolled
@@ -25,7 +25,7 @@
[eva] Recording results for test_unroll
[eva] Done for function test_unroll
[eva] computing for function test_split <- main.
- Called from partitioning-annots.c:225.
+ Called from partitioning-annots.c:280.
[eva] computing for function Frama_C_interval <- test_split <- main.
Called from partitioning-annots.c:73.
[eva] using specification for function Frama_C_interval
@@ -65,7 +65,7 @@
[eva] Recording results for test_split
[eva] Done for function test_split
[eva] computing for function test_dynamic_split <- main.
- Called from partitioning-annots.c:226.
+ Called from partitioning-annots.c:281.
[eva] partitioning-annots.c:95: Warning:
this partitioning parameter cannot be evaluated safely on all states
[eva] computing for function Frama_C_interval <- test_dynamic_split <- main.
@@ -90,13 +90,44 @@
[eva] Recording results for test_dynamic_split
[eva] Done for function test_dynamic_split
[eva] computing for function test_dynamic_split_predicate <- main.
- Called from partitioning-annots.c:227.
+ Called from partitioning-annots.c:282.
[eva] partitioning-annots.c:124: starting to merge loop iterations
[eva] Recording results for test_dynamic_split_predicate
[eva] Done for function test_dynamic_split_predicate
+[eva] computing for function test_splits_post_call <- main.
+ Called from partitioning-annots.c:283.
+[eva] computing for function Frama_C_interval <- test_splits_post_call <- main.
+ Called from partitioning-annots.c:205.
+[eva] partitioning-annots.c:205:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function spec <- test_splits_post_call <- main.
+ Called from partitioning-annots.c:206.
+[eva] using specification for function spec
+[eva] Done for function spec
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: [-2147483648..-10], ⊥
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: [10..2147483647], ⊥
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: {-1}, [-1000..1000]
+[eva] computing for function body <- test_splits_post_call <- main.
+ Called from partitioning-annots.c:212.
+[eva] Recording results for body
+[eva] Done for function body
+[eva] partitioning-annots.c:212: Reusing old results for call to body
+[eva] partitioning-annots.c:212: Reusing old results for call to body
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: [-510..-10], ⊥
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: [10..510], ⊥
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: {-1}, [-1000..1000]
+[eva] Recording results for test_splits_post_call
+[eva] Done for function test_splits_post_call
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function body:
+ i2 ∈ [-500..500]
+ absolute ∈ [0..500]
+ state ∈ {-1; 0; 1}
+ y ∈ [-1000..1000] or UNINITIALIZED
+ __retres ∈ [-510..510]
[eva:final-states] Values at end of function test_dynamic_split:
Frama_C_entropy_source ∈ [--..--]
a ∈ {0}
@@ -117,6 +148,13 @@
k ∈ {0; 1}
i ∈ {0; 1}
j ∈ {0; 1; 2}
+[eva:final-states] Values at end of function test_splits_post_call:
+ Frama_C_entropy_source ∈ [--..--]
+ x ∈ [-1000..1000] or UNINITIALIZED
+ y ∈ [-1000..1000] or UNINITIALIZED
+ error ∈ [-1000..1000] or UNINITIALIZED
+ i ∈ [-1000..1000]
+ r ∈ [-510..510]
[eva:final-states] Values at end of function test_unroll:
a[0..9] ∈ {42}
b[0..9] ∈ {42}
@@ -145,6 +183,8 @@
[eva:final-states] Values at end of function main:
Frama_C_entropy_source ∈ [--..--]
k ∈ {0; 1}
+[from] Computing for function body
+[from] Done for function body
[from] Computing for function test_dynamic_split
[from] Computing for function Frama_C_interval <-test_dynamic_split
[from] Done for function Frama_C_interval
@@ -155,6 +195,10 @@
[from] Done for function test_slevel
[from] Computing for function test_split
[from] Done for function test_split
+[from] Computing for function test_splits_post_call
+[from] Computing for function spec <-test_splits_post_call
+[from] Done for function spec
+[from] Done for function test_splits_post_call
[from] Computing for function test_unroll
[from] Done for function test_unroll
[from] Computing for function main
@@ -164,6 +208,12 @@
[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 body:
+ y FROM nondet; i; p (and SELF)
+ \result FROM nondet; i
+[from] Function spec:
+ x FROM i
+ \result FROM i
[from] Function test_dynamic_split:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
[from] Function test_dynamic_split_predicate:
@@ -173,12 +223,18 @@
[from] Function test_split:
Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
k FROM Frama_C_entropy_source
+[from] Function test_splits_post_call:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
[from] Function test_unroll:
NO EFFECTS
[from] Function main:
Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
k FROM Frama_C_entropy_source
[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function body:
+ i2; absolute; tmp; state; y; __retres
+[inout] Inputs for function body:
+ nondet
[inout] Out (internal) for function test_dynamic_split:
Frama_C_entropy_source; a; b
[inout] Inputs for function test_dynamic_split:
@@ -195,6 +251,10 @@
Frama_C_entropy_source; k; i; j
[inout] Inputs for function test_split:
Frama_C_entropy_source; k
+[inout] Out (internal) for function test_splits_post_call:
+ Frama_C_entropy_source; x; y; error; i; r
+[inout] Inputs for function test_splits_post_call:
+ Frama_C_entropy_source; nondet
[inout] Out (internal) for function test_unroll:
a[0..9]; b[0..9]; c[0..19]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1;
i_2; i_3; j_1
diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle
index 3fe49f8ff92..365ff709693 100644
--- a/tests/value/oracle/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle/partitioning-annots.3.res.oracle
@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
- Called from partitioning-annots.c:167.
+ Called from partitioning-annots.c:222.
[eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:167:
+[eva] partitioning-annots.c:222:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:173: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] partitioning-annots.c:176: Warning:
+[eva] partitioning-annots.c:228: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] partitioning-annots.c:231: Warning:
division by zero. assert j ≢ 0;
[eva] Recording results for test_history
[eva] done for function test_history
diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle
index 793324f2603..8ad2cdfc8af 100644
--- a/tests/value/oracle/partitioning-annots.4.res.oracle
+++ b/tests/value/oracle/partitioning-annots.4.res.oracle
@@ -6,13 +6,13 @@
nondet ∈ [--..--]
k ∈ {0}
[eva] computing for function Frama_C_interval <- test_history.
- Called from partitioning-annots.c:167.
+ Called from partitioning-annots.c:222.
[eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:167:
+[eva] partitioning-annots.c:222:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:173: Frama_C_show_each: {0}, {0}
-[eva] partitioning-annots.c:173: Frama_C_show_each: {1}, {1}
+[eva] partitioning-annots.c:228: Frama_C_show_each: {0}, {0}
+[eva] partitioning-annots.c:228: Frama_C_show_each: {1}, {1}
[eva] Recording results for test_history
[eva] done for function test_history
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle_apron/partitioning-annots.0.res.oracle b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
index 94ed9ffca14..68d268103b8 100644
--- a/tests/value/oracle_apron/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle_apron/partitioning-annots.0.res.oracle
@@ -1,4 +1,16 @@
-105,106c105,106
+115,116c115,122
+< [eva] partitioning-annots.c:212: Reusing old results for call to body
+< [eva] partitioning-annots.c:212: Reusing old results for call to body
+---
+> [eva] computing for function body <- test_splits_post_call <- main.
+> Called from partitioning-annots.c:212.
+> [eva] Recording results for body
+> [eva] Done for function body
+> [eva] computing for function body <- test_splits_post_call <- main.
+> Called from partitioning-annots.c:212.
+> [eva] Recording results for body
+> [eva] Done for function body
+136,137c142,143
< x ∈ [0..44]
< y ∈ [0..44]
---
diff --git a/tests/value/oracle_apron/partitioning-annots.3.res.oracle b/tests/value/oracle_apron/partitioning-annots.3.res.oracle
index d04cebfc945..5a8823d8cc9 100644
--- a/tests/value/oracle_apron/partitioning-annots.3.res.oracle
+++ b/tests/value/oracle_apron/partitioning-annots.3.res.oracle
@@ -1,3 +1,3 @@
15,16d14
-< [eva:alarm] partitioning-annots.c:176: Warning:
+< [eva:alarm] partitioning-annots.c:231: Warning:
< division by zero. assert j ≢ 0;
diff --git a/tests/value/oracle_octagon/partitioning-annots.0.res.oracle b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
index cd64a1b908f..141d3a1f322 100644
--- a/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
+++ b/tests/value/oracle_octagon/partitioning-annots.0.res.oracle
@@ -1,4 +1,4 @@
-105,106c105,106
+136,137c136,137
< x ∈ [0..44]
< y ∈ [0..44]
---
diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c
index d3ab58aaa50..393b1fe4bbd 100644
--- a/tests/value/partitioning-annots.c
+++ b/tests/value/partitioning-annots.c
@@ -162,6 +162,61 @@ void test_loop_split()
}
}
+/*@
+ assigns \result, *p \from i;
+ behavior error:
+ assumes nondet == 0;
+ assigns \result, *p \from i;
+ ensures \result == -1;
+ ensures \initialized(p) && *p == \old(i);
+ behavior positive:
+ assumes nondet > 0;
+ assigns \result \from i;
+ ensures \result >= 10;
+ behavior negative:
+ assumes nondet < 0;
+ assigns \result \from i;
+ ensures \result <= -10;
+ disjoint behaviors;
+ complete behaviors;
+*/
+int spec(int i, int* p);
+
+int body(int i, int *p) {
+ int i2 = i / 2;
+ int absolute = i2 < 0 ? -i2 : i2;
+ int state = nondet % 2;
+ //@ split state;
+ if (state < 0)
+ return - 10 - absolute;
+ if (state > 0)
+ return 10 + absolute;
+ *p = i;
+ return -1;
+}
+
+/* Tests the application of multiple splits according to the return value of a
+ call, to keep in the caller some state partitioning from the callee.
+ The splits must be defined after the call, so the state partitioning from the
+ callee must be kept until all splits are performed.
+ Tests this whether the function body or a specification is used. */
+void test_splits_post_call (void) {
+ int x, y, error;
+ int i = Frama_C_interval(-1000, 1000);
+ int r = spec(i, &x);
+ //@ split r < -1;
+ //@ split r > -1;
+ if (r == -1)
+ error = x; // There should be no alarm.
+ Frama_C_show_each_spec(r, x); // There should be three states.
+ r = body(i, &y);
+ //@ split r < -1;
+ //@ split r > -1;
+ if (r == -1)
+ error = y; // There should be no alarm.
+ Frama_C_show_each_body(r, y); // There should be three states.
+}
+
void test_history()
{
int i = Frama_C_interval(0,1);
@@ -225,4 +280,5 @@ void main(void)
test_split();
test_dynamic_split();
test_dynamic_split_predicate();
+ test_splits_post_call();
}
--
GitLab