[Eva] multidim: add a test for eva_domain_scope

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();
 }

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: