[Eva] Add a test for interprocedural splits

tests/value/oracle/partitioning-interproc.2.res.oracle

+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at fabs_splits_test
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] computing for function fabs_splits <- fabs_splits_test.
+  Called from tests/value/partitioning-interproc.c:71.
+[eva] Recording results for fabs_splits
+[eva] Done for function fabs_splits
+[eva] Recording results for fabs_splits_test
+[eva] done for function fabs_splits_test
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function fabs_splits:
+  __retres ∈ [0. .. 1.79769313486e+308]
+[eva:final-states] Values at end of function fabs_splits_test:
+  x ∈ [-1. .. 1.]
+[from] Computing for function fabs_splits
+[from] Done for function fabs_splits
+[from] Computing for function fabs_splits_test
+[from] Done for function fabs_splits_test
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function fabs_splits:
+  \result FROM x
+[from] Function fabs_splits_test:
+  NO EFFECTS
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function fabs_splits:
+    __retres
+[inout] Inputs for function fabs_splits:
+    \nothing
+[inout] Out (internal) for function fabs_splits_test:
+    x; tmp
+[inout] Inputs for function fabs_splits_test:
+    \nothing

tests/value/partitioning-interproc.c

@@ -2,8 +2,8 @@
    GCC:
    STDOPT: #"-main cassign_test -eva-partition-history 1 -eva-interprocedural-partitioning-keep-history"
    STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-domains equality -eva-interprocedural-partitioning-keep-history"
+   STDOPT: #"-main fabs_splits_test -eva-partition-history 1 -eva-domains equality -eva-interprocedural-partitioning-keep-splits"
    */
-
 #include "__fc_builtin.h"
 
 int cassign(int *p)
@@ -51,3 +51,24 @@ void fabs_test(double x)
     x = x < 0 ? -1.0 : 1.0;
   }
 }
+
+
+double fabs_splits(double x)
+{
+  //@ split x > 0.0;
+  //@ split x < 0.0;
+  if (x == 0.0) {
+    return 0.0;
+  } else if (x > 0.0) {
+    return x;
+  } else {
+    return -x;
+  } 
+}
+
+void fabs_splits_test(double x)
+{
+  if (fabs_splits(x) > 1.0) {
+    x = x < 0 ? -1.0 : 1.0;
+  }
+}