diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml index 899fb60129901f150699afc38977f924bef104f0..f17c7e4f86e72193b7c2f989cd578e98f6aa784e 100644 --- a/src/plugins/eva/engine/iterator.ml +++ b/src/plugins/eva/engine/iterator.ml @@ -100,15 +100,6 @@ module Make_Dataflow (* --- Plugin parameters --- *) - type descending_strategy = NoIteration | FullIteration | ExitIteration - - let descending_iteration : descending_strategy = - match Parameters.DescendingIteration.get () with - | "no" -> NoIteration - | "exits" -> ExitIteration - | "full" -> FullIteration - | _ -> assert false - let hierachical_convergence : bool = Parameters.HierarchicalConvergence.get () @@ -584,7 +575,7 @@ module Make_Dataflow incr iteration_count; done; (* Descending sequence *) - let l = match descending_iteration with + let l = match Parameters.DescendingIteration.get () with | NoIteration -> [] | ExitIteration -> Self.debug ~dkey diff --git a/src/plugins/eva/parameters.ml b/src/plugins/eva/parameters.ml index 9900dd5cc70f953e69095e7a1a3e02c8453f7105..9f28b45413909c1f5fa636036d365b884c4b92e8 100644 --- a/src/plugins/eva/parameters.ml +++ b/src/plugins/eva/parameters.ml @@ -566,20 +566,27 @@ let () = add_correctness_dep InitializationPaddingGlobals.parameter (* --- Iteration strategy --- *) +type descending_strategy = NoIteration | FullIteration | ExitIteration + let () = Parameter_customize.set_group precision_tuning let () = Parameter_customize.is_invisible () module DescendingIteration = - String + Enum (struct - let default = "no" let option_name = "-eva-descending-iteration" let arg_name = "no|exits|full" let help = "Experimental. After hitting a postfix point, try to improve \ the precision with either a <full> iteration or an iteration \ from loop head to exit paths (<exits>) or do not try anything \ (<no>). Default is <no>." + type t = descending_strategy + let default = NoIteration + let all_values = [NoIteration ; FullIteration ; ExitIteration] + let to_string = function + | NoIteration -> "no" + | FullIteration -> "full" + | ExitIteration -> "exits" end) -let () = DescendingIteration.set_possible_values ["no" ; "exits" ; "full"] let () = add_precision_dep DescendingIteration.parameter let () = Parameter_customize.set_group precision_tuning diff --git a/src/plugins/eva/parameters.mli b/src/plugins/eva/parameters.mli index 7fa79238485ed73982558724e55d2687172c97ae..7c580cf947f83391e2eb898aa173fcbe1793f966 100644 --- a/src/plugins/eva/parameters.mli +++ b/src/plugins/eva/parameters.mli @@ -62,7 +62,9 @@ module WarnSignedConvertedDowncast: Parameter_sig.Bool module WarnPointerSubstraction: Parameter_sig.Bool module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set -module DescendingIteration: Parameter_sig.String +type descending_strategy = NoIteration | FullIteration | ExitIteration + +module DescendingIteration: Parameter_sig.S with type t = descending_strategy module HierarchicalConvergence: Parameter_sig.Bool module WideningDelay: Parameter_sig.Int module WideningPeriod: Parameter_sig.Int