[Eva] Add tests for interprocedural trace partitioning

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

+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at cassign_test
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] computing for function cassign <- cassign_test.
+  Called from tests/value/partitioning-interproc.c:24.
+[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
+  Called from tests/value/partitioning-interproc.c:11.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for cassign
+[eva] Done for function cassign
+[eva:alarm] tests/value/partitioning-interproc.c:25: Warning: 
+  accessing uninitialized left-value. assert \initialized(&x);
+[eva] tests/value/partitioning-interproc.c:26: Frama_C_show_each: {1}
+[eva] computing for function cassign <- cassign_test.
+  Called from tests/value/partitioning-interproc.c:30.
+[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
+  Called from tests/value/partitioning-interproc.c:11.
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for cassign
+[eva] Done for function cassign
+[eva] computing for function cassign <- cassign_test.
+  Called from tests/value/partitioning-interproc.c:30.
+[eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
+  Called from tests/value/partitioning-interproc.c:11.
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for cassign
+[eva] Done for function cassign
+[eva:alarm] tests/value/partitioning-interproc.c:31: Warning: 
+  accessing uninitialized left-value. assert \initialized(&x);
+[eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
+[eva] tests/value/partitioning-interproc.c:32: Frama_C_show_each: {1}
+[eva] Recording results for cassign_test
+[eva] done for function cassign_test
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function cassign:
+  Frama_C_entropy_source ∈ [--..--]
+  x ∈ {0} or UNINITIALIZED
+  __retres ∈ {0; 1}
+[eva:final-states] Values at end of function cassign_test:
+  Frama_C_entropy_source ∈ [--..--]
+  x ∈ {0} or UNINITIALIZED
+  y ∈ {1} or UNINITIALIZED
+[from] Computing for function cassign
+[from] Computing for function Frama_C_nondet <-cassign
+[from] Done for function Frama_C_nondet
+[from] Done for function cassign
+[from] Computing for function cassign_test
+[from] Done for function cassign_test
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_nondet:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; a; b
+[from] Function cassign:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  x FROM Frama_C_entropy_source; p (and SELF)
+  \result FROM Frama_C_entropy_source
+[from] Function cassign_test:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function cassign:
+    Frama_C_entropy_source; tmp; x; __retres
+[inout] Inputs for function cassign:
+    Frama_C_entropy_source
+[inout] Out (internal) for function cassign_test:
+    Frama_C_entropy_source; x; y; tmp; tmp_0
+[inout] Inputs for function cassign_test:
+    Frama_C_entropy_source

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

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

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

+[kernel] Parsing tests/value/partitioning-interproc.c (with preprocessing)
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva] computing for function conditional_assign <- main.
+  Called from tests/value/partitioning-interproc.c:23.
+[eva] computing for function Frama_C_nondet <- conditional_assign <- main.
+  Called from tests/value/partitioning-interproc.c:10.
+[eva] using specification for function Frama_C_nondet
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for conditional_assign
+[eva] Done for function conditional_assign
+[eva] tests/value/partitioning-interproc.c:25: Frama_C_show_each: {1}
+[eva] tests/value/partitioning-interproc.c:29: 
+  Reusing old results for call to conditional_assign
+[eva] computing for function conditional_assign <- main.
+  Called from tests/value/partitioning-interproc.c:29.
+[eva] computing for function Frama_C_nondet <- conditional_assign <- main.
+  Called from tests/value/partitioning-interproc.c:10.
+[eva] Done for function Frama_C_nondet
+[eva] Recording results for conditional_assign
+[eva] Done for function conditional_assign
+[eva] tests/value/partitioning-interproc.c:31: Frama_C_show_each: {1}
+[eva] Recording results for main
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function conditional_assign:
+  Frama_C_entropy_source ∈ [--..--]
+  x ∈ {0} or UNINITIALIZED
+  __retres ∈ {0; 1}
+[eva:final-states] Values at end of function main:
+  Frama_C_entropy_source ∈ [--..--]
+  x ∈ {0} or UNINITIALIZED
+  y ∈ {1} or UNINITIALIZED
+[from] Computing for function conditional_assign
+[from] Computing for function Frama_C_nondet <-conditional_assign
+[from] Done for function Frama_C_nondet
+[from] Done for function conditional_assign
+[from] Computing for function main
+[from] Done for function main
+[from] ====== DEPENDENCIES COMPUTED ======
+  These dependencies hold at termination for the executions that terminate:
+[from] Function Frama_C_nondet:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  \result FROM Frama_C_entropy_source; a; b
+[from] Function conditional_assign:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+  x FROM Frama_C_entropy_source; p (and SELF)
+  \result FROM Frama_C_entropy_source
+[from] Function main:
+  Frama_C_entropy_source FROM Frama_C_entropy_source (and SELF)
+[from] ====== END OF DEPENDENCIES ======
+[inout] Out (internal) for function conditional_assign:
+    Frama_C_entropy_source; tmp; x; __retres
+[inout] Inputs for function conditional_assign:
+    Frama_C_entropy_source
+[inout] Out (internal) for function main:
+    Frama_C_entropy_source; x; y; tmp; tmp_0
+[inout] Inputs for function main:
+    Frama_C_entropy_source

tests/value/partitioning-interproc.c

+/* run.config*
+   GCC:
+   STDOPT: #"-main cassign_test -eva-partition-history 1"
+   STDOPT: #"-main fabs_test -eva-partition-history 1 -eva-equality-domain"
+   */
+
+#include "__fc_builtin.h"
+
+int cassign(int *p)
+{
+  if (Frama_C_nondet(0,1))
+  {
+    *p = 0;
+    return 1;
+  }
+
+  return 0;
+}
+
+void cassign_test(void) {
+  int x, y;
+
+  // First call
+  if (cassign(&x)) {
+    y = x + 1;
+    Frama_C_show_each(y);
+  }
+
+  // Second call with some MemExec hit
+  if (cassign(&x)) {
+    y = x + 1;
+    Frama_C_show_each(y);
+  }
+}
+
+
+double fabs(double x)
+{
+  if (x == 0.0) {
+    return 0.0;
+  } else if (x > 0.0) {
+    return x;
+  } else {
+    return -x;
+  } 
+}
+
+void fabs_test(double x)
+{
+  if (fabs(x) > 1.0) {
+    x = x < 0 ? -1.0 : 1.0;
+  }
+}