diff --git a/src/plugins/value/engine/basic_partitioning.ml b/src/plugins/value/engine/basic_partitioning.ml index a2ee7cd2334c2054306e511758b2aff6391218ef..ca14677cc57a45b07e9da67418bb96f2b03cf5dc 100644 --- a/src/plugins/value/engine/basic_partitioning.ml +++ b/src/plugins/value/engine/basic_partitioning.ml @@ -182,6 +182,9 @@ struct w.previous_state <- `Bottom; w.widening_counter <- widening_delay + let reset_widening_counter (w : widening) : unit = + w.widening_counter <- widening_delay + (* Operators *) let clear_propagation (p : propagation) : unit = diff --git a/src/plugins/value/engine/legacy_partitioning.ml b/src/plugins/value/engine/legacy_partitioning.ml index 119ce80be5b7c8fc63e922e867423bda28c061a4..29552b96f667365380db7a0b632cf597c01085bd 100644 --- a/src/plugins/value/engine/legacy_partitioning.ml +++ b/src/plugins/value/engine/legacy_partitioning.ml @@ -141,6 +141,8 @@ struct w.previous_state <- `Bottom; w.widening_counter <- widening_delay + let reset_widening_counter w = w.widening_counter <- widening_delay + (* Operators *) let clear_propagation (p : propagation) : unit = diff --git a/src/plugins/value/engine/loop_partitioning.ml b/src/plugins/value/engine/loop_partitioning.ml index eda3d98eaddd19d1e10df402a34e5cf313d77c21..3036e5bd5a397dda9ee62c14deeb7d967c63fcc7 100644 --- a/src/plugins/value/engine/loop_partitioning.ml +++ b/src/plugins/value/engine/loop_partitioning.ml @@ -359,6 +359,10 @@ struct in Tree.iter reset w.widening_tree + let reset_widening_counter (w : widening) : unit = + let reset w = w.widening_counter <- widening_delay in + Tree.iter reset w.widening_tree + (* Operators *) let clear_propagation (p : propagation) : unit = diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/partitioned_dataflow.ml index 24468248e01ddab61772479a99508b42e6ec234a..8a7d4a1be7da52c943e88bffcef343ddc54d4f6a 100644 --- a/src/plugins/value/engine/partitioned_dataflow.ml +++ b/src/plugins/value/engine/partitioned_dataflow.ml @@ -624,8 +624,9 @@ module Make_Dataflow ignore (process_vertex v) | Wto.Component (v, w) as component -> (* Reset the component if hierachical_convergence is set *) - if hierachical_convergence then - reset_component (v :: Wto.flatten w); + if hierachical_convergence + then reset_component (v :: Wto.flatten w) + else Partition.reset_widening_counter (get_vertex_widening v); (* Iterate until convergence *) let iteration_count = ref 0 in while diff --git a/src/plugins/value/engine/state_partitioning.mli b/src/plugins/value/engine/state_partitioning.mli index 50932afe1d8bee85ac3cadc44c8906d4c0fcc080..a7b54408b6a3f910d4d6984577e18c8fcc386810 100644 --- a/src/plugins/value/engine/state_partitioning.mli +++ b/src/plugins/value/engine/state_partitioning.mli @@ -90,6 +90,7 @@ sig val reset_propagation : propagation -> unit val reset_shadow : shadow -> unit val reset_widening : widening -> unit + val reset_widening_counter : widening -> unit (* --- Partition transfer functions --- *)