From 2600bd3bc45e163fb1c3fadf08ecc22635688246 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 2 Dec 2021 16:54:01 +0100
Subject: [PATCH] [Eva] multidim: merges tests into one
---
tests/value/multidim.c | 14 +-
tests/value/oracle/multidim.res.oracle | 226 +++++++++++++++++++++++++
2 files changed, 235 insertions(+), 5 deletions(-)
create mode 100644 tests/value/oracle/multidim.res.oracle
diff --git a/tests/value/multidim.c b/tests/value/multidim.c
index 9ec307546d8..bc3e62d3e8a 100644
--- a/tests/value/multidim.c
+++ b/tests/value/multidim.c
@@ -1,8 +1,5 @@
/* run.config*
- STDOPT: #"-main main -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
- STDOPT: #"-main main2 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
- STDOPT: #"-main main3 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
- STDOPT: #"-main main4 -eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
+ STDOPT: #"-eva-msg-key d-multidim -eva-domains multidim -eva-plevel 1"
*/
#include "__fc_builtin.h"
#define N 4
@@ -32,7 +29,7 @@ void f(void);
volatile int nondet;
-void main(s x) {
+void main1(s x) {
s y1 = {{{{3.0}}}};
s y2;
@@ -88,3 +85,10 @@ void main4(void) { // How trace partitioning changes array partitioning ?
}
Frama_C_domain_show_each(t);
}
+
+void main(s x) {
+ main1(x);
+ main2();
+ main3();
+ main4();
+}
diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle
new file mode 100644
index 00000000000..83818a8f1c6
--- /dev/null
+++ b/tests/value/oracle/multidim.res.oracle
@@ -0,0 +1,226 @@
+[kernel] Parsing multidim.c (with preprocessing)
+[eva:experimental] Warning: The multidim domain is experimental.
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+ z[0..3] ∈ {0}
+ nondet ∈ [--..--]
+[eva] computing for function main1 <- main.
+ Called from multidim.c:90.
+[eva] multidim.c:39:
+ Frama_C_domain_show_each:
+ x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[0].i ∈ [--..--]
+ .t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[1].i ∈ [--..--]
+ .t1[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[2].i ∈ [--..--]
+ .t1[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[3].i ∈ [--..--]
+ .t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[0].i ∈ [--..--]
+ .t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[1].i ∈ [--..--]
+ .t2[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[2].i ∈ [--..--]
+ .t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[3].i ∈ [--..--]
+ # multidim: T
+ y1 : # cvalue: .t1[0].f ∈ {3.}
+ {.t1{[0].i; [1..3]}; .t2[0..3]} ∈ {0}
+ # multidim: {
+ .t1[0] = { .f = {3.}, .i = {0} },
+ .t2{
+ [0] = { .f = {0}, .i = {0} },
+ [1] = { .f = {0}, .i = {0} },
+ [2] = { .f = {0}, .i = {0} },
+ [3] = { .f = {0}, .i = {0} }
+ }
+ }
+ y2 : # cvalue: .t1[0].f ∈ {4.} or UNINITIALIZED
+ {.t1{[0].i; [1..3]}; .t2[0..3]} ∈ UNINITIALIZED
+ # multidim: { .t1[0] = { .f = {4.} } }
+ z : # cvalue: {0}
+ # multidim: 0
+[eva] multidim.c:45:
+ Frama_C_domain_show_each:
+ x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[0].i ∈ [--..--]
+ .t1[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[1].i ∈ [--..--]
+ .t1[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[2].i ∈ [--..--]
+ .t1[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t1[3].i ∈ [--..--]
+ .t2[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[0].i ∈ [--..--]
+ .t2[1].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[1].i ∈ [--..--]
+ .t2[2].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[2].i ∈ [--..--]
+ .t2[3].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
+ .t2[3].i ∈ [--..--]
+ # multidim: {
+ .t1[0 .. 3] = { .f = {{ ANYTHING }} },
+ .t2[0 .. 3] = { .f = {{ ANYTHING }} }
+ }
+[eva] computing for function f <- main1 <- main.
+ Called from multidim.c:47.
+[eva] using specification for function f
+[eva] Done for function f
+[eva] multidim.c:48:
+ Frama_C_domain_show_each:
+ z : # cvalue: [--..--]
+ # multidim: [0 .. 3] = {
+ .t1[0 .. 3] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38]
+ },
+ .t2[0 .. 3] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38]
+ }
+ }
+[eva:alarm] multidim.c:50: Warning: check got status unknown.
+[eva] Recording results for main1
+[eva] Done for function main1
+[eva] computing for function main2 <- main.
+ Called from multidim.c:91.
+[eva] multidim.c:55: starting to merge loop iterations
+[eva:alarm] multidim.c:58: Warning: check got status unknown.
+[eva] multidim.c:59:
+ Frama_C_domain_show_each:
+ t : # cvalue: {0; 1}
+ # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} }
+[eva] Recording results for main2
+[eva] Done for function main2
+[eva] computing for function main3 <- main.
+ Called from multidim.c:92.
+[eva] multidim.c:64: starting to merge loop iterations
+[eva] multidim.c:63: starting to merge loop iterations
+[kernel] multidim.c:65:
+ more than 1(20) locations to update in array. Approximating.
+[kernel] multidim.c:66:
+ more than 1(20) locations to update in array. Approximating.
+[kernel] multidim.c:65:
+ more than 1(28) locations to update in array. Approximating.
+[kernel] multidim.c:66:
+ more than 1(28) locations to update in array. Approximating.
+[eva] computing for function Frama_C_interval <- main3 <- main.
+ Called from multidim.c:70.
+[eva] using specification for function Frama_C_interval
+[eva] multidim.c:70:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- main3 <- main.
+ Called from multidim.c:71.
+[eva] multidim.c:71:
+ function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] multidim.c:73:
+ Frama_C_domain_show_each:
+ z : # cvalue: [--..--]
+ # multidim: [0 .. 3] = {
+ .t1[0 .. 3] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38],
+ .i = T
+ },
+ .t2[0 .. 3] = {
+ .f = [-3.40282346639e+38 .. 3.40282346639e+38]
+ }
+ }
+ r : # cvalue: [--..--]
+ # multidim: { .f = [-3.40282346639e+38 .. 3.40282346639e+38], .i = T }
+[eva] Recording results for main3
+[kernel] multidim.c:65: more than 1(28) elements to enumerate. Approximating.
+[kernel] multidim.c:66: more than 1(28) elements to enumerate. Approximating.
+[eva] Done for function main3
+[eva] computing for function main4 <- main.
+ Called from multidim.c:93.
+[eva:loop-unroll:partial] multidim.c:80: loop not completely unrolled
+[eva] multidim.c:80: starting to merge loop iterations
+[eva] multidim.c:82: starting to merge loop iterations
+[eva] multidim.c:86:
+ Frama_C_domain_show_each:
+ t : # cvalue: {42}
+ # multidim: { [0] = {42}, [1] = {42}, [2] = {42}, [3] = {42} }
+[eva] Recording results for main4
+[eva] Done for function main4
+[eva] Recording results for main
+[eva] done for function main
+[kernel] multidim.c:50: more than 1(28) elements to enumerate. Approximating.
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function main1:
+ z[0..3] ∈ [--..--]
+ y1.t1[0].f ∈ {3.}
+ {.t1{[0].i; [1..3]}; .t2[0..3]} ∈ {0}
+ y2.t1[0].f ∈ {4.} or UNINITIALIZED
+ {.t1{[0].i; [1..3]}; .t2[0..3]} ∈ UNINITIALIZED
+[eva:final-states] Values at end of function main2:
+ t[0..9] ∈ {0; 1}
+[eva:final-states] Values at end of function main3:
+ Frama_C_entropy_source ∈ [--..--]
+ z[0..3] ∈ [--..--]
+ a ∈ {0; 1; 2; 3}
+ b ∈ {0; 1; 2; 3}
+ r ∈ [--..--]
+[eva:final-states] Values at end of function main4:
+ t[0..3] ∈ {42}
+[eva:final-states] Values at end of function main:
+ Frama_C_entropy_source ∈ [--..--]
+ z[0..3] ∈ [--..--]
+[from] Computing for function main1
+[from] Computing for function f <-main1
+[from] Done for function f
+[from] Done for function main1
+[from] Computing for function main2
+[from] Done for function main2
+[from] Computing for function main3
+[kernel] multidim.c:65: more than 1(28) dependencies to update. Approximating.
+[kernel] multidim.c:66: more than 1(28) dependencies to update. Approximating.
+[from] Computing for function Frama_C_interval <-main3
+[from] Done for function Frama_C_interval
+[from] Done for function main3
+[from] Computing for function main4
+[from] Done for function main4
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+ These dependencies hold at termination for the executions that terminate:
+[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 f:
+ z[0..3] FROM \nothing
+[from] Function main1:
+ z[0..3] FROM \nothing
+[from] Function main2:
+ NO EFFECTS
+[from] Function main3:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ z{[0..2]; [3].t1[0..3]} FROM \nothing (and SELF)
+[from] Function main4:
+ NO EFFECTS
+[from] Function main:
+ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+ z[0..3] FROM \nothing
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function main1:
+ z[0..3]; y1; y2.t1[0].f
+[inout] Inputs for function main1:
+ nondet
+[inout] Out (internal) for function main2:
+ t[0..9]; i
+[inout] Inputs for function main2:
+ \nothing
+[inout] Out (internal) for function main3:
+ Frama_C_entropy_source; z{[0..2]; [3].t1[0..3]}; i; j; a; b; r
+[inout] Inputs for function main3:
+ Frama_C_entropy_source; z{[0..2]; [3].t1[0..3]}
+[inout] Out (internal) for function main4:
+ t[0..3]; i; j
+[inout] Inputs for function main4:
+ \nothing
+[inout] Out (internal) for function main:
+ Frama_C_entropy_source; z[0..3]
+[inout] Inputs for function main:
+ Frama_C_entropy_source; z{[0..2]; [3].t1[0..3]}; nondet
--
GitLab