Skip to content
Snippets Groups Projects
Commit dda07291 authored by David Bühler's avatar David Bühler
Browse files

[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.
parent 1d4fe906
No related branches found
No related tags found
No related merge requests found
...@@ -240,7 +240,7 @@ struct ...@@ -240,7 +240,7 @@ struct
(* Get every source flow *) (* Get every source flow *)
let sources_states = let sources_states =
(* Is there more than one non-empty incomming flow ? *) (* 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] | [(_,flow)] -> [flow]
| sources -> | sources ->
(* Several branches -> partition according to the incoming branch *) (* Several branches -> partition according to the incoming branch *)
......
...@@ -11,6 +11,9 @@ ...@@ -11,6 +11,9 @@
[eva] tests/value/partitioning-annots.c:127: [eva] tests/value/partitioning-annots.c:127:
function Frama_C_interval: precondition 'order' got status valid. function Frama_C_interval: precondition 'order' got status valid.
[eva] Done for function Frama_C_interval [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] tests/value/partitioning-annots.c:125: starting to merge loop iterations
[eva] computing for function Frama_C_interval <- test_loop_split. [eva] computing for function Frama_C_interval <- test_loop_split.
Called from tests/value/partitioning-annots.c:127. Called from tests/value/partitioning-annots.c:127.
......
...@@ -12,9 +12,9 @@ ...@@ -12,9 +12,9 @@
[eva] Done for function Frama_C_nondet [eva] Done for function Frama_C_nondet
[eva] Recording results for cassign [eva] Recording results for cassign
[eva] Done for function 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: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. [eva] computing for function cassign <- cassign_test.
Called from tests/value/partitioning-interproc.c:30. Called from tests/value/partitioning-interproc.c:30.
[eva] computing for function Frama_C_nondet <- cassign <- cassign_test. [eva] computing for function Frama_C_nondet <- cassign <- cassign_test.
...@@ -22,6 +22,15 @@ ...@@ -22,6 +22,15 @@
[eva] Done for function Frama_C_nondet [eva] Done for function Frama_C_nondet
[eva] Recording results for cassign [eva] Recording results for cassign
[eva] Done for function 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] Recording results for cassign_test
[eva] done for function cassign_test [eva] done for function cassign_test
......
...@@ -14,7 +14,7 @@ ...@@ -14,7 +14,7 @@
[eva:final-states] Values at end of function fabs: [eva:final-states] Values at end of function fabs:
__retres ∈ [-0. .. 1.79769313486e+308] __retres ∈ [-0. .. 1.79769313486e+308]
[eva:final-states] Values at end of function fabs_test: [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] Computing for function fabs
[from] Done for function fabs [from] Done for function fabs
[from] Computing for function fabs_test [from] Computing for function fabs_test
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment