diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml index 127f9c35c513faf3d8abc0f04b89f841ea56dce5..3f03b79168e15b99e716e1d7b458d3fd0afcc24c 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 0d4702a132229cc2c69b9b8ae06fb02ddf1d7786..1d1a14a2671438875798c21c4c233aae76eff722 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