diff --git a/tests/value/multidim.c b/tests/value/multidim.c index 16853e329c422f2741c43adf16ee6403152bfdfe..60ac31b0ddde170be56ddd133bec1382b167ec88 100644 --- a/tests/value/multidim.c +++ b/tests/value/multidim.c @@ -169,6 +169,20 @@ void main8(void) { Frama_C_domain_show_each(t); } +void main9(void) { + int t1[10], t2[10]; + //@ eva_domain_scope multidim,t1; + + for (int i = 0 ; i < 10 ; i++) { + //@ eva_domain_scope multidim,i; + t1[i] = 0; + t2[i] = 0; + } + + Frama_C_domain_show_each(t1, t2); +} + + void main(s x) { main1(x); main2(); @@ -178,4 +192,5 @@ void main(s x) { main6(); main7(); main8(); + main9(); } diff --git a/tests/value/oracle/multidim.res.oracle b/tests/value/oracle/multidim.res.oracle index 634b46a94bfb621d05be1133b608b0fa10ab9f00..fb4bb1d3533963d673aaff3181e56d9f3bb0a472 100644 --- a/tests/value/oracle/multidim.res.oracle +++ b/tests/value/oracle/multidim.res.oracle @@ -9,7 +9,7 @@ z[0..3] ∈ {0} nondet ∈ [--..--] [eva] computing for function main1 <- main. - Called from multidim.c:173. + Called from multidim.c:187. [eva] multidim.c:39: Frama_C_domain_show_each: x : # cvalue: .t1[0].f ∈ [-3.40282346639e+38 .. 3.40282346639e+38] @@ -86,7 +86,7 @@ [eva] Recording results for main1 [eva] Done for function main1 [eva] computing for function main2 <- main. - Called from multidim.c:174. + Called from multidim.c:188. [eva] multidim.c:55: starting to merge loop iterations [eva:alarm] multidim.c:58: Warning: check got status unknown. [eva] multidim.c:59: @@ -96,7 +96,7 @@ [eva] Recording results for main2 [eva] Done for function main2 [eva] computing for function main3 <- main. - Called from multidim.c:175. + Called from multidim.c:189. [eva] multidim.c:64: starting to merge loop iterations [eva] multidim.c:63: starting to merge loop iterations [kernel] multidim.c:65: @@ -137,7 +137,7 @@ [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:176. + Called from multidim.c:190. [eva:loop-unroll:partial] multidim.c:81: loop not completely unrolled [eva] multidim.c:81: starting to merge loop iterations [eva] multidim.c:83: starting to merge loop iterations @@ -148,7 +148,7 @@ [eva] Recording results for main4 [eva] Done for function main4 [eva] computing for function main5 <- main. - Called from multidim.c:177. + Called from multidim.c:191. [eva] multidim.c:96: starting to merge loop iterations [eva] multidim.c:106: Frama_C_domain_show_each: @@ -163,7 +163,7 @@ [eva] Recording results for main5 [eva] Done for function main5 [eva] computing for function main6 <- main. - Called from multidim.c:178. + Called from multidim.c:192. [eva] multidim.c:114: Trace partitioning superposing up to 100 states [eva] multidim.c:118: Frama_C_domain_show_each: @@ -181,7 +181,7 @@ [eva] Recording results for main6 [eva] Done for function main6 [eva] computing for function main7 <- main. - Called from multidim.c:179. + Called from multidim.c:193. [eva] multidim.c:134: starting to merge loop iterations [kernel] multidim.c:136: more than 1(1000) locations to update in array. Approximating. @@ -214,7 +214,7 @@ [kernel] multidim.c:137: more than 1(1000) elements to enumerate. Approximating. [eva] Done for function main7 [eva] computing for function main8 <- main. - Called from multidim.c:180. + Called from multidim.c:194. [eva] multidim.c:165: starting to merge loop iterations [eva] multidim.c:169: Frama_C_domain_show_each: @@ -222,6 +222,17 @@ # multidim: { [0 .. 9] = {1}, [10 .. 9] = {0} } [eva] Recording results for main8 [eva] Done for function main8 +[eva] computing for function main9 <- main. + Called from multidim.c:195. +[eva] multidim.c:176: starting to merge loop iterations +[eva] multidim.c:182: + Frama_C_domain_show_each: + t1 : # cvalue: {0} or UNINITIALIZED + # multidim: [0 .. 9] = {0} or UNINITIALIZED + t2 : # cvalue: {0} or UNINITIALIZED + # multidim: UNINITIALIZED +[eva] Recording results for main9 +[eva] Done for function main9 [eva] Recording results for main [eva] done for function main [kernel] multidim.c:50: more than 1(28) elements to enumerate. Approximating. @@ -255,6 +266,9 @@ [eva:final-states] Values at end of function main8: t[0..9] ∈ {0; 1} p ∈ {{ &t[0] }} +[eva:final-states] Values at end of function main9: + t1[0..9] ∈ {0} or UNINITIALIZED + t2[0..9] ∈ {0} or UNINITIALIZED [eva:final-states] Values at end of function main: Frama_C_entropy_source ∈ [--..--] z[0..3] ∈ [--..--] @@ -288,6 +302,8 @@ [from] Done for function main7 [from] Computing for function main8 [from] Done for function main8 +[from] Computing for function main9 +[from] Done for function main9 [from] Computing for function main [from] Done for function main [from] ====== DEPENDENCIES COMPUTED ====== @@ -314,6 +330,8 @@ Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF) [from] Function main8: NO EFFECTS +[from] Function main9: + NO EFFECTS [from] Function main: Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF) z[0..3] FROM \nothing @@ -350,6 +368,10 @@ t[0..9]; p; i [inout] Inputs for function main8: \nothing +[inout] Out (internal) for function main9: + t1[0..9]; t2[0..9]; i +[inout] Inputs for function main9: + \nothing [inout] Out (internal) for function main: Frama_C_entropy_source; z[0..3] [inout] Inputs for function main: