diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index 060ea5842489ddacd0c62b317e5f6ad4852c9880..4906addb8276c4ef313be7fbd09c7f76b575709d 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -295,33 +295,19 @@ module type Filepath = S with type t = Filepath.Normalized.t
(** signature for searching files in a specific directory. *)
module type Specific_dir = sig
- exception No_dir
-
- val force_dir: bool
- (** 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 *)
-
- val dir: ?error:bool -> unit -> Filepath.Normalized.t
- (** [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 -> Filepath.Normalized.t
- (** [file basename] returns the complete filename of a file stored in [dir
- ()]. If there is no such directory, 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 set: Filepath.Normalized.t -> unit
+ val get: unit -> Filepath.Normalized.t
+ val is_set: unit -> bool
- module Dir_name: Filepath
- (** Option [-<short-name>-<specific-dir>]. *)
+ val get_dir:
+ ?mode:[`Create_path | `Normalize_only | `Must_exist ] ->
+ string ->
+ Filepath.Normalized.t
+ val get_file:
+ ?mode:[`Create_path | `Normalize_only | `Must_exist ] ->
+ string ->
+ Filepath.Normalized.t
end
(* ************************************************************************** *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index d437277a6da46c91e6edf8c6f882e1809331945f..41bde48cfc510df064794f528fca305d8401fee9 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -837,9 +837,9 @@ module Journal = struct
let default =
let dir =
(* duplicate code from Plugin.Session *)
- if Session.Dir_name.is_set ()
+ if Session.is_set ()
then
- (Session.Dir_name.get () :> string)
+ (Session.get () :> string)
else
try Sys.getenv "FRAMAC_SESSION"
with Not_found -> "./.frama-c"
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 4b7b4a2de3b925a0d3700d224e50f45bb70519a6..ecc78065fc36d43580326ef27ed77b83c880cf5d 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -299,13 +299,11 @@ struct
(D: sig
val dirs: unit -> string list
val visible_ref: bool
- val force_dir: bool
end)
=
struct
let is_visible = D.visible_ref
- let force_dir = D.force_dir
let is_kernel = is_kernel () (* the side effect must be applied right now *)
let () =
@@ -323,65 +321,95 @@ struct
let file_kind = ""
end)
- exception No_dir
-
let mk_dir d =
try
Extlib.mkdir ~parents:true d 0o755;
L.warning "creating %s directory `%s'" O.option_name d;
d
with Unix.Unix_error _ ->
- L.warning "cannot create %s directory `%s'" O.option_name d;
- raise No_dir
-
- let rec get_and_check_dirs error = function
- | [] ->
- raise No_dir
- | d::l ->
- if (try Sys.is_directory d with Sys_error _ -> false) then d
- else
- get_and_check_dirs error l
-
- let get_and_check_dirs ?(error=true) = function
- | [] ->
- if error then
- L.abort "no %s directories to look into" O.option_name
- else
- raise No_dir
- | (first::_) as l ->
- try
- get_and_check_dirs error l
- with
- | No_dir when error ->
- L.abort "no %s directory for plug-in `%s' among %a"
- O.option_name
- P.name
- Pretty_utils.(pp_list ~sep:",@ " Format.pp_print_string) l
- | No_dir when force_dir ->
- (* create the parent, if it does not exist *)
- let p = Filename.dirname first in
- if not (try Sys.is_directory p with Sys_error _ -> false) then
- ignore (mk_dir p);
- mk_dir first
-
- let dir ?error () =
- (* get the specified dir if any *)
- let d = if is_visible then (Dir_name.get () :> string) else empty_string in
- let dirs =
- if d = empty_string
+ L.abort "cannot create %s directory `%s'" O.option_name d
+
+ let set filepath = Dir_name.set filepath
+ let get () = Dir_name.get ()
+ let is_set () = Dir_name.is_set ()
+
+ let base_dirs () =
+ (* Get the specified dir if any. *)
+ let plugin_base_dir =
+ if is_visible
+ then Dir_name.get ()
+ else Datatype.Filepath.dummy
+ in
+ if not (plugin_base_dir = Datatype.Filepath.dummy)
+ then [plugin_base_dir]
+ else begin
+ (* No specified dir: look for the default one. *)
+ let dirs = D.dirs () in
+ assert (dirs <> []);
+ if is_kernel
then
- (* no specified dir: look for the default one. *)
- if is_kernel
- then D.dirs ()
- else List.map (fun x -> x ^ "/" ^ plugin_subpath) (D.dirs ())
+ List.map Datatype.Filepath.of_string dirs
else
- [d]
- in
- Datatype.Filepath.of_string (get_and_check_dirs ?error dirs)
+ List.map
+ (fun x -> Datatype.Filepath.of_string (x ^ "/" ^ plugin_subpath))
+ dirs
+ end
- let file ?error f =
- let dir = dir ?error () in
- Datatype.Filepath.concat dir ("/" ^ f)
+ let get_dir ?(mode=`Normalize_only) s =
+ match mode with
+ | `Must_exist ->
+ begin
+ let dir =
+ let exception Found of Datatype.Filepath.t in
+ try
+ List.fold_left
+ (fun dummy d ->
+ let name = Datatype.Filepath.concat d ("/" ^ s) in
+ if Sys.file_exists (name :> string)
+ then raise (Found name)
+ else dummy)
+ None
+ (base_dirs ())
+ with Found d ->
+ Some d
+ in
+ match dir with
+ | None ->
+ L.abort "no directory %s exist in %s directories" s O.option_name
+ | Some d -> d
+ end
+ | _ ->
+ begin
+ 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 ->
+ ignore (mk_dir (filepath :> string));
+ filepath
+ end
+
+ let get_file ?(mode=`Normalize_only) s =
+ let s_dirname = Filename.dirname s in
+ let base_dir = get_dir ~mode s_dirname in
+ let s_basename = Filename.basename s in
+ let filepath = Datatype.Filepath.concat base_dir ("/" ^ s_basename) in
+ match mode with
+ | `Must_exist ->
+ if Sys.file_exists (filepath :> string)
+ then filepath
+ else L.abort "no file %s exist in %s directories" s O.option_name
+ | `Normalize_only ->
+ filepath
+ | `Create_path ->
+ filepath
end
@@ -396,7 +424,6 @@ struct
(struct
let dirs () = Fc_config.datadirs
let visible_ref = !share_visible_ref
- let force_dir = false
end)
module Session =
@@ -413,11 +440,10 @@ struct
try Sys.getenv "FRAMAC_SESSION"
with Not_found -> "./.frama-c"]
let visible_ref = !session_visible_ref
- let force_dir = true
end)
let () =
if is_kernel ()
- then Journal.get_session_file := (fun s -> Session.file ~error:false s)
+ then Journal.get_session_file := (fun s -> Session.get_file s)
module Config =
Make_specific_dir
@@ -445,7 +471,6 @@ struct
d ^ if vis then "/frama-c" else "/.frama-c"
]
let visible_ref = !config_visible_ref
- let force_dir = true
end)
let help = add_group "Getting Information"
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 285438e7d87be09f19608712a09634902f61c0af..0f4d38ef3fb6f37bd2ab33dd37c1f0d1ff021063 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -30,7 +30,7 @@ open Cil_datatype
let library_files () =
List.map
- (fun d -> Options.Share.file ~error:true d)
+ (fun d -> Options.Share.get_file ~mode:`Must_exist d)
[ "e_acsl_gmp_api.h";
"e_acsl.h" ]
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index c8027aa8d6f690b468b5aae66a1e98e8e957fdfc..a7f26523d4c08bd8b4028b8522d8f3073ecb857c 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -38,7 +38,7 @@ let extended_ast_project: extended_project ref = ref To_be_extended
let unmemoized_extend_ast () =
let extend () =
- let share = Options.Share.dir ~error:true () in
+ let share = Options.Share.get_dir ~mode:`Must_exist "." in
Options.feedback ~level:3 "setting kernel options for E-ACSL.";
Kernel.CppExtraArgs.add
(Format.asprintf " -DE_ACSL_MACHDEP=%s -I%a/memory_model"
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 298d75d184f3a4716f4ba7573be412659061ef06..9253046cb295846e25da7e910bda4095d3ccd40c 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -47,8 +47,7 @@ let framac_logo, framac_icon =
module Configuration = struct
include Cilconfig
let configuration_file () =
- try (Gui_parameters.Config.file ~error:false "frama-c-gui.config")
- with Gui_parameters.Config.No_dir -> Datatype.Filepath.dummy
+ Gui_parameters.Config.get_file "frama-c-gui.config"
let load () = loadConfiguration (configuration_file ())
let save () = saveConfiguration (configuration_file ())
let reset () = Extlib.safe_remove (configuration_file () :> string);
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index 9ad747a9afb3196f58a6a8712e520b6d7a873866..a1f4594ddba1101cda469be56dd43fe3d88e5875 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -165,7 +165,7 @@ class visitor fmt c =
let df = D_file f in
if not (List.mem df deps) then deps <- df :: deps
- method add_shared f = self#add_dfile ((Wp_parameters.Share.file ~error:true f) :> string)
+ method add_shared f = self#add_dfile ((Wp_parameters.Share.get_file ~mode:`Must_exist f) :> string)
method add_library f = self#add_dfile f
method on_cluster c = deps <- (D_cluster c) :: deps
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index b4074ed1bb1b9f989a06f9e145794ec2aee52a6c..2b31bf272f2bded093f4c811297210f43fc01cdb 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -51,7 +51,7 @@ let get_why3_env = Env.memoize
let main = Why3.Whyconf.get_main config in
let ld =
(WpContext.directory ())::
- ((Wp_parameters.Share.file "why3") :> string)::
+ ((Wp_parameters.Share.get_file "why3") :> string)::
(Why3.Whyconf.loadpath main) in
Why3.Env.create_env ld
end
@@ -786,7 +786,7 @@ class visitor (ctx:context) c =
let copy_file source =
if not (Datatype.Filepath.equal
(Datatype.Filepath.of_string (Filename.dirname source))
- (Wp_parameters.Share.dir ()))
+ (Wp_parameters.Share.get_dir "."))
then
let tgtdir = WpContext.directory () in
let why3src = Filename.basename source in
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index d541988a96627f9bc479832c2b7ecf9422b6a758..1a13f28d9e6b5f17eb2ebc38f3ddfc6435aae216 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -501,8 +501,8 @@ and bal = parse
let descr = String.concat "," drvs in
let includes =
let directories =
- try [(Wp_parameters.Share.dir ~error:false () :> string)]
- with Wp_parameters.Share.No_dir -> [] in
+ [(Wp_parameters.Share.get_dir "." :> string)]
+ in
if Wp_parameters.has_dkey dkey then
Wp_parameters.debug ~dkey "Included directories:%t"
(fun fmt ->
@@ -519,8 +519,8 @@ and bal = parse
then Filepath.normalize file
else LogicBuiltins.find_lib file)
drivers in
- let default = Wp_parameters.Share.file ~error:true "wp.driver" in
- let feedback = Wp_parameters.Share.Dir_name.is_set () in
+ let default = Wp_parameters.Share.get_file ~mode:`Must_exist "wp.driver" in
+ let feedback = Wp_parameters.Share.is_set () in
let ontty = if feedback then `Message else `Transient in
load_file ~ontty (default :> string);
List.iter load_file drivers
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index bc0cf0c9d05b4bc49359bbba300b655823f449bc..b6c45ae76c0d113fd33ed5378b7a1e197ae4280c 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -557,7 +557,7 @@ let spawn_wp_proofs_iter ~mode iter_on_goals =
if mode.tactical || mode.provers<>[] then
begin
let server = ProverTask.server () in
- ignore (Wp_parameters.Share.dir ()); (* To prevent further errors *)
+ ignore (Wp_parameters.Share.get_dir "."); (* To prevent further errors *)
iter_on_goals
(fun goal ->
if mode.tactical
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index c1d7d6ad7193254c12a6a6f973fa8c5913f3a775..7d8a2e381c2f113d42356837e80079a93d62a117 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1118,21 +1118,21 @@ let get_output_dir d =
let default = Sys.getcwd () ^ "/.frama-c"
let has_session () =
- Session.Dir_name.is_set () ||
+ Session.is_set () ||
( Sys.file_exists default && Sys.is_directory default )
let get_session ~force () =
if force then
- Session.dir ~error:false ()
+ Session.get_dir "."
else
- if Session.Dir_name.is_set () then
- Session.Dir_name.get ()
+ if Session.is_set () then
+ Session.get ()
else
- Session.dir ~error:false ()
+ Session.get_dir "."
let get_session_dir ~force d =
let base = get_session ~force () in
- let path = Format.asprintf "%a/%s" Datatype.Filepath.pp_abs base d in
+ let path = Format.asprintf "%s/%s" (base :> string) d in
if force then make_output_dir path ; path
(* -------------------------------------------------------------------------- *)