diff --git a/tests/value/oracle/partitioning-annots.0.res.oracle b/tests/value/oracle/partitioning-annots.0.res.oracle index 2c8c96f8d80e8fe07ec3674832261f7378c6d258..4bf575a86cd583e6667c60fe93145adcf4430756 100644 --- a/tests/value/oracle/partitioning-annots.0.res.oracle +++ b/tests/value/oracle/partitioning-annots.0.res.oracle @@ -3,75 +3,110 @@ [eva] Computing initial state [eva] Initial state computed [eva:initial-state] Values of globals at initialization - k ∈ {0} nondet ∈ [--..--] + k ∈ {0} [eva] computing for function test_slevel <- main. - Called from tests/value/partitioning-annots.c:185. -[eva] tests/value/partitioning-annots.c:150: starting to merge loop iterations -[eva] tests/value/partitioning-annots.c:155: starting to merge loop iterations + Called from tests/value/partitioning-annots.c:205. +[eva] tests/value/partitioning-annots.c:170: starting to merge loop iterations +[eva] tests/value/partitioning-annots.c:175: starting to merge loop iterations [eva] Recording results for test_slevel [eva] Done for function test_slevel [eva] computing for function test_unroll <- main. - Called from tests/value/partitioning-annots.c:186. -[eva:loop-unroll] tests/value/partitioning-annots.c:24: + Called from tests/value/partitioning-annots.c:206. +[eva:loop-unroll] tests/value/partitioning-annots.c:26: loop not completely unrolled -[eva] tests/value/partitioning-annots.c:24: starting to merge loop iterations -[eva:loop-unroll] tests/value/partitioning-annots.c:32: +[eva] tests/value/partitioning-annots.c:26: starting to merge loop iterations +[eva:loop-unroll] tests/value/partitioning-annots.c:34: loop not completely unrolled -[eva] tests/value/partitioning-annots.c:32: starting to merge loop iterations [eva] tests/value/partitioning-annots.c:34: starting to merge loop iterations -[eva:loop-unroll] tests/value/partitioning-annots.c:47: +[eva] tests/value/partitioning-annots.c:36: starting to merge loop iterations +[eva:loop-unroll] tests/value/partitioning-annots.c:49: loop not completely unrolled -[eva] tests/value/partitioning-annots.c:47: starting to merge loop iterations -[eva:loop-unroll] tests/value/partitioning-annots.c:52: +[eva] tests/value/partitioning-annots.c:49: starting to merge loop iterations +[eva:loop-unroll] tests/value/partitioning-annots.c:54: loop not completely unrolled -[eva] tests/value/partitioning-annots.c:52: starting to merge loop iterations +[eva] tests/value/partitioning-annots.c:54: starting to merge loop iterations [eva] Recording results for test_unroll [eva] Done for function test_unroll [eva] computing for function test_split <- main. - Called from tests/value/partitioning-annots.c:187. + Called from tests/value/partitioning-annots.c:207. [eva] computing for function Frama_C_interval <- test_split <- main. - Called from tests/value/partitioning-annots.c:71. + Called from tests/value/partitioning-annots.c:73. [eva] using specification for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:71: +[eva] tests/value/partitioning-annots.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 <- test_split <- main. - Called from tests/value/partitioning-annots.c:72. -[eva] tests/value/partitioning-annots.c:72: + Called from tests/value/partitioning-annots.c:74. +[eva] tests/value/partitioning-annots.c:74: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:78: +[eva] tests/value/partitioning-annots.c:80: Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0} -[eva] tests/value/partitioning-annots.c:81: +[eva] tests/value/partitioning-annots.c:83: Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1} -[eva] tests/value/partitioning-annots.c:81: - Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0} [eva] tests/value/partitioning-annots.c:83: + Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0} +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {1}, {2}, {1} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {1}, {1}, {1} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {1}, {0}, {1} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {0}, {2}, {0} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {0}, {1}, {0} -[eva] tests/value/partitioning-annots.c:83: - Frama_C_show_each_before_first_merge: {0}, {0}, {0} [eva] tests/value/partitioning-annots.c:85: + Frama_C_show_each_before_first_merge: {0}, {0}, {0} +[eva] tests/value/partitioning-annots.c:87: Frama_C_show_each_before_second_merge: {0; 1}, {2}, {0; 1} -[eva] tests/value/partitioning-annots.c:85: +[eva] tests/value/partitioning-annots.c:87: Frama_C_show_each_before_second_merge: {0; 1}, {1}, {0; 1} -[eva] tests/value/partitioning-annots.c:85: - Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1} [eva] tests/value/partitioning-annots.c:87: + Frama_C_show_each_before_second_merge: {0; 1}, {0}, {0; 1} +[eva] tests/value/partitioning-annots.c:89: Frama_C_show_each_end: {0; 1}, {0; 1; 2}, {0; 1} [eva] Recording results for test_split [eva] Done for function test_split +[eva] computing for function test_dynamic_split <- main. + Called from tests/value/partitioning-annots.c:208. +[eva] tests/value/partitioning-annots.c:95: Warning: + this partitioning parameter cannot be evaluated safely on all states +[eva] computing for function Frama_C_interval <- test_dynamic_split <- main. + Called from tests/value/partitioning-annots.c:97. +[eva] tests/value/partitioning-annots.c:97: + function Frama_C_interval: precondition 'order' got status valid. +[eva] Done for function Frama_C_interval +[eva] tests/value/partitioning-annots.c:100: + Frama_C_show_each_split_with_uninit: {2}, {2} +[eva] tests/value/partitioning-annots.c:100: + Frama_C_show_each_split_with_uninit: {1}, {1} +[eva] tests/value/partitioning-annots.c:100: + Frama_C_show_each_split_with_uninit: {0}, {0} +[eva] tests/value/partitioning-annots.c:100: + Frama_C_show_each_split_with_uninit: Bottom, Bottom +[eva] tests/value/partitioning-annots.c:102: + Frama_C_show_each_no_split: {0}, {0; 1; 2} +[eva] computing for function Frama_C_interval <- test_dynamic_split <- main. + Called from tests/value/partitioning-annots.c:103. +[eva] tests/value/partitioning-annots.c:103: + function Frama_C_interval: precondition 'order' got status valid. +[eva] Done for function Frama_C_interval +[eva] tests/value/partitioning-annots.c:107: Frama_C_show_each_split: {0}, {2} +[eva] tests/value/partitioning-annots.c:107: Frama_C_show_each_split: {0}, {1} +[eva] tests/value/partitioning-annots.c:107: Frama_C_show_each_split: {0}, {0} +[eva] tests/value/partitioning-annots.c:109: + Frama_C_show_each_no_split: {0}, {0; 1; 2} +[eva] Recording results for test_dynamic_split +[eva] Done for function test_dynamic_split [eva] Recording results for main [eva] done for function main [eva] ====== VALUES COMPUTED ====== +[eva:final-states] Values at end of function test_dynamic_split: + Frama_C_entropy_source ∈ [--..--] + a ∈ {0} + b ∈ {0; 1; 2} [eva:final-states] Values at end of function test_slevel: a[0..9] ∈ {42} b[0..9] ∈ {42} or UNINITIALIZED @@ -112,11 +147,13 @@ [eva:final-states] Values at end of function main: Frama_C_entropy_source ∈ [--..--] k ∈ {0; 1} +[from] Computing for function test_dynamic_split +[from] Computing for function Frama_C_interval <-test_dynamic_split +[from] Done for function Frama_C_interval +[from] Done for function test_dynamic_split [from] Computing for function test_slevel [from] Done for function test_slevel [from] Computing for function test_split -[from] Computing for function Frama_C_interval <-test_split -[from] Done for function Frama_C_interval [from] Done for function test_split [from] Computing for function test_unroll [from] Done for function test_unroll @@ -127,6 +164,8 @@ [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 test_dynamic_split: + Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF) [from] Function test_slevel: NO EFFECTS [from] Function test_split: @@ -135,9 +174,13 @@ [from] Function test_unroll: NO EFFECTS [from] Function main: - Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF) + Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF) k FROM Frama_C_entropy_source [from] ====== END OF DEPENDENCIES ====== +[inout] Out (internal) for function test_dynamic_split: + Frama_C_entropy_source; a; b +[inout] Inputs for function test_dynamic_split: + Frama_C_entropy_source; nondet [inout] Out (internal) for function test_slevel: a[0..9]; b[0..9]; c[0..9]; d[0..9]; e[0..3]; i; i_0; i_1; i_2; i_3 [inout] Inputs for function test_slevel: @@ -154,4 +197,4 @@ [inout] Out (internal) for function main: Frama_C_entropy_source; k [inout] Inputs for function main: - Frama_C_entropy_source; k; nondet + Frama_C_entropy_source; nondet; k diff --git a/tests/value/oracle/partitioning-annots.1.res.oracle b/tests/value/oracle/partitioning-annots.1.res.oracle index 4c75b70926ab40b8ea13caf8ecdca906ab2294bb..10704f7b9a550d3d2fa4c500be708b4ec8206f79 100644 --- a/tests/value/oracle/partitioning-annots.1.res.oracle +++ b/tests/value/oracle/partitioning-annots.1.res.oracle @@ -3,52 +3,52 @@ [eva] Computing initial state [eva] Initial state computed [eva:initial-state] Values of globals at initialization - k ∈ {0} nondet ∈ [--..--] + k ∈ {0} [eva] computing for function Frama_C_interval <- test_split. - Called from tests/value/partitioning-annots.c:71. + Called from tests/value/partitioning-annots.c:73. [eva] using specification for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:71: +[eva] tests/value/partitioning-annots.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 <- test_split. - Called from tests/value/partitioning-annots.c:72. -[eva] tests/value/partitioning-annots.c:72: + Called from tests/value/partitioning-annots.c:74. +[eva] tests/value/partitioning-annots.c:74: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:78: +[eva] tests/value/partitioning-annots.c:80: Frama_C_show_each_before_first_split: {0; 1}, {0; 1; 2}, {0} -[eva] tests/value/partitioning-annots.c:81: +[eva] tests/value/partitioning-annots.c:83: Frama_C_show_each_before_second_split: {1}, {0; 1; 2}, {1} -[eva] tests/value/partitioning-annots.c:81: - Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0} [eva] tests/value/partitioning-annots.c:83: + Frama_C_show_each_before_second_split: {0}, {0; 1; 2}, {0} +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {1}, {2}, {1} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {1}, {1}, {1} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {1}, {0}, {1} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {0}, {2}, {0} -[eva] tests/value/partitioning-annots.c:83: +[eva] tests/value/partitioning-annots.c:85: Frama_C_show_each_before_first_merge: {0}, {1}, {0} -[eva] tests/value/partitioning-annots.c:83: - Frama_C_show_each_before_first_merge: {0}, {0}, {0} [eva] tests/value/partitioning-annots.c:85: + Frama_C_show_each_before_first_merge: {0}, {0}, {0} +[eva] tests/value/partitioning-annots.c:87: Frama_C_show_each_before_second_merge: {1}, {2}, {1} -[eva] tests/value/partitioning-annots.c:85: +[eva] tests/value/partitioning-annots.c:87: Frama_C_show_each_before_second_merge: {1}, {1}, {1} -[eva] tests/value/partitioning-annots.c:85: +[eva] tests/value/partitioning-annots.c:87: Frama_C_show_each_before_second_merge: {1}, {0}, {1} -[eva] tests/value/partitioning-annots.c:85: +[eva] tests/value/partitioning-annots.c:87: Frama_C_show_each_before_second_merge: {0}, {2}, {0} -[eva] tests/value/partitioning-annots.c:85: +[eva] tests/value/partitioning-annots.c:87: Frama_C_show_each_before_second_merge: {0}, {1}, {0} -[eva] tests/value/partitioning-annots.c:85: - Frama_C_show_each_before_second_merge: {0}, {0}, {0} [eva] tests/value/partitioning-annots.c:87: + Frama_C_show_each_before_second_merge: {0}, {0}, {0} +[eva] tests/value/partitioning-annots.c:89: Frama_C_show_each_end: {1}, {0; 1; 2}, {1} -[eva] tests/value/partitioning-annots.c:87: +[eva] tests/value/partitioning-annots.c:89: Frama_C_show_each_end: {0}, {0; 1; 2}, {0} [eva] Recording results for test_split [eva] done for function test_split diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle index c2bbd71dfb8fe7ec0378ff78a76d09e3cd628d89..da1dee03a864d7ec4bfbbfcafaa36a21158a914f 100644 --- a/tests/value/oracle/partitioning-annots.2.res.oracle +++ b/tests/value/oracle/partitioning-annots.2.res.oracle @@ -3,44 +3,44 @@ [eva] Computing initial state [eva] Initial state computed [eva:initial-state] Values of globals at initialization - k ∈ {0} nondet ∈ [--..--] + k ∈ {0} [eva] computing for function Frama_C_interval <- test_loop_split. - Called from tests/value/partitioning-annots.c:105. + Called from tests/value/partitioning-annots.c:127. [eva] using specification for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:105: +[eva] tests/value/partitioning-annots.c:127: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval [eva] computing for function Frama_C_interval <- test_loop_split. - Called from tests/value/partitioning-annots.c:105. + Called from tests/value/partitioning-annots.c:127. [eva] Done for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:103: starting to merge loop iterations +[eva] tests/value/partitioning-annots.c:125: starting to merge loop iterations [eva] computing for function Frama_C_interval <- test_loop_split. - Called from tests/value/partitioning-annots.c:105. + Called from tests/value/partitioning-annots.c:127. [eva] Done for function Frama_C_interval [eva] computing for function Frama_C_interval <- test_loop_split. - Called from tests/value/partitioning-annots.c:105. + Called from tests/value/partitioning-annots.c:127. [eva] Done for function Frama_C_interval [eva] computing for function Frama_C_interval <- test_loop_split. - Called from tests/value/partitioning-annots.c:105. + Called from tests/value/partitioning-annots.c:127. [eva] Done for function Frama_C_interval [eva] computing for function Frama_C_interval <- test_loop_split. - Called from tests/value/partitioning-annots.c:105. + Called from tests/value/partitioning-annots.c:127. [eva] Done for function Frama_C_interval -[eva:alarm] tests/value/partitioning-annots.c:112: Warning: +[eva:alarm] tests/value/partitioning-annots.c:134: Warning: accessing uninitialized left-value. assert \initialized(&A[i]); -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {9}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {8}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {7}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {6}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {5}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {4}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {3}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {2}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {1}, {42} -[eva] tests/value/partitioning-annots.c:117: Frama_C_show_each: {0}, {42} -[eva] tests/value/partitioning-annots.c:118: assertion got status valid. -[eva] tests/value/partitioning-annots.c:121: +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {9}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {8}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {7}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {6}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {5}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {4}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {3}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {2}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {1}, {42} +[eva] tests/value/partitioning-annots.c:139: Frama_C_show_each: {0}, {42} +[eva] tests/value/partitioning-annots.c:140: assertion got status valid. +[eva] tests/value/partitioning-annots.c:143: Frama_C_show_each: {{ "Value 42 not found" }} [eva] Recording results for test_loop_split [eva] done for function test_loop_split diff --git a/tests/value/oracle/partitioning-annots.3.res.oracle b/tests/value/oracle/partitioning-annots.3.res.oracle index f319bc5df3899a9179b08822c8c6d8bc60113af6..eeb698d400e482bf2fb9c492d5f74fe2fb0b81fd 100644 --- a/tests/value/oracle/partitioning-annots.3.res.oracle +++ b/tests/value/oracle/partitioning-annots.3.res.oracle @@ -3,16 +3,16 @@ [eva] Computing initial state [eva] Initial state computed [eva:initial-state] Values of globals at initialization - k ∈ {0} nondet ∈ [--..--] + k ∈ {0} [eva] computing for function Frama_C_interval <- test_history. - Called from tests/value/partitioning-annots.c:127. + Called from tests/value/partitioning-annots.c:149. [eva] using specification for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:127: +[eva] tests/value/partitioning-annots.c:149: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {0; 1}, {0; 1} -[eva:alarm] tests/value/partitioning-annots.c:136: Warning: +[eva] tests/value/partitioning-annots.c:155: Frama_C_show_each: {0; 1}, {0; 1} +[eva:alarm] tests/value/partitioning-annots.c:158: Warning: division by zero. assert j ≢ 0; [eva] Recording results for test_history [eva] done for function test_history diff --git a/tests/value/oracle/partitioning-annots.4.res.oracle b/tests/value/oracle/partitioning-annots.4.res.oracle index 22626883a487f3d89ad6232c24cbf73ee118053b..1718f8213307143be4ea8df27c930e7540c14ba9 100644 --- a/tests/value/oracle/partitioning-annots.4.res.oracle +++ b/tests/value/oracle/partitioning-annots.4.res.oracle @@ -3,16 +3,16 @@ [eva] Computing initial state [eva] Initial state computed [eva:initial-state] Values of globals at initialization - k ∈ {0} nondet ∈ [--..--] + k ∈ {0} [eva] computing for function Frama_C_interval <- test_history. - Called from tests/value/partitioning-annots.c:127. + Called from tests/value/partitioning-annots.c:149. [eva] using specification for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:127: +[eva] tests/value/partitioning-annots.c:149: function Frama_C_interval: precondition 'order' got status valid. [eva] Done for function Frama_C_interval -[eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {0}, {0} -[eva] tests/value/partitioning-annots.c:133: Frama_C_show_each: {1}, {1} +[eva] tests/value/partitioning-annots.c:155: Frama_C_show_each: {0}, {0} +[eva] tests/value/partitioning-annots.c:155: Frama_C_show_each: {1}, {1} [eva] Recording results for test_history [eva] done for function test_history [eva] ====== VALUES COMPUTED ====== diff --git a/tests/value/partitioning-annots.c b/tests/value/partitioning-annots.c index c84390f8c985153d00669cd4fecc7d984cef4ed8..a0a6b0161c0fe51695fbf948f723a10cda7e372e 100644 --- a/tests/value/partitioning-annots.c +++ b/tests/value/partitioning-annots.c @@ -11,6 +11,8 @@ #define N 10 +volatile nondet; + void test_unroll() { int a[N], b[N], c[2*N], d[2*N], e[N]; @@ -87,6 +89,26 @@ void test_split() Frama_C_show_each_end(i,j,k); } +void test_dynamic_split() +{ + int a, b; + //@ dynamic_split a; + if (nondet) { + a = Frama_C_interval(0, 2); + b = a; + } + Frama_C_show_each_split_with_uninit(a, b); + a = 0; + Frama_C_show_each_no_split(a, b); + a = Frama_C_interval(0, 2); + b = a; + //@ split a; + a = 0; + Frama_C_show_each_split(a, b); + //@ merge a; + Frama_C_show_each_no_split(a, b); +} + void test_loop_split() { int A[N]; @@ -136,8 +158,6 @@ void test_history() k = k / j; } -volatile nondet; - void test_slevel() { int a[N], b[N], c[N], d[N], e[4]; @@ -185,5 +205,6 @@ void main(void) test_slevel(); test_unroll(); test_split(); + test_dynamic_split(); }