From bfd6fc9df7dbaff714803d50da0f7870fafcf566 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Wed, 20 Mar 2019 16:34:13 +0100
Subject: [PATCH] [Eva] Emit slevel consumption messages only when on a
statement
- prevents the wrong display of locations ; we always have a suitable
from a statement
---
src/plugins/value/engine/partitioned_dataflow.ml | 6 +++---
tests/builtins/oracle/allocated.1.res.oracle | 3 ++-
2 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml
index 127f9c35c51..3f03b79168e 100644
--- a/src/plugins/value/engine/partitioned_dataflow.ml
+++ b/src/plugins/value/engine/partitioned_dataflow.ml
@@ -473,15 +473,15 @@ module Make_Dataflow
let store = get_vertex_store v in
(* Join incoming s tates *)
let f = Partition.join sources store in
- (* Output slevel related things *)
- let store_size = Partition.store_size store in
- output_slevel store_size;
begin match v.vertex_start_of with
| Some stmt ->
(* Callbacks *)
call_statement_callbacks stmt f;
(* Transfer function associated to the statement *)
Partition.transfer (transfer_statement stmt) f;
+ (* Output slevel related things *)
+ let store_size = Partition.store_size store in
+ output_slevel store_size;
(* Debug informations *)
Value_parameters.debug ~dkey ~current:true
"reached statement %d with %d / %d eternal states, %d to propagate"
diff --git a/tests/builtins/oracle/allocated.1.res.oracle b/tests/builtins/oracle/allocated.1.res.oracle
index 0d4702a1322..1d1a14a2671 100644
--- a/tests/builtins/oracle/allocated.1.res.oracle
+++ b/tests/builtins/oracle/allocated.1.res.oracle
@@ -325,7 +325,8 @@
Semantic level unrolling superposing up to 100 states
[eva] tests/builtins/allocated.c:84:
Semantic level unrolling superposing up to 200 states
-[eva] :0: Semantic level unrolling superposing up to 300 states
+[eva] tests/builtins/allocated.c:84:
+ Semantic level unrolling superposing up to 300 states
[eva] tests/builtins/allocated.c:84:
Semantic level unrolling superposing up to 400 states
[eva] tests/builtins/allocated.c:87: Call to builtin free
--
GitLab