From c8373aa76ccaba02e78628d91773ad8e54433856 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 1 Jul 2024 11:35:58 +0200
Subject: [PATCH] [kernel] we do not expect user dirs to exist
---
.../cmdline_parameters/parameter_sig.ml | 23 ++++++-
.../plugin_entry_points/plugin.ml | 63 +++++++++----------
.../plugin_entry_points/plugin.mli | 9 +--
src/plugins/gui/gui_parameters.mli | 2 +-
4 files changed, 57 insertions(+), 40 deletions(-)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.ml b/src/kernel_services/cmdline_parameters/parameter_sig.ml
index c07ef6b5afc..2d8ed92a533 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.ml
@@ -337,7 +337,7 @@ module type Specific_dir = sig
(** @return whether the plugin <specific-dir> has been set. *)
val get_dir:
- ?mode:[`Normalize_only | `Create_path | `Must_exist ] ->
+ ?mode:[< `Normalize_only | `Create_path | `Must_exist > `Normalize_only] ->
string ->
Filepath.Normalized.t
(** [get_dir ?mode p] returns a (local) path [p], i.e. relative to the plugin
@@ -349,7 +349,7 @@ module type Specific_dir = sig
+ [Must_exist] aborts if the resulting path does not exist. *)
val get_file:
- ?mode:[`Normalize_only | `Create_path | `Must_exist ] ->
+ ?mode:[< `Normalize_only | `Create_path | `Must_exist > `Normalize_only] ->
string ->
Filepath.Normalized.t
(** [get_file ?mode p] returns a (local) path [p], i.e. relative to the
@@ -361,6 +361,25 @@ module type Specific_dir = sig
+ [Must_exist] aborts if the resulting path does not exist. *)
end
+(** Specializes Specific_dir for user directories (config, state, ...). These
+ directories. We do not expect these directories to exist.
+
+ @since Frama-C+dev
+*)
+module type User_dir = sig
+ include Specific_dir
+
+ val get_dir:
+ ?mode:[< `Normalize_only | `Create_path > `Normalize_only ] ->
+ string -> Filepath.Normalized.t
+ (** Refer to {!Specific_dir.get_dir} *)
+
+ val get_file:
+ ?mode:[< `Normalize_only | `Create_path > `Normalize_only ] ->
+ string -> Filepath.Normalized.t
+ (** Refer to {!Specific_dir.get_file} *)
+end
+
(* ************************************************************************** *)
(** {3 Collections} *)
(* ************************************************************************** *)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index ae7e9e43cd3..2fb07450328 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -44,9 +44,9 @@ module type S_no_log = sig
module Debug: Parameter_sig.Int
module Share: Parameter_sig.Specific_dir
module Session: Parameter_sig.Specific_dir
- module Cache_dir () : Parameter_sig.Specific_dir
- module Config_dir () : Parameter_sig.Specific_dir
- module State_dir () : Parameter_sig.Specific_dir
+ module Cache_dir () : Parameter_sig.User_dir
+ module Config_dir () : Parameter_sig.User_dir
+ module State_dir () : Parameter_sig.User_dir
val help: Cmdline.Group.t
val messages: Cmdline.Group.t
val add_plugin_output_aliases:
@@ -296,7 +296,8 @@ struct
(D: sig
val dirs: unit -> Fc_Filepath.Normalized.t list
val visible_ref: bool
- end)
+ end) :
+ Parameter_sig.Specific_dir
=
struct
@@ -354,6 +355,13 @@ struct
end
let get_dir ?(mode=`Normalize_only) s =
+ (* In presence of more than one base directory, consider the first to
+ form the resulting [filepath]. *)
+ let filepath =
+ match base_dirs () with
+ | [] -> assert false
+ | d :: _ -> Datatype.Filepath.concat d s
+ in
match mode with
| `Must_exist ->
begin
@@ -387,35 +395,21 @@ struct
(base_dirs ())
| Some d -> d
end
- | _ ->
+ | `Normalize_only ->
+ filepath
+ | `Create_path ->
begin
- (* In presence of more than one base directory, consider the first to
- form the resulting [filepath]. *)
- let filepath =
- match base_dirs () with
- | [] -> assert false
- | d :: _ -> Datatype.Filepath.concat d s
- in
- match mode with
- | `Must_exist ->
- (* Already taken care of. *)
- assert false
- | `Normalize_only ->
- filepath
- | `Create_path ->
- begin
- (try
- if not (Fc_Filepath.is_dir filepath)
- then
- (* [filepath] already exists, and it is a file. *)
- L.abort
- "cannot create directory as file %a already exists"
- Datatype.Filepath.pretty filepath
- with Sys_error _ ->
- (* [filepath] does not exist: create the directory path. *)
- ignore (mk_dir (filepath :> string)));
- filepath
- end
+ (try
+ if not (Fc_Filepath.is_dir filepath)
+ then
+ (* [filepath] already exists, and it is a file. *)
+ L.abort
+ "cannot create directory as file %a already exists"
+ Datatype.Filepath.pretty filepath
+ with Sys_error _ ->
+ (* [filepath] does not exist: create the directory path. *)
+ ignore (mk_dir (filepath :> string)));
+ filepath
end
let get_file ?(mode=`Normalize_only) s =
@@ -475,7 +469,7 @@ struct
val kernel_is_set: unit -> bool
end
- module User_dir (I: User_dir_input) = struct
+ module User_dir (I: User_dir_input) : Parameter_sig.User_dir = struct
include Make_specific_dir
(struct
let option_name = I.name
@@ -495,6 +489,9 @@ struct
]
let visible_ref = !Parameter_customize.is_visible_ref
end)
+
+ let get_dir ?mode s = get_dir ?mode s
+ let get_file ?mode s = get_file ?mode s
end
module Cache_dir () = User_dir
diff --git a/src/kernel_services/plugin_entry_points/plugin.mli b/src/kernel_services/plugin_entry_points/plugin.mli
index 890465ab053..2057743a4bb 100644
--- a/src/kernel_services/plugin_entry_points/plugin.mli
+++ b/src/kernel_services/plugin_entry_points/plugin.mli
@@ -54,18 +54,19 @@ module type S_no_log = sig
(** Handle the specific `cache' directory of the plug-in.
@since Frama-C+dev
*)
- module Cache_dir (): Parameter_sig.Specific_dir
+ module Cache_dir (): Parameter_sig.User_dir
(** Handle the specific `config' directory of the plug-in.
@since Neon-20140301
- @before Frama-C+dev this was not a functor
+ @before Frama-C+dev this was not a functor and one could expect the
+ directory to exist
*)
- module Config_dir (): Parameter_sig.Specific_dir
+ module Config_dir (): Parameter_sig.User_dir
(** Handle the specific `state' directory of the plug-in.
@since Frama-C+dev
*)
- module State_dir (): Parameter_sig.Specific_dir
+ module State_dir (): Parameter_sig.User_dir
val help: Cmdline.Group.t
(** The group containing option -*-help.
diff --git a/src/plugins/gui/gui_parameters.mli b/src/plugins/gui/gui_parameters.mli
index 2c665e2dc1b..e13bb21231e 100644
--- a/src/plugins/gui/gui_parameters.mli
+++ b/src/plugins/gui/gui_parameters.mli
@@ -24,7 +24,7 @@
include Plugin.S
-module Config_dir : Parameter_sig.Specific_dir
+module Config_dir : Parameter_sig.User_dir
module Project_name: Parameter_sig.String
(** Option -gui-project. *)
--
GitLab