diff --git a/src/plugins/value/partitioning/trace_partitioning.ml b/src/plugins/value/partitioning/trace_partitioning.ml index d70eaeb3dedf59eff07f8d6f1f94371ed72895d5..c3c7de25a7e8ba38afd8853589bc250d31b981b2 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 5c65066b2aae5c7774ac47d36a126fb55b6a1375..da1dee03a864d7ec4bfbbfcafaa36a21158a914f 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 4481fdb71c75b560b40d5f611f615da44aa446a3..76c88a345e072128c5c455ea5432d089b98654f0 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 dfd3684a60556eb5eb3f3103610e38cf700f7c6a..a2bde102b390521d164ac45c3f46efd0e6c0d98e 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