diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index 0403e08909b0f8bef41f2569955e593035555758..6997606429cfe4cfcbede1bf6b57a8e80259ef8f 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -534,6 +534,127 @@ struct
let is_empty () = Filepath.Normalized.is_empty (get ())
end
+ (* ************************************************************************ *)
+ (** {3 Custom parameters} *)
+ (* ************************************************************************ *)
+
+ module Custom
+ (X: sig
+ include Parameter_sig.Input_with_arg
+ include Datatype.S
+ val default: t
+ val of_string: string -> t option
+ val to_string: t -> string
+ end) =
+ struct
+
+ include Build
+ (struct
+ include X
+ let default () = default
+ let functor_name = "Value"
+ end)
+
+ let possible_values = ref []
+ let set_possible_values s = possible_values := s
+ let get_possible_values () = !possible_values
+
+ (* Same interface as current module but with t replaced with string *)
+ module String_parameter =
+ struct
+ let get () =
+ X.to_string (get ())
+
+ let set s =
+ match X.of_string s with
+ | Some x -> set x
+ | None ->
+ (* Error during conversion from string to t, abort *)
+ let help_text =
+ match !possible_values with
+ | [] -> ""
+ | l ->
+ Format.asprintf "@ Possible values are: %a"
+ (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) l
+ in
+ P.L.abort "invalid input '%s' for option %s. %s" s name help_text
+
+ let add_set_hook f =
+ let f' x1 x2 = f (X.to_string x1) (X.to_string x2) in
+ add_set_hook f'
+
+ let add_update_hook f =
+ let f' x1 x2 = f (X.to_string x1) (X.to_string x2) in
+ add_update_hook f'
+ end
+
+ let parameter =
+ let accessor =
+ let open String_parameter in
+ Typed_parameter.String (
+ { get; set; add_set_hook; add_update_hook },
+ get_possible_values)
+ in
+ let reconfigurable = is_parameter_reconfigurable stage in
+ let p =
+ Typed_parameter.create ~name ~help:X.help ~accessor
+ ~visible:is_visible ~reconfigurable ~is_set
+ in
+ add_parameter !Parameter_customize.group_ref stage p;
+ Cmdline.add_option option_name
+ ~argname:X.arg_name
+ ~help:X.help
+ ~visible:is_visible
+ ~ext_help:!Parameter_customize.optional_help_ref
+ ~plugin:P.shortname
+ ~group
+ stage
+ (Cmdline.String String_parameter.set);
+ Parameter_customize.reset ();
+ if is_dynamic then
+ Dynamic.register ~plugin:empty_string X.option_name Typed_parameter.ty p
+ else
+ p
+ end
+
+ module Enum
+ (X: sig
+ include Parameter_sig.Input_with_arg
+ type t
+ val default: t
+ val all_values: t list
+ val to_string: t -> string
+ end) =
+ struct
+ module Custom_input =
+ struct
+ include Datatype.Make (struct
+ include Datatype.Serializable_undefined
+ let name = "Parameter_builder.Enum(" ^ X.option_name ^ ")"
+ type t = X.t
+ let copy x = x
+ let compare = Stdlib.compare
+ let equal = Datatype.from_compare
+ let reprs = X.all_values
+ end)
+
+ include X
+
+ let of_string =
+ let table =
+ List.to_seq X.all_values
+ |> Seq.map (fun x -> X.to_string x, x)
+ |> Hashtbl.of_seq
+ in
+ Hashtbl.find_opt table
+ end
+
+ include Custom (Custom_input)
+
+ let () =
+ set_possible_values (List.map X.to_string X.all_values)
+ end
+
(* ************************************************************************ *)
(** {3 Collections} *)
(* ************************************************************************ *)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.ml b/src/kernel_services/cmdline_parameters/parameter_sig.ml
index 7cb76c39aeef211ed269d0a1533c8048a74700a4..e6f7335c2c0d1275724ce71a31168e9be132a242 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.ml
@@ -279,6 +279,21 @@ module type String = sig
*)
end
+(** Signature for a custom parameter. *)
+module type Custom = sig
+ include S
+
+ val set_possible_values: string list -> unit
+ (** Set what are the acceptable values for this parameter.
+ If the given list is empty, then all values are acceptable.
+ @since Frama-C+dev *)
+
+ val get_possible_values: unit -> string list
+ (** What are the acceptable values for this parameter.
+ If the returned list is empty, then all values are acceptable.
+ @since Frama-C+dev *)
+end
+
(* ************************************************************************** *)
(** {3 Custom signatures} *)
(* ************************************************************************** *)
@@ -558,6 +573,28 @@ module type Builder = sig
and vice-versa. *)
end): Filepath
+ (** Allow using custom types as parameters.
+ @since Frama-c+dev *)
+ module Custom(X: sig
+ include Input_with_arg
+ include Datatype.S
+ val default: t
+ val of_string: string -> t option
+ val to_string: t -> string
+ end) : Custom with type t = X.t
+
+ (** A fixed set of possible values, represented by a type [t], intended to be
+ a variant with only a finite number of possible constructions.
+ Note that [t] must be comparable using [Stdlib.compare].
+ @since Frama-c+dev *)
+ module Enum(X : sig
+ include Input_with_arg
+ type t
+ val default: t
+ val all_values: t list
+ val to_string: t -> string
+ end) : S with type t = X.t
+
exception Cannot_build of string
module Make_set
(E:
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