From dcc7fb49fa579fef8144b76b71e008971d22b148 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Apr 2022 16:56:48 +0200
Subject: [PATCH] [Eva] Removes unused oracles.
---
tests/value/oracle/multidim.0.res.oracle | 107 -----------------------
tests/value/oracle/multidim.1.res.oracle | 30 -------
tests/value/oracle/multidim.2.res.oracle | 73 ----------------
tests/value/oracle/multidim.3.res.oracle | 31 -------
4 files changed, 241 deletions(-)
delete mode 100644 tests/value/oracle/multidim.0.res.oracle
delete mode 100644 tests/value/oracle/multidim.1.res.oracle
delete mode 100644 tests/value/oracle/multidim.2.res.oracle
delete mode 100644 tests/value/oracle/multidim.3.res.oracle
diff --git a/tests/value/oracle/multidim.0.res.oracle b/tests/value/oracle/multidim.0.res.oracle
deleted file mode 100644
index 05a95cd5a3b..00000000000
--- a/tests/value/oracle/multidim.0.res.oracle
+++ /dev/null
@@ -1,107 +0,0 @@
-[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] multidim.c:42:
- 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:48:
- 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 <- main.
- Called from multidim.c:50.
-[eva] using specification for function f
-[eva] Done for function f
-[eva] multidim.c:51:
- 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:53: Warning: check got status unknown.
-[eva] Recording results for main
-[eva] done for function main
-[kernel] multidim.c:53: more than 1(28) elements to enumerate. Approximating.
-[kernel] multidim.c:53: more than 1(28) elements to enumerate. Approximating.
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
- 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
-[from] Computing for function main
-[from] Computing for function f <-main
-[from] Done for function f
-[from] Done for function main
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function f:
- z[0..3] FROM \nothing
-[from] Function main:
- z[0..3] FROM \nothing
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main:
- z[0..3]; y1; y2.t1[0].f
-[inout] Inputs for function main:
- nondet
diff --git a/tests/value/oracle/multidim.1.res.oracle b/tests/value/oracle/multidim.1.res.oracle
deleted file mode 100644
index 253201525cd..00000000000
--- a/tests/value/oracle/multidim.1.res.oracle
+++ /dev/null
@@ -1,30 +0,0 @@
-[kernel] Parsing multidim.c (with preprocessing)
-[eva:experimental] Warning: The multidim domain is experimental.
-[eva] Analyzing a complete application starting at main2
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- z[0..3] ∈ {0}
- nondet ∈ [--..--]
-[eva] multidim.c:58: starting to merge loop iterations
-[eva:alarm] multidim.c:61: Warning: check got status unknown.
-[eva] multidim.c:62:
- 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] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main2:
- t[0..9] ∈ {0; 1}
-[from] Computing for function main2
-[from] Done for function main2
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main2:
- NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main2:
- t[0..9]; i
-[inout] Inputs for function main2:
- \nothing
diff --git a/tests/value/oracle/multidim.2.res.oracle b/tests/value/oracle/multidim.2.res.oracle
deleted file mode 100644
index 6a6d57ae5a5..00000000000
--- a/tests/value/oracle/multidim.2.res.oracle
+++ /dev/null
@@ -1,73 +0,0 @@
-[kernel] Parsing multidim.c (with preprocessing)
-[eva:experimental] Warning: The multidim domain is experimental.
-[eva] Analyzing a complete application starting at main3
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- z[0..3] ∈ {0}
- nondet ∈ [--..--]
-[eva] multidim.c:67: starting to merge loop iterations
-[eva] multidim.c:66: starting to merge loop iterations
-[kernel] multidim.c:68:
- more than 1(20) locations to update in array. Approximating.
-[kernel] multidim.c:69:
- more than 1(20) locations to update in array. Approximating.
-[kernel] multidim.c:68:
- more than 1(28) locations to update in array. Approximating.
-[kernel] multidim.c:69:
- more than 1(28) locations to update in array. Approximating.
-[eva] computing for function Frama_C_interval <- main3.
- Called from multidim.c:73.
-[eva] using specification for function Frama_C_interval
-[eva] multidim.c:73:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] computing for function Frama_C_interval <- main3.
- Called from multidim.c:74.
-[eva] multidim.c:74:
- function Frama_C_interval: precondition 'order' got status valid.
-[eva] Done for function Frama_C_interval
-[eva] multidim.c:76:
- Frama_C_domain_show_each:
- z : # cvalue: [0].t1[0].f ∈ [0. .. 2.]
- {[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
- [--..--]
- [3].t1[3].i ∈ {0; 2}
- [3].t2[0..3] ∈ {0}
- # multidim: [0 .. 3] = { .t1[0 .. 3] = { .f = [0. .. 2.], .i = {0; 2} } }
- r : # cvalue: [--..--]
- # multidim: { .f = [0. .. 2.], .i = {0; 2} }
-[eva] Recording results for main3
-[kernel] multidim.c:68: more than 1(28) elements to enumerate. Approximating.
-[kernel] multidim.c:69: more than 1(28) elements to enumerate. Approximating.
-[eva] done for function main3
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main3:
- Frama_C_entropy_source ∈ [--..--]
- z[0].t1[0].f ∈ [0. .. 2.]
- {[0]{.t1{[0].i; [1..3]}; .t2[0..3]}; [1..2]; [3].t1{[0..2]; [3].f}} ∈
- [--..--]
- [3].t1[3].i ∈ {0; 2}
- [3].t2[0..3] ∈ {0}
- a ∈ {0; 1; 2; 3}
- b ∈ {0; 1; 2; 3}
- r ∈ [--..--]
-[from] Computing for function main3
-[kernel] multidim.c:68: more than 1(28) dependencies to update. Approximating.
-[kernel] multidim.c:69: 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] ====== 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 main3:
- Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
- z{[0..2]; [3].t1[0..3]} FROM \nothing (and SELF)
-[from] ====== END OF DEPENDENCIES ======
-[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]}
diff --git a/tests/value/oracle/multidim.3.res.oracle b/tests/value/oracle/multidim.3.res.oracle
deleted file mode 100644
index a560275847d..00000000000
--- a/tests/value/oracle/multidim.3.res.oracle
+++ /dev/null
@@ -1,31 +0,0 @@
-[kernel] Parsing multidim.c (with preprocessing)
-[eva:experimental] Warning: The multidim domain is experimental.
-[eva] Analyzing a complete application starting at main4
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- z[0..3] ∈ {0}
- nondet ∈ [--..--]
-[eva:loop-unroll:partial] multidim.c:83: loop not completely unrolled
-[eva] multidim.c:83: starting to merge loop iterations
-[eva] multidim.c:85: starting to merge loop iterations
-[eva] multidim.c:89:
- 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] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main4:
- t[0..3] ∈ {42}
-[from] Computing for function main4
-[from] Done for function main4
-[from] ====== DEPENDENCIES COMPUTED ======
- These dependencies hold at termination for the executions that terminate:
-[from] Function main4:
- NO EFFECTS
-[from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main4:
- t[0..3]; i; j
-[inout] Inputs for function main4:
- \nothing
--
GitLab