Commit 85ced63b authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

Merge branch 'feature/michele/kernel-files-as-filepaths' into 'master'

Use Filepath as machinery for Kernel.Files

See merge request frama-c/frama-c!2487
parents ac86ded4 3a5b4e76
......@@ -96,12 +96,9 @@ ML_LINT_KO+=src/kernel_services/ast_transformations/filter.ml
ML_LINT_KO+=src/kernel_services/ast_transformations/filter.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_builder.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_builder.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_category.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_category.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_customize.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_sig.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_state.ml
ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_state.mli
ML_LINT_KO+=src/kernel_services/cmdline_parameters/typed_parameter.ml
......
......@@ -1639,7 +1639,7 @@ let init_from_cmdline () =
let files = Kernel.Files.get () in
if files = [] && not !Config.is_gui then Kernel.warning "no input file.";
let files =
List.map (fun s -> from_filename s) files
List.map (fun f -> from_filename (Filepath.Normalized.to_pretty_string f)) files
in
try
init_from_c_files files;
......
......@@ -726,7 +726,7 @@ let add_aliases orig ~plugin ~group stage aliases =
let replace_option_setting = Plugin.replace_option_setting
module On_Files = Hook.Build(struct type t = string list end)
module On_Files = Hook.Build(struct type t = Filepath.Normalized.t list end)
let use_cmdline_files = On_Files.extend
let set_files used_loading l =
......@@ -746,7 +746,7 @@ let set_files used_loading l =
"ignoring source files specified on the command line \
while loading a global initial context."
else begin
On_Files.apply l;
On_Files.apply (List.map Filepath.Normalized.of_string l);
After_setting.apply l
end
......
......@@ -227,7 +227,7 @@ val nb_given_options: unit -> int
Should not be called before the end of the command line parsing.
@since Beryllium-20090601-beta1 *)
val use_cmdline_files: (string list -> unit) -> unit
val use_cmdline_files: (Datatype.Filepath.t list -> unit) -> unit
(** What to do with the list of files put on the command lines.
@since Beryllium-20090601-beta1 *)
......
......@@ -27,15 +27,15 @@
(* ************************************************************************* *)
module Make
(P: sig
val shortname: string
val parameters: (string, Typed_parameter.t list) Hashtbl.t
module L: sig
val abort: ('a,'b) Log.pretty_aborter
val warning: 'a Log.pretty_printer
end
val messages_group: Cmdline.Group.t
end):
(P: sig
val shortname: string
val parameters: (string, Typed_parameter.t list) Hashtbl.t
module L: sig
val abort: ('a,'b) Log.pretty_aborter
val warning: 'a Log.pretty_printer
end
val messages_group: Cmdline.Group.t
end):
Parameter_sig.Builder
(* ************************************************************************* *)
......
......@@ -23,7 +23,7 @@
(** Signatures for command line options. *)
(* ************************************************************************** *)
(** {2 Input signatures}
(** {2 Input signatures}
One of these signatures is required to implement a new command line
option. *)
......@@ -33,10 +33,10 @@
option on the command line argument. *)
module type Input = sig
val option_name: string
(** The name of the option *)
(** The name of the option *)
val help: string
(** A description for this option (e.g. used by -help).
If [help = ""], then it has the special meaning "undocumented" *)
(** A description for this option (e.g. used by -help).
If [help = ""], then it has the special meaning "undocumented" *)
end
(** Minimal signature to implement for each parameter corresponding to an
......@@ -44,8 +44,8 @@ end
module type Input_with_arg = sig
include Input
val arg_name: string
(** A standard name for the argument which may be used in the description.
If empty, a generic arg_name is generated. *)
(** A standard name for the argument which may be used in the description.
If empty, a generic arg_name is generated. *)
end
(** Minimal signature for collections of custom datatype *)
......@@ -81,7 +81,7 @@ module type String_datatype_with_collections = sig
(** If a single string can be mapped to several elements. Can
default to {!no_element_of_string} to indicate that each string [s] is
mapped exactly to [of_string s].
*)
*)
val to_string: t -> string
end
......@@ -104,11 +104,11 @@ module type Value_datatype = sig
string. *)
val to_string: key:key -> t option -> string option
(** [key] is the key associated to this value. The optional string is [None] if
there is no value associated to the key, and [Some v] (potentially [v =
""]) otherwise.
@return None if there is no value to associate to the key or [Some v]
otherwise. *)
(** [key] is the key associated to this value. The optional string is [None] if
there is no value associated to the key, and [Some v] (potentially [v =
""]) otherwise.
@return None if there is no value to associate to the key or [Some v]
otherwise. *)
end
......@@ -123,7 +123,7 @@ module type Multiple_value_datatype = sig
end
(* ************************************************************************** *)
(** {2 Output signatures}
(** {2 Output signatures}
Signatures corresponding to a command line option of a specific type. *)
(* ************************************************************************** *)
......@@ -140,12 +140,12 @@ module type S_no_parameter = sig
module implementing this signature. *)
val set: t -> unit
(** Set the option. *)
(** Set the option. *)
val add_set_hook: (t -> t -> unit) -> unit
(** Add a hook to be called after the function {!set} is called.
The first parameter of the hook is the old value of the parameter while
the second one is the new value. *)
(** Add a hook to be called after the function {!set} is called.
The first parameter of the hook is the old value of the parameter while
the second one is the new value. *)
val add_update_hook: (t -> t -> unit) -> unit
(** Add a hook to be called when the value of the parameter changes (by
......@@ -156,18 +156,18 @@ module type S_no_parameter = sig
@since Nitrogen-20111001 *)
val get: unit -> t
(** Option value (not necessarily set on the current command line). *)
(** Option value (not necessarily set on the current command line). *)
val clear: unit -> unit
(** Set the option to its default value, that is the value if [set] was
never called. *)
(** Set the option to its default value, that is the value if [set] was
never called. *)
val is_default: unit -> bool
(** Is the option equal to its default value? *)
(** Is the option equal to its default value? *)
val option_name: string
(** Name of the option on the command-line
@since Carbon-20110201 *)
(** Name of the option on the command-line
@since Carbon-20110201 *)
val print_help: Format.formatter -> unit
(** Print the help of the parameter in the given formatter as it would be
......@@ -191,8 +191,8 @@ module type S_no_parameter = sig
never be used. *)
val unsafe_set: t -> unit
(** Set but without clearing the dependencies.*)
(**/**)
(** Set but without clearing the dependencies.*)
(**/**)
end
......@@ -214,10 +214,10 @@ module type Bool = sig
include S with type t = bool
val on: unit -> unit
(** Set the boolean to [true]. *)
(** Set the boolean to [true]. *)
val off: unit -> unit
(** Set the boolean to [false]. *)
(** Set the boolean to [false]. *)
end
......@@ -228,15 +228,15 @@ module type Int = sig
include S with type t = int
val incr: unit -> unit
(** Increment the integer. *)
(** Increment the integer. *)
val set_range: min:int -> max:int -> unit
(** Set what is the possible range of values for this parameter.
@since Beryllium-20090901 *)
(** Set what is the possible range of values for this parameter.
@since Beryllium-20090901 *)
val get_range: unit -> int * int
(** What is the possible range of values for this parameter.
@since Beryllium-20090901 *)
(** What is the possible range of values for this parameter.
@since Beryllium-20090901 *)
end
......@@ -246,29 +246,29 @@ module type String = sig
include S with type t = string
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 Beryllium-20090901 *)
(** Set what are the acceptable values for this parameter.
If the given list is empty, then all values are acceptable.
@since Beryllium-20090901 *)
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 Beryllium-20090901 *)
(** What are the acceptable values for this parameter.
If the returned list is empty, then all values are acceptable.
@since Beryllium-20090901 *)
val get_function_name: unit -> string
(** returns the given argument only if it is a valid function name
(see {!Parameter_customize.get_c_ified_functions} for more information),
and abort otherwise.
(** returns the given argument only if it is a valid function name
(see {!Parameter_customize.get_c_ified_functions} for more information),
and abort otherwise.
Requires that the AST has been computed. Default getter when
{!Parameter_customize.argument_is_function_name} has been called.
@since Sodium-20150201
*)
Requires that the AST has been computed. Default getter when
{!Parameter_customize.argument_is_function_name} has been called.
@since Sodium-20150201
*)
val get_plain_string: unit -> string
(** always return the argument, even if the argument is not a function name.
@since Sodium-20150201
*)
*)
end
(* ************************************************************************** *)
......@@ -298,15 +298,15 @@ module type Specific_dir = sig
(** For functions below: if [force_dir] is true: if [error] is [false], then
creates the directory if it does not exist (or raises No_dir if the
directory cannot be created). Otherwise ([force_dir =
false]), raise No_dir if [error] is [false].
@since Neon-20140301 *)
false]), raise No_dir if [error] is [false].
@since Neon-20140301 *)
val dir: ?error:bool -> unit -> string
(** [dir ~error ()] returns the specific directory name, if
any. Otherwise, Frama-C halts on an user error if [error] or if the
behavior depends on [force_dir]. Default of [error] is [true].
@raise No_dir if there is no share directory for this plug-in and [not
error] and [not force_dir]. *)
(** [dir ~error ()] returns the specific directory name, if
any. Otherwise, Frama-C halts on an user error if [error] or if the
behavior depends on [force_dir]. Default of [error] is [true].
@raise No_dir if there is no share directory for this plug-in and [not
error] and [not force_dir]. *)
val file: ?error:bool -> string -> string
(** [file basename] returns the complete filename of a file stored in [dir
......@@ -317,30 +317,13 @@ module type Specific_dir = sig
error] and [not force_dir]. *)
module Dir_name: String
(** Option [-<short-name>-<specific-dir>]. *)
(** Option [-<short-name>-<specific-dir>]. *)
end
type existence = Must_exist | Must_not_exist | Indifferent
(** signature for normalized pathnames. *)
module type Filepath = sig
exception No_file
(** raised by {!check_existence} if no file exists and [existence] is [Must_exist]. *)
module type Filepath = S with type t = Filepath.Normalized.t
exception File_exists
(** raised by {!check_existence} if some file exists and [existence] is
[Must_nos_exist]. *)
val existence: existence
val check_existence: existence -> Filepath.Normalized.t -> unit
(** Checks the existence/absence of a file. May raise [No_file] or [File_exists]. *)
include S with type t = Filepath.Normalized.t
end
(* ************************************************************************** *)
(** {3 Collections} *)
......@@ -406,7 +389,7 @@ module type Collection = sig
(** A collection is a standard string parameter *)
module Category: Collection_category with type elt = elt
(** Categories for this collection. *)
(** Categories for this collection. *)
end
(** Signature for sets as command line parameters.
......@@ -422,7 +405,7 @@ module type Set = sig
(** Does the given element belong to the set? *)
val exists: (elt -> bool) -> bool
(** Is there some element satisfying the given predicate? *)
(** Is there some element satisfying the given predicate? *)
end
......@@ -436,12 +419,12 @@ module type String_set =
@plugin development guide *)
module type Kernel_function_set =
Set with type elt = Cil_types.kernel_function
and type t = Cil_datatype.Kf.Set.t
and type t = Cil_datatype.Kf.Set.t
(** @since Sodium-20150201 *)
module type Fundec_set =
Set with type elt = Cil_types.fundec
and type t = Cil_datatype.Fundec.Set.t
and type t = Cil_datatype.Fundec.Set.t
(** Signature for lists as command line parameters.
@since Sodium-20150201 *)
......@@ -453,8 +436,8 @@ module type List = sig
(** {3 Additional accessors to the list.} *)
val append_before: t -> unit
(** append a list in front of the current state
@since Neon-20140301 *)
(** append a list in front of the current state
@since Neon-20140301 *)
val append_after: t -> unit
(** append a list at the end of the current state
......@@ -465,6 +448,9 @@ end
(** @modify Sodium-20150201 *)
module type String_list = List with type elt = string and type t = string list
module type Filepath_list =
List with type elt = Datatype.Filepath.t and type t = Datatype.Filepath.t list
(** Signature for maps as command line parameters.
@since Sodium-20150201 *)
module type Map = sig
......@@ -479,8 +465,8 @@ module type Map = sig
(** {3 Additional accessors to the map.} *)
val find: key -> value
(** Search a given key in the map.
@raise Not_found if there is no such key in the map. *)
(** Search a given key in the map.
@raise Not_found if there is no such key in the map. *)
val mem: key -> bool
......@@ -521,7 +507,7 @@ module type Builder = sig
module True(X: Input) : Bool
module WithOutput
(X: sig include Input val output_by_default: bool end):
(X: sig include Input val output_by_default: bool end):
With_output
(** @plugin development guide *)
......@@ -540,102 +526,113 @@ module type Builder = sig
module Filepath(X: sig
include Input_with_arg
val existence: existence
val existence: Filepath.existence
val file_kind: string
(** used in error message if the file does not exist where it should
and vice-versa. *)
end): Filepath
exception Cannot_build of string
module Make_set
(E:
sig
include String_datatype_with_collections
val of_singleton_string: string -> Set.t
end)
(X: sig include Input_collection val default: E.Set.t end):
(E:
sig
include String_datatype_with_collections
val of_singleton_string: string -> Set.t
end)
(X: sig include Input_collection val default: E.Set.t end):
Set with type elt = E.t and type t = E.Set.t
(** @plugin development guide *)
module String_set(X: Input_with_arg): String_set
module Filled_string_set
(X: sig
include Input_with_arg
val default: Datatype.String.Set.t
end): String_set
(X: sig
include Input_with_arg
val default: Datatype.String.Set.t
end): String_set
(** @plugin development guide *)
module Kernel_function_set(X: Input_with_arg): Kernel_function_set
module Fundec_set(X: Input_with_arg): Fundec_set
module Make_list
(E:
sig
include String_datatype
val of_singleton_string: string -> t list
end)
(X: sig include Input_collection val default: E.t list end):
(E:
sig
include String_datatype
val of_singleton_string: string -> t list
end)
(X: sig include Input_collection val default: E.t list end):
List with type elt = E.t and type t = E.t list
module String_list(X: Input_with_arg): String_list
module Filepath_list
(X: sig
include Input_with_arg
val existence: Fc_Filepath.existence
val file_kind: string
(** see [Filepath] module. *)
end): Filepath_list
(** Parameter is a map where multibindings are **not** allowed. *)
module Make_map
(K: String_datatype_with_collections)
(V: Value_datatype with type key = K.t)
(X: sig include Input_collection val default: V.t K.Map.t end):
(K: String_datatype_with_collections)
(V: Value_datatype with type key = K.t)
(X: sig include Input_collection val default: V.t K.Map.t end):
Map
with type key = K.t and type value = V.t and type t = V.t K.Map.t
module String_map
(V: Value_datatype with type key = string)
(X: sig include Input_with_arg val default: V.t Datatype.String.Map.t end):
(V: Value_datatype with type key = string)
(X: sig include Input_with_arg val default: V.t Datatype.String.Map.t end):
Map
with type key = string
and type value = V.t
and type t = V.t Datatype.String.Map.t
and type value = V.t
and type t = V.t Datatype.String.Map.t
(** As for Kernel_function_set, by default keys can only be defined functions.
Use {!Parameter_customize.argument_may_be_fundecl} to also include
pure prototypes. *)
module Kernel_function_map
(V: Value_datatype with type key = Cil_types.kernel_function)
(X: sig include Input_with_arg val default: V.t Cil_datatype.Kf.Map.t end):
(V: Value_datatype with type key = Cil_types.kernel_function)
(X: sig include Input_with_arg val default: V.t Cil_datatype.Kf.Map.t end):
Map
with type key = Cil_types.kernel_function
and type value = V.t
and type t = V.t Cil_datatype.Kf.Map.t
and type value = V.t
and type t = V.t Cil_datatype.Kf.Map.t
(** Parameter is a map where multibindings are allowed. *)
module Make_multiple_map
(K: String_datatype_with_collections)
(V: Multiple_value_datatype with type key = K.t)
(X: sig include Input_collection val default: V.t list K.Map.t end):
(K: String_datatype_with_collections)
(V: Multiple_value_datatype with type key = K.t)
(X: sig include Input_collection val default: V.t list K.Map.t end):
Multiple_map
with type key = K.t and type value = V.t and type t = V.t list K.Map.t
module String_multiple_map
(V: Multiple_value_datatype with type key = string)
(X: sig
include Input_with_arg
val default: V.t list Datatype.String.Map.t
end):
(V: Multiple_value_datatype with type key = string)
(X: sig
include Input_with_arg
val default: V.t list Datatype.String.Map.t
end):
Multiple_map
with type key = string
and type value = V.t
and type t = V.t list Datatype.String.Map.t
and type value = V.t
and type t = V.t list Datatype.String.Map.t
(** As for Kernel_function_set, by default keys can only be defined functions.
Use {!Parameter_customize.argument_may_be_fundecl} to also include
pure prototypes. *)
module Kernel_function_multiple_map
(V: Multiple_value_datatype with type key = Cil_types.kernel_function)
(X: sig
include Input_with_arg
val default: V.t list Cil_datatype.Kf.Map.t
end):
(V: Multiple_value_datatype with type key = Cil_types.kernel_function)
(X: sig
include Input_with_arg
val default: V.t list Cil_datatype.Kf.Map.t
end):
Multiple_map
with type key = Cil_types.kernel_function
and type value = V.t
and type t = V.t list Cil_datatype.Kf.Map.t
and type value = V.t
and type t = V.t list Cil_datatype.Kf.Map.t
val parameters: unit -> Typed_parameter.t list
......
......@@ -247,6 +247,18 @@ module String_list(X: Input_with_arg) =
include X
end)
module Filepath_list
(X: sig
include Input_with_arg
val existence: Filepath.existence
val file_kind: string
end) =
P.Filepath_list
(struct
let () = Parameter_customize.set_module_name X.module_name
include X
end)
module Kernel_function_set(X: Input_with_arg) =
P.Kernel_function_set
(struct
......@@ -720,7 +732,8 @@ module LoadState =
(struct
let option_name = "-load"
let arg_name = "filename"
let existence = Parameter_sig.Must_exist
let existence = Filepath.Must_exist
let file_kind = "Frama-C state"
let help = "load a previously-saved session from file <filename>"
end)
......@@ -1216,12 +1229,14 @@ module Files = struct
let () = Parameter_customize.is_invisible ()
let () = Parameter_customize.no_category ()
include String_list
include Filepath_list
(struct
let option_name = ""