[Eva] Adds a test of a dynamic split on an ACSL predicate.

tests/value/oracle/partitioning-annots.0.res.oracle

@@ -89,6 +89,11 @@
 [eva] 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] computing for function test_dynamic_split_predicate <- main.
+  Called from partitioning-annots.c:227.
+[eva] partitioning-annots.c:124: starting to merge loop iterations
+[eva] Recording results for test_dynamic_split_predicate
+[eva] Done for function test_dynamic_split_predicate
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
@@ -96,6 +101,10 @@
   Frama_C_entropy_source ∈ [--..--]
   a ∈ {0}
   b ∈ {0; 1; 2}
+[eva:final-states] Values at end of function test_dynamic_split_predicate:
+  x ∈ [0..44]
+  y ∈ [0..44]
+  c ∈ [--..--]
 [eva:final-states] Values at end of function test_slevel:
   a[0..9] ∈ {42}
   b[0..9] ∈ {42} or UNINITIALIZED
@@ -140,6 +149,8 @@
 [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_dynamic_split_predicate
+[from] Done for function test_dynamic_split_predicate
 [from] Computing for function test_slevel
 [from] Done for function test_slevel
 [from] Computing for function test_split
@@ -155,6 +166,8 @@
   \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_dynamic_split_predicate:
+  NO EFFECTS
 [from] Function test_slevel:
   NO EFFECTS
 [from] Function test_split:
@@ -170,6 +183,10 @@
     Frama_C_entropy_source; a; b
 [inout] Inputs for function test_dynamic_split:
     Frama_C_entropy_source; nondet
+[inout] Out (internal) for function test_dynamic_split_predicate:
+    x; y; c; i
+[inout] Inputs for function test_dynamic_split_predicate:
+    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:

tests/value/partitioning-annots.c

@@ -109,23 +109,23 @@ void test_dynamic_split()
   Frama_C_show_each_no_split(a, b);
 }
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+void test_dynamic_split_predicate()
+{
+  int x, y;
+  //@ dynamic_split \initialized(&x);
+  int c = nondet;
+  if (c != 1) {
+    x = 42;
+  }
+  y = 2;
+  if (c != 1)
+    x += y; // No alarm on x initialization with the dynamic partitioning.
+  else {
+    for (int i = 0; i < 32; i++)
+      x = i;
+  }
+  y = x; // No alarm on x initialization with the dynamic partitioning.
+}
 
 void test_loop_split()
 {
@@ -224,4 +224,5 @@ void main(void)
   test_unroll();
   test_split();
   test_dynamic_split();
+  test_dynamic_split_predicate();
 }