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

[Eva] multidim: update test

parent 7518364c
No related branches found
No related tags found
No related merge requests found
[kernel] Parsing tests/value/multidim-relations.c (with preprocessing)
[kernel] Parsing multidim-relations.c (with preprocessing)
[eva:experimental] Warning: The multidim domain is experimental.
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
......@@ -8,42 +8,42 @@
g ∈ {0}
h ∈ {1}
[eva] computing for function init_array <- main.
Called from tests/value/multidim-relations.c:35.
[eva] tests/value/multidim-relations.c:18: starting to merge loop iterations
[kernel] tests/value/multidim-relations.c:19:
Called from multidim-relations.c:35.
[eva] multidim-relations.c:18: starting to merge loop iterations
[kernel] multidim-relations.c:19:
more than 1(350) locations to update in array. Approximating.
[kernel] tests/value/multidim-relations.c:20:
[kernel] multidim-relations.c:20:
more than 1(350) locations to update in array. Approximating.
[kernel] tests/value/multidim-relations.c:21:
[kernel] multidim-relations.c:21:
more than 1(175) locations to update in array. Approximating.
[eva] Recording results for init_array
[kernel] tests/value/multidim-relations.c:19:
[kernel] multidim-relations.c:19:
more than 1(350) elements to enumerate. Approximating.
[kernel] tests/value/multidim-relations.c:20:
[kernel] multidim-relations.c:20:
more than 1(350) elements to enumerate. Approximating.
[kernel] tests/value/multidim-relations.c:21:
[kernel] multidim-relations.c:21:
more than 1(175) elements to enumerate. Approximating.
[eva] Done for function init_array
[eva] computing for function set_null <- main.
Called from tests/value/multidim-relations.c:36.
Called from multidim-relations.c:36.
[eva] Recording results for set_null
[eva] Done for function set_null
[eva] computing for function set_null <- main.
Called from tests/value/multidim-relations.c:37.
Called from multidim-relations.c:37.
[eva] Recording results for set_null
[eva] Done for function set_null
[eva] computing for function Frama_C_interval <- main.
Called from tests/value/multidim-relations.c:38.
Called from multidim-relations.c:38.
[eva] using specification for function Frama_C_interval
[eva] tests/value/multidim-relations.c:38:
[eva] multidim-relations.c:38:
function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval
[eva] computing for function use_array <- main.
Called from tests/value/multidim-relations.c:40.
[eva:alarm] tests/value/multidim-relations.c:31: Warning:
Called from multidim-relations.c:40.
[eva:alarm] multidim-relations.c:31: Warning:
out of bounds read. assert \valid_read(t[index].ptr);
[eva] Recording results for use_array
[kernel] tests/value/multidim-relations.c:31:
[kernel] multidim-relations.c:31:
more than 1(350) elements to enumerate. Approximating.
[eva] Done for function use_array
[eva] Recording results for main
......@@ -53,84 +53,60 @@
t[0]{.kind; .[bits 8 to 31]#} ∈ {0; 1} repeated %8
[0].value ∈ [--..--]
[0].ptr ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:19}) }}
[1].kind ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:18}) }}
[1].[bits 8 to 31] ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:19}) }}
[1].value ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:18}) }}
[1].ptr ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[2].kind ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:18}) }}
[2].[bits 8 to 31] ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[2].value ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:18}) }}
{[2].ptr; [3..348]} ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[349].kind ∈
{{ garbled mix of &{g}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g} (origin: Merge {multidim-relations.c:19}) }}
[349]{.value; .[bits 8 to 31]} ∈
{{ garbled mix of &{g}
(origin: Merge {tests/value/multidim-relations.c:21}) }}
{{ garbled mix of &{g} (origin: Merge {multidim-relations.c:21}) }}
[349].ptr ∈ {{ NULL ; &g }}
i ∈ {350}
[eva:final-states] Values at end of function set_null:
t[0]{.kind; .[bits 8 to 31]#} ∈ {0; 1} repeated %8
[0].value ∈ [--..--]
[0].ptr ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:19}) }}
[1].kind ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:18}) }}
[1].[bits 8 to 31] ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:19}) }}
[1].value ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:18}) }}
[1].ptr ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[2].kind ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:18}) }}
[2].[bits 8 to 31] ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[2].value ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:18}) }}
{[2].ptr; [3..56]} ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[57].kind ∈ {0}
[57]{.value; .[bits 8 to 31]} ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[57].ptr ∈ {0}
[58..348] ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[349].kind ∈
{{ garbled mix of &{g}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g} (origin: Merge {multidim-relations.c:19}) }}
[349]{.value; .[bits 8 to 31]} ∈
{{ garbled mix of &{g}
(origin: Merge {tests/value/multidim-relations.c:21}) }}
{{ garbled mix of &{g} (origin: Merge {multidim-relations.c:21}) }}
[349].ptr ∈ {{ NULL ; &g }}
[eva:final-states] Values at end of function use_array:
result ∈ {0; 1}
......@@ -139,62 +115,47 @@
t[0]{.kind; .[bits 8 to 31]#} ∈ {0; 1} repeated %8
[0].value ∈ [--..--]
[0].ptr ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:19}) }}
[1].kind ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:18}) }}
[1].[bits 8 to 31] ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:19}) }}
[1].value ∈
{{ garbled mix of &{h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{h} (origin: Merge {multidim-relations.c:18}) }}
[1].ptr ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[2].kind ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:18}) }}
[2].[bits 8 to 31] ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[2].value ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:18}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:18}) }}
{[2].ptr; [3..56]} ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[57].kind ∈ {0}
[57]{.value; .[bits 8 to 31]} ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[57].ptr ∈ {0}
[58..140] ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[141].kind ∈ {0}
[141]{.value; .[bits 8 to 31]} ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[141].ptr ∈ {0}
[142..348] ∈
{{ garbled mix of &{g; h}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g; h} (origin: Merge {multidim-relations.c:19}) }}
[349].kind ∈
{{ garbled mix of &{g}
(origin: Merge {tests/value/multidim-relations.c:19}) }}
{{ garbled mix of &{g} (origin: Merge {multidim-relations.c:19}) }}
[349]{.value; .[bits 8 to 31]} ∈
{{ garbled mix of &{g}
(origin: Merge {tests/value/multidim-relations.c:21}) }}
{{ garbled mix of &{g} (origin: Merge {multidim-relations.c:21}) }}
[349].ptr ∈ {{ NULL ; &g }}
index ∈ [0..349]
[from] Computing for function init_array
[kernel] tests/value/multidim-relations.c:19:
[kernel] multidim-relations.c:19:
more than 1(350) dependencies to update. Approximating.
[kernel] tests/value/multidim-relations.c:20:
[kernel] multidim-relations.c:20:
more than 1(350) dependencies to update. Approximating.
[kernel] tests/value/multidim-relations.c:21:
[kernel] multidim-relations.c:21:
more than 1(175) dependencies to update. Approximating.
[from] Done for function init_array
[from] Computing for function set_null
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment