From 235be4a8358cd79f80e37ff173cf68466b1dacf2 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Thu, 18 Jan 2024 00:37:09 +0100
Subject: [PATCH] [Eva] Use the new Parameter_builder.Enum
---
src/plugins/eva/engine/iterator.ml | 11 +----------
src/plugins/eva/parameters.ml | 13 ++++++++++---
src/plugins/eva/parameters.mli | 4 +++-
3 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/plugins/eva/engine/iterator.ml b/src/plugins/eva/engine/iterator.ml
index 899fb601299..f17c7e4f86e 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 9900dd5cc70..9f28b454139 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 7fa79238485..7c580cf947f 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
--
GitLab