From dda0729176cf05c62d33c7fabb4df239d42ed9b1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 1 Oct 2021 13:21:39 +0200
Subject: [PATCH] [Eva] Reverts a fix of a precision bug on
 -eva-partition-history.

The fix is correct, but it significantly changes the behavior of the history
partitioning on some case studies.
Keep it for later, in order to fully understand the consequences.
---
 .../value/partitioning/trace_partitioning.ml        |  2 +-
 tests/value/oracle/partitioning-annots.2.res.oracle |  3 +++
 .../oracle/partitioning-interproc.0.res.oracle      | 13 +++++++++++--
 .../oracle/partitioning-interproc.1.res.oracle      |  2 +-
 4 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml
index d70eaeb3ded..c3c7de25a7e 100644
--- a/src/plugins/value/partitioning/trace_partitioning.ml
+++ b/src/plugins/value/partitioning/trace_partitioning.ml
@@ -240,7 +240,7 @@ struct
     (* Get every source flow *)
     let sources_states =
       (* Is there more than one non-empty incomming flow ? *)
-      match List.filter (fun (_b,f) -> not (Flow.is_empty f)) sources with
+      match sources with
       | [(_,flow)] -> [flow]
       | sources ->
         (* Several branches -> partition according to the incoming branch *)
diff --git a/tests/value/oracle/partitioning-annots.2.res.oracle b/tests/value/oracle/partitioning-annots.2.res.oracle
index 5c65066b2aa..da1dee03a86 100644
--- a/tests/value/oracle/partitioning-annots.2.res.oracle
+++ b/tests/value/oracle/partitioning-annots.2.res.oracle
@@ -11,6 +11,9 @@
 [eva] tests/value/partitioning-annots.c:127: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- test_loop_split.
+  Called from tests/value/partitioning-annots.c:127.
+[eva] Done for function Frama_C_interval
 [eva] tests/value/partitioning-annots.c:125: starting to merge loop iterations
 [eva] computing for function Frama_C_interval <- test_loop_split.
   Called from tests/value/partitioning-annots.c:127.
diff --git a/tests/value/oracle/partitioning-interproc.0.res.oracle b/tests/value/oracle/partitioning-interproc.0.res.oracle
index 4481fdb71c7..76c88a345e0 100644
--- a/tests/value/oracle/partitioning-interproc.0.res.oracle
+++ b/tests/value/oracle/partitioning-interproc.0.res.oracle
@@ -12,9 +12,9 @@
 [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] tests/value/partitioning-interproc.c:30: 
-  Reusing old results for call to 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.
@@ -22,6 +22,15 @@
 [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] Recording results for cassign_test
 [eva] done for function cassign_test
diff --git a/tests/value/oracle/partitioning-interproc.1.res.oracle b/tests/value/oracle/partitioning-interproc.1.res.oracle
index dfd3684a605..a2bde102b39 100644
--- a/tests/value/oracle/partitioning-interproc.1.res.oracle
+++ b/tests/value/oracle/partitioning-interproc.1.res.oracle
@@ -14,7 +14,7 @@
 [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. .. 1.]
+  x ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
 [from] Computing for function fabs
 [from] Done for function fabs
 [from] Computing for function fabs_test
-- 
GitLab