[Eva] Adds a test of splits according to the returning value of a call.

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

@@ -6,13 +6,13 @@
   nondet ∈ [--..--]
   k ∈ {0}
 [eva] computing for function test_slevel <- main.
-  Called from partitioning-annots.c:223.
-[eva] partitioning-annots.c:188: starting to merge loop iterations
-[eva] partitioning-annots.c:193: starting to merge loop iterations
+  Called from partitioning-annots.c:278.
+[eva] partitioning-annots.c:243: starting to merge loop iterations
+[eva] partitioning-annots.c:248: 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 partitioning-annots.c:224.
+  Called from partitioning-annots.c:279.
 [eva:loop-unroll:partial] partitioning-annots.c:26: loop not completely unrolled
 [eva] partitioning-annots.c:26: starting to merge loop iterations
 [eva:loop-unroll:partial] partitioning-annots.c:34: loop not completely unrolled
@@ -25,7 +25,7 @@
 [eva] Recording results for test_unroll
 [eva] Done for function test_unroll
 [eva] computing for function test_split <- main.
-  Called from partitioning-annots.c:225.
+  Called from partitioning-annots.c:280.
 [eva] computing for function Frama_C_interval <- test_split <- main.
   Called from partitioning-annots.c:73.
 [eva] using specification for function Frama_C_interval
@@ -65,7 +65,7 @@
 [eva] Recording results for test_split
 [eva] Done for function test_split
 [eva] computing for function test_dynamic_split <- main.
-  Called from partitioning-annots.c:226.
+  Called from partitioning-annots.c:281.
 [eva] 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.
@@ -90,13 +90,44 @@
 [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.
+  Called from partitioning-annots.c:282.
 [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] computing for function test_splits_post_call <- main.
+  Called from partitioning-annots.c:283.
+[eva] computing for function Frama_C_interval <- test_splits_post_call <- main.
+  Called from partitioning-annots.c:205.
+[eva] partitioning-annots.c:205: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function spec <- test_splits_post_call <- main.
+  Called from partitioning-annots.c:206.
+[eva] using specification for function spec
+[eva] Done for function spec
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: [-2147483648..-10], ⊥
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: [10..2147483647], ⊥
+[eva] partitioning-annots.c:211: Frama_C_show_each_spec: {-1}, [-1000..1000]
+[eva] computing for function body <- test_splits_post_call <- main.
+  Called from partitioning-annots.c:212.
+[eva] Recording results for body
+[eva] Done for function body
+[eva] partitioning-annots.c:212: Reusing old results for call to body
+[eva] partitioning-annots.c:212: Reusing old results for call to body
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: [-510..-10], ⊥
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: [10..510], ⊥
+[eva] partitioning-annots.c:217: Frama_C_show_each_body: {-1}, [-1000..1000]
+[eva] Recording results for test_splits_post_call
+[eva] Done for function test_splits_post_call
 [eva] Recording results for main
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function body:
+  i2 ∈ [-500..500]
+  absolute ∈ [0..500]
+  state ∈ {-1; 0; 1}
+  y ∈ [-1000..1000] or UNINITIALIZED
+  __retres ∈ [-510..510]
 [eva:final-states] Values at end of function test_dynamic_split:
   Frama_C_entropy_source ∈ [--..--]
   a ∈ {0}
@@ -117,6 +148,13 @@
   k ∈ {0; 1}
   i ∈ {0; 1}
   j ∈ {0; 1; 2}
+[eva:final-states] Values at end of function test_splits_post_call:
+  Frama_C_entropy_source ∈ [--..--]
+  x ∈ [-1000..1000] or UNINITIALIZED
+  y ∈ [-1000..1000] or UNINITIALIZED
+  error ∈ [-1000..1000] or UNINITIALIZED
+  i ∈ [-1000..1000]
+  r ∈ [-510..510]
 [eva:final-states] Values at end of function test_unroll:
   a[0..9] ∈ {42}
   b[0..9] ∈ {42}
@@ -145,6 +183,8 @@
 [eva:final-states] Values at end of function main:
   Frama_C_entropy_source ∈ [--..--]
   k ∈ {0; 1}
+[from] Computing for function body
+[from] Done for function body
 [from] Computing for function test_dynamic_split
 [from] Computing for function Frama_C_interval <-test_dynamic_split
 [from] Done for function Frama_C_interval
@@ -155,6 +195,10 @@
 [from] Done for function test_slevel
 [from] Computing for function test_split
 [from] Done for function test_split
+[from] Computing for function test_splits_post_call
+[from] Computing for function spec <-test_splits_post_call
+[from] Done for function spec
+[from] Done for function test_splits_post_call
 [from] Computing for function test_unroll
 [from] Done for function test_unroll
 [from] Computing for function main
@@ -164,6 +208,12 @@
 [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 body:
+  y FROM nondet; i; p (and SELF)
+  \result FROM nondet; i
+[from] Function spec:
+  x FROM i
+  \result FROM i
 [from] Function test_dynamic_split:
   Frama_C_entropy_source FROM Frama_C_entropy_source; nondet (and SELF)
 [from] Function test_dynamic_split_predicate:
@@ -173,12 +223,18 @@
 [from] Function test_split:
   Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
   k FROM Frama_C_entropy_source
+[from] Function test_splits_post_call:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
 [from] Function test_unroll:
   NO EFFECTS
 [from] Function main:
   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 body:
+    i2; absolute; tmp; state; y; __retres
+[inout] Inputs for function body:
+    nondet
 [inout] Out (internal) for function test_dynamic_split:
     Frama_C_entropy_source; a; b
 [inout] Inputs for function test_dynamic_split:
@@ -195,6 +251,10 @@
     Frama_C_entropy_source; k; i; j
 [inout] Inputs for function test_split:
     Frama_C_entropy_source; k
+[inout] Out (internal) for function test_splits_post_call:
+    Frama_C_entropy_source; x; y; error; i; r
+[inout] Inputs for function test_splits_post_call:
+    Frama_C_entropy_source; nondet
 [inout] Out (internal) for function test_unroll:
     a[0..9]; b[0..9]; c[0..19]; d[0..19]; e[0..9]; i; j; i_0; j_0; i_1; 
     i_2; i_3; j_1

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

@@ -6,13 +6,13 @@
   nondet ∈ [--..--]
   k ∈ {0}
 [eva] computing for function Frama_C_interval <- test_history.
-  Called from partitioning-annots.c:167.
+  Called from partitioning-annots.c:222.
 [eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:167: 
+[eva] partitioning-annots.c:222: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:173: Frama_C_show_each: {0; 1}, {0; 1}
-[eva:alarm] partitioning-annots.c:176: Warning: 
+[eva] partitioning-annots.c:228: Frama_C_show_each: {0; 1}, {0; 1}
+[eva:alarm] partitioning-annots.c:231: Warning: 
   division by zero. assert j ≢ 0;
 [eva] Recording results for test_history
 [eva] done for function test_history

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

@@ -6,13 +6,13 @@
   nondet ∈ [--..--]
   k ∈ {0}
 [eva] computing for function Frama_C_interval <- test_history.
-  Called from partitioning-annots.c:167.
+  Called from partitioning-annots.c:222.
 [eva] using specification for function Frama_C_interval
-[eva] partitioning-annots.c:167: 
+[eva] partitioning-annots.c:222: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] partitioning-annots.c:173: Frama_C_show_each: {0}, {0}
-[eva] partitioning-annots.c:173: Frama_C_show_each: {1}, {1}
+[eva] partitioning-annots.c:228: Frama_C_show_each: {0}, {0}
+[eva] partitioning-annots.c:228: Frama_C_show_each: {1}, {1}
 [eva] Recording results for test_history
 [eva] done for function test_history
 [eva] ====== VALUES COMPUTED ======

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

-105,106c105,106
+115,116c115,122
+< [eva] partitioning-annots.c:212: Reusing old results for call to body
+< [eva] partitioning-annots.c:212: Reusing old results for call to body
+---
+> [eva] computing for function body <- test_splits_post_call <- main.
+>   Called from partitioning-annots.c:212.
+> [eva] Recording results for body
+> [eva] Done for function body
+> [eva] computing for function body <- test_splits_post_call <- main.
+>   Called from partitioning-annots.c:212.
+> [eva] Recording results for body
+> [eva] Done for function body
+136,137c142,143
 <   x ∈ [0..44]
 <   y ∈ [0..44]
 ---

tests/value/oracle_apron/partitioning-annots.3.res.oracle

 15,16d14
-< [eva:alarm] partitioning-annots.c:176: Warning: 
+< [eva:alarm] partitioning-annots.c:231: Warning: 
 <   division by zero. assert j ≢ 0;

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

-105,106c105,106
+136,137c136,137
 <   x ∈ [0..44]
 <   y ∈ [0..44]
 ---

tests/value/partitioning-annots.c

@@ -162,6 +162,61 @@ void test_loop_split()
   }
 }
 
+/*@
+   assigns \result, *p \from i;
+   behavior error:
+     assumes nondet == 0;
+     assigns \result, *p \from i;
+     ensures \result == -1;
+     ensures \initialized(p) && *p == \old(i);
+   behavior positive:
+     assumes nondet > 0;
+     assigns \result \from i;
+     ensures \result >= 10;
+   behavior negative:
+     assumes nondet < 0;
+     assigns \result \from i;
+     ensures \result <= -10;
+   disjoint behaviors;
+   complete behaviors;
+*/
+int spec(int i, int* p);
+
+int body(int i, int *p) {
+  int i2 = i / 2;
+  int absolute = i2 < 0 ? -i2 : i2;
+  int state = nondet % 2;
+  //@ split state;
+  if (state < 0)
+    return - 10 - absolute;
+  if (state > 0)
+    return 10 + absolute;
+  *p = i;
+  return -1;
+}
+
+/* Tests the application of multiple splits according to the return value of a
+   call, to keep in the caller some state partitioning from the callee.
+   The splits must be defined after the call, so the state partitioning from the
+   callee must be kept until all splits are performed.
+   Tests this whether the function body or a specification is used. */
+void test_splits_post_call (void) {
+  int x, y, error;
+  int i = Frama_C_interval(-1000, 1000);
+  int r = spec(i, &x);
+  //@ split r < -1;
+  //@ split r > -1;
+  if (r == -1)
+    error = x; // There should be no alarm.
+  Frama_C_show_each_spec(r, x); // There should be three states.
+  r = body(i, &y);
+  //@ split r < -1;
+  //@ split r > -1;
+  if (r == -1)
+    error = y; // There should be no alarm.
+  Frama_C_show_each_body(r, y); // There should be three states.
+}
+
 void test_history()
 {
   int i = Frama_C_interval(0,1);
@@ -225,4 +280,5 @@ void main(void)
   test_split();
   test_dynamic_split();
   test_dynamic_split_predicate();
+  test_splits_post_call();
 }