Skip to content
Snippets Groups Projects
Commit 2600bd3b authored by Valentin Perrelle's avatar Valentin Perrelle Committed by David Bühler
Browse files

[Eva] multidim: merges tests into one

parent 8837765c
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
tests/value/multidim.c
+ 9
− 5
View file @ 2600bd3b
/* 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();
}
tests/value/oracle/multidim.res.oracle 0 → 100644
+ 226
− 0
View file @ 2600bd3b
[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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment