diff --git a/tests/value/oracle/multidim-relations.res.oracle b/tests/value/oracle/multidim-relations.res.oracle index 37dd8d96be94bd379abf5f8bcb2c5770704d82c0..da6ceeabd1743c7d0e0475bf834dcd2ac42580c8 100644 --- a/tests/value/oracle/multidim-relations.res.oracle +++ b/tests/value/oracle/multidim-relations.res.oracle @@ -1,4 +1,4 @@ -[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