diff --git a/Makefile b/Makefile index 9f7c9a8ba71b486fea60e94dfec7e679af684693..6ee2ea8d025c772f5f28f2d22f32774bbeb493b9 100644 --- a/Makefile +++ b/Makefile @@ -917,9 +917,9 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \ domains/cvalue/cvalue_domain \ engine/subdivided_evaluation engine/evaluation engine/abstractions \ engine/recursion engine/transfer_stmt engine/transfer_specification \ - engine/partitioning engine/mem_exec \ + engine/partitioning_index engine/mem_exec \ engine/partition engine/partitioning_parameters engine/trace_partitioning \ - engine/partitioned_dataflow \ + engine/iterator \ engine/initialization \ engine/compute_functions engine/analysis register PLUGIN_CMI:= values/abstract_value values/abstract_location \ diff --git a/headers/header_spec.txt b/headers/header_spec.txt index e94bb4bef29fba47a4d4011839b7e546957bd5b1..98f4907dbfa66dff810e72c8c66479c7f8502c9a 100644 --- a/headers/header_spec.txt +++ b/headers/header_spec.txt @@ -1176,14 +1176,14 @@ src/plugins/value/engine/evaluation.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/evaluation.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/initialization.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/initialization.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/engine/iterator.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/engine/iterator.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/mem_exec.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/mem_exec.mli: CEA_LGPL_OR_PROPRIETARY -src/plugins/value/engine/partitioned_dataflow.ml: CEA_LGPL_OR_PROPRIETARY -src/plugins/value/engine/partitioned_dataflow.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/partition.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/partition.mli: CEA_LGPL_OR_PROPRIETARY -src/plugins/value/engine/partitioning.ml: CEA_LGPL_OR_PROPRIETARY -src/plugins/value/engine/partitioning.mli: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/engine/partitioning_index.ml: CEA_LGPL_OR_PROPRIETARY +src/plugins/value/engine/partitioning_index.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/partitioning_parameters.ml: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/partitioning_parameters.mli: CEA_LGPL_OR_PROPRIETARY src/plugins/value/engine/recursion.ml: CEA_LGPL_OR_PROPRIETARY diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml index cac999676f65a89e8938639c4120039094b8d4eb..d265352833e4dbbf7b2d88c7ed8483849670c57d 100644 --- a/src/plugins/value/engine/compute_functions.ml +++ b/src/plugins/value/engine/compute_functions.ml @@ -124,7 +124,7 @@ let () = let handler (_signal: int) = !prev Sys.sigusr1; (* Call previous signal handler *) Value_parameters.warning "Stopping analysis at user request@."; - Partitioned_dataflow.signal_abort () + Iterator.signal_abort () in try match Sys.signal Sys.sigusr1 (Sys.Signal_handle handler) with @@ -143,7 +143,7 @@ module Make (Abstract: Abstractions.Eva) = struct module Init = Initialization.Make (Abstract.Dom) (Abstract.Eval) (Transfer) module Computer = - Partitioned_dataflow.Computer + Iterator.Computer (Abstract) (PowersetDomain) (Transfer) (Init) (Logic) (Spec) let initial_state = Init.initial_state diff --git a/src/plugins/value/engine/partitioned_dataflow.ml b/src/plugins/value/engine/iterator.ml similarity index 100% rename from src/plugins/value/engine/partitioned_dataflow.ml rename to src/plugins/value/engine/iterator.ml diff --git a/src/plugins/value/engine/partitioned_dataflow.mli b/src/plugins/value/engine/iterator.mli similarity index 100% rename from src/plugins/value/engine/partitioned_dataflow.mli rename to src/plugins/value/engine/iterator.mli diff --git a/src/plugins/value/engine/partitioning.ml b/src/plugins/value/engine/partitioning_index.ml similarity index 100% rename from src/plugins/value/engine/partitioning.ml rename to src/plugins/value/engine/partitioning_index.ml diff --git a/src/plugins/value/engine/partitioning.mli b/src/plugins/value/engine/partitioning_index.mli similarity index 100% rename from src/plugins/value/engine/partitioning.mli rename to src/plugins/value/engine/partitioning_index.mli diff --git a/src/plugins/value/engine/trace_partitioning.ml b/src/plugins/value/engine/trace_partitioning.ml index b9aef2190db4efef5ff4ed091e71f731cf33eb79..96c8bc8f5afb1c72207353101382a350536a074a 100644 --- a/src/plugins/value/engine/trace_partitioning.ml +++ b/src/plugins/value/engine/trace_partitioning.ml @@ -36,7 +36,7 @@ struct module Domain = Abstract.Dom - module Index = Partitioning.Make (Domain) + module Index = Partitioning_index.Make (Domain) module Flow = Partition.MakeFlow (Abstract) type state = Domain.t