diff --git a/src/kernel_services/ast_queries/cil_builtins.ml b/src/kernel_services/ast_queries/cil_builtins.ml
index 789e3120b093108723d8bf995668b124673f61d3..1a6dc1cdbda38ab9379de4084625ef1b51742409 100644
--- a/src/kernel_services/ast_queries/cil_builtins.ml
+++ b/src/kernel_services/ast_queries/cil_builtins.ml
@@ -387,14 +387,14 @@ let instantiate_available_templates type_table name (entry : builtin_template) =
let init_gcc_builtin_templates () =
let fp =
- Kernel.Share.get_file ~mode:`Must_exist "compliance/gcc_builtins.json"
+ Kernel.Share.get_file "compliance/gcc_builtins.json"
in
Json.init_builtin_templates ~default_compiler:GCC fp;
Gcc_builtin_templates_loaded.set true
let init_other_builtin_templates () =
let fp =
- Kernel.Share.get_file ~mode:`Must_exist "compliance/compiler_builtins.json"
+ Kernel.Share.get_file "compliance/compiler_builtins.json"
in
Json.init_builtin_templates fp
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index 9e5d005ddf2fe5ce5380c36a4a3657d3b3dd798e..234bd09e5f6a41fd1fc26b8e4cdbfa6958764ba3 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -270,7 +270,7 @@ let print_machdep fmt (m : Cil_types.mach) =
(if m.has__builtin_va_list then "has" else "has not") ;
end
-let machdep_dir () = Kernel.Share.get_dir ~mode:`Must_exist "machdeps"
+let machdep_dir () = Kernel.Share.get_dir "machdeps"
let regexp_machdep = Str.regexp "^machdep_\\([^.]*\\).yaml$"
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.ml b/src/kernel_services/cmdline_parameters/parameter_sig.ml
index 4f870b5976a2e7ef96a908cc8adce9669357b10f..833a3e4e2c9243242cafca4e8242133c9f945a63 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.ml
@@ -324,79 +324,71 @@ module type Filepath = sig
val is_empty: unit -> bool
end
-(** signature for searching files in a specific directory. *)
-module type Specific_dir = sig
+(** Dune site directories (share, lib, ...).
+ The root of a particular directory (say share) may not be unique, and these
+ are considered as installed files (although the user might provide another
+ location).
+ @since Frama-C+dev
+*)
+module type Dune_site_dir = sig
val set: Filepath.Normalized.t -> unit
- (** Sets the plugin <specific-dir> directory (without creating it). *)
+ (** Sets the <dune-site-dir> directory (without creating it). *)
val get: unit -> Filepath.Normalized.t
- (** @return the plugin <specific-dir> directory (without creating it). *)
+ (** @return the <dune-site-dir> directory (without creating it). *)
val is_set: unit -> bool
- (** @return whether the plugin <specific-dir> has been set. *)
-
- val get_dir:
- ?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
- <specific-dir> directory, of a sub-directory of the plugin <specific-dir>
- directory.
- @param mode determines how to handle the resulting path:
- + [Normalize_only] just normalizes the resulting path (default).
- + [Create_path] creates the resulting path, if does not exist.
- + [Must_exist] aborts if the resulting path does not exist. *)
-
- val get_file:
- ?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
- plugin <specific-dir> directory, of a file in the plugin <specific-dir>
- directory.
- @param mode determines how to handle the resulting path:
- + [Normalize_only] just normalizes the resulting path (default).
- + [Create_path] creates the dirname of resulting path, if does not exist.
- + [Must_exist] aborts if the resulting path does not exist. *)
-end
+ (** @return whether the <dune-site-dir> has been set. *)
-(** Specializes Specific_dir for dune site directories (share, lib, ...).
- We expect these directories to exist.
+ val get_dir: string -> Filepath.Normalized.t
+ (** [get_dir name] tries to find the directory named [name] in the
+ site. The function aborts if: [name] cannot be found or is a file instead
+ of a directory, otherwise it returns the path.
+ *)
- @since Frama-C+dev
-*)
-module type Dune_site_dir =sig
- include Specific_dir
-
- (** Refer to {!Specific_dir.get_dir} *)
- val get_dir:
- ?mode:[< `Normalize_only | `Must_exist > `Normalize_only ] ->
- string -> Filepath.Normalized.t
-
- (** Refer to {!Specific_dir.get_file} *)
- val get_file:
- ?mode:[< `Normalize_only | `Must_exist > `Normalize_only ] ->
- string -> Filepath.Normalized.t
+ val get_file: string -> Filepath.Normalized.t
+ (** [get_file name] tries to find the file named [name] in the
+ site. The function aborts if: [name] cannot be found or is a directory
+ instead of a file, otherwise it returns the path.
+ *)
end
(** Specializes Specific_dir for user directories (config, state, ...).
- We do not expect these directories to exist.
+ We do not expect these directories/files to exist.
@since Frama-C+dev
*)
module type User_dir = sig
- include Specific_dir
+ val set: Filepath.Normalized.t -> unit
+ (** Sets the <user-dir> directory (without creating it). *)
- (** Refer to {!Specific_dir.get_dir} *)
- val get_dir:
- ?mode:[< `Normalize_only | `Create_path > `Normalize_only ] ->
- string -> Filepath.Normalized.t
+ val get: unit -> Filepath.Normalized.t
+ (** @return the <user-dir> directory (without creating it). *)
+
+ val is_set: unit -> bool
+ (** @return whether the <user-dir> has been set. *)
+
+ val get_dir: ?create_path:bool -> string -> Filepath.Normalized.t
+ (** [get_dir ~create_path name] tries to get the directory [name].
+ The function aborts if:
+ - a file named [name] exists,
+ - creating a the directory fails.
- (** Refer to {!Specific_dir.get_file} *)
- val get_file:
- ?mode:[< `Normalize_only | `Create_path > `Normalize_only ] ->
- string -> Filepath.Normalized.t
+ Otherwise returns the path, and creates it if [create_path] is true
+ (it defaults to false).
+ *)
+
+ val get_file: ?create_path:bool -> string -> Filepath.Normalized.t
+ (** [get_file ~create_path name] tries to get the file [name].
+ The function aborts if:
+ - a directory named [name] exists,
+ - creating the path to the file fails.
+
+ Otherwise returns the path, and creates the directories that lead to the
+ file if [create_path] is true (it defaults to false). The file is *not*
+ created by the function.
+ *)
end
(* ************************************************************************** *)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 2ae26520799afc19b42ca28532f813d2bce285bd..deba5d3f6123601766a9dc6739cfc42cccaf63f6 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -326,45 +326,28 @@ struct
if is_visible && is_set () then [ get () ]
else List.map add_plugin System_config.Share.dirs
- let find relative =
+ let find ~is_dir relative =
let exception Found of Datatype.Filepath.t in
let check_presence dir =
let path = Datatype.Filepath.concat dir relative in
if Fc_Filepath.exists path then raise (Found path)
in
- try List.iter check_presence (dirs ()) ; None
- with Found path -> Some path
-
- let default relative =
- match dirs () with
- | [] -> assert false
- | x :: _ -> Datatype.Filepath.concat x relative
-
- let get_dir ?(mode=`Normalize_only) s =
- let path = find s in
- match mode, path with
- | `Normalize_only, None -> default s
- | (`Must_exist | `Normalize_only), Some p when Fc_Filepath.is_dir p -> p
- | (`Must_exist | `Normalize_only), Some p ->
- L.abort "%a is expected to be a directory" Datatype.Filepath.pretty p
- | `Must_exist, None ->
- L.abort "Could not find directory %s in Frama-C%s share"
- s (if is_kernel then "" else "/" ^ P.name)
-
- let get_file ?(mode=`Normalize_only) s =
- let dirname = Filename.dirname s in
- let basename = Filename.basename s in
- let dir = get_dir ~mode dirname in
- let path = Datatype.Filepath.concat dir basename in
- match mode with
- | `Must_exist when not @@ Fc_Filepath.exists path ->
- L.abort "Could not find file %s in Frama-C%s share"
- s (if is_kernel then "" else "/" ^ P.name)
- | (`Normalize_only | `Must_exist)
- when Fc_Filepath.exists path && Fc_Filepath.is_dir path ->
- L.abort "%a is expected to be a file"
+ try
+ List.iter check_presence (dirs ()) ;
+ L.abort
+ "Could not find %s %s in Frama-C%s share"
+ (if is_dir then "directory" else "file")
+ relative
+ (if is_kernel then "" else "/" ^ P.name)
+ with
+ | Found path when is_dir <> Fc_Filepath.is_dir path ->
+ L.abort "%a is expected to be a %s"
Datatype.Filepath.pretty path
- | (`Normalize_only | `Must_exist) -> path
+ (if is_dir then "directory" else "file")
+ | Found path -> path
+
+ let get_dir = find ~is_dir:true
+ let get_file = find ~is_dir:false
end
module Make_user_dir
@@ -425,26 +408,31 @@ struct
with Unix.Unix_error _ ->
L.abort "cannot create %s directory `%a'" D.name Fc_Filepath.Normalized.pretty d'
- let get_dir ?(mode=`Normalize_only) s =
+ let get_dir ?(create_path=false) s =
let dir = Datatype.Filepath.concat (get ()) s in
- match mode with
- | `Normalize_only -> dir
- | `Create_path ->
- try
- if not @@ Fc_Filepath.is_dir dir
- then
- L.abort
- "cannot create directory as file %a already exists"
+ if Fc_Filepath.exists dir then
+ begin
+ if Fc_Filepath.is_dir dir then dir
+ else
+ L.abort "%a is expected to be a directory"
Datatype.Filepath.pretty dir
+ end
+ else
+ begin
+ if create_path then ((ignore (mk_dir (dir :> string))) ; dir)
else dir
- with Sys_error _ ->
- ignore (mk_dir (dir :> string)); dir
+ end
- let get_file ?(mode=`Normalize_only) s =
- let base_dir = get_dir ~mode @@ Filename.dirname s in
+ let get_file ?create_path s =
+ let base_dir = get_dir ?create_path @@ Filename.dirname s in
(* No need to create anything here, as the path of sub-directories has
been already created by [get_dir] for computing [base_dir]. *)
- Datatype.Filepath.concat base_dir @@ Filename.basename s
+ let path = Datatype.Filepath.concat base_dir @@ Filename.basename s in
+ if Fc_Filepath.exists path && Fc_Filepath.is_dir path then
+ L.abort "%a is expected to be a file, found a directory"
+ Datatype.Filepath.pretty path
+ else
+ path
end
module Session = Make_user_dir
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index be5d5eb32d2a062c937c4ad3f6fbacb69418a82d..f0780382e5e2da28d3ace5b32ea24c179caeb828 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -23,7 +23,7 @@
open Cil_types
open Cil_datatype
-let rtl_file () = Options.Share.get_file ~mode:`Must_exist "e_acsl.h"
+let rtl_file () = Options.Share.get_file "e_acsl.h"
(* create the RTL AST in a fresh project *)
let create_rtl_ast prj =
diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml
index 8a62282176800b1a76e1432543bd0e199de55c43..5f754a5e98b29b3b7a3494f514e7d63eb5824703 100644
--- a/src/plugins/gui/gtk_helper.ml
+++ b/src/plugins/gui/gtk_helper.ml
@@ -48,7 +48,7 @@ let framac_logo, framac_icon =
module Configuration = struct
include Cilconfig
let configuration_file () =
- Gui_parameters.Config_dir.get_file ~mode:`Create_path "frama-c-gui.config"
+ Gui_parameters.Config_dir.get_file ~create_path:true "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/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 25d3218843795c5157b54a1685279812b6263ce3..8cd2d6366bb5baa79e2c7c6919e4fb2dc60d3ad9 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -58,7 +58,7 @@ let get_why3_conf = Conf.memoize
let main = Why3.Whyconf.get_main config in
let ld =
(WpContext.directory () :> string)::
- ((Wp_parameters.Share.get_dir ~mode:`Must_exist "why3") :> string)::
+ ((Wp_parameters.Share.get_dir "why3") :> string)::
(Why3.Whyconf.loadpath main) in
{ env = Why3.Env.create_env ld ; config = main }
end
diff --git a/src/plugins/wp/driver.mll b/src/plugins/wp/driver.mll
index a15af98a9889f7d51ded4e6b8579bec6f6afeaa7..cde182958a1d8429de7c3442f185eb13bd7ac82c 100644
--- a/src/plugins/wp/driver.mll
+++ b/src/plugins/wp/driver.mll
@@ -491,7 +491,7 @@ and bal = parse
let descr = String.concat "," drvs in
let includes =
let directories =
- [Wp_parameters.Share.get_dir ~mode:`Must_exist "."]
+ [Wp_parameters.Share.get_dir "."]
in
if Wp_parameters.has_dkey dkey then
Wp_parameters.debug ~dkey "Included directories:%t"
@@ -509,7 +509,7 @@ and bal = parse
then file
else LogicBuiltins.find_lib file)
drivers in
- let default = Wp_parameters.Share.get_file ~mode:`Must_exist "wp.driver" in
+ let default = Wp_parameters.Share.get_file "wp.driver" in
let feedback = Wp_parameters.Share.is_set () in
let ontty = if feedback then `Message else `Transient in
load_file ~ontty default;
diff --git a/tests/libc/check_parsing_individual_headers.ml b/tests/libc/check_parsing_individual_headers.ml
index 3f9c35918acef2fdf3f119c27689c2d6d7f5fd3d..21969ad8745198a0bd7e76a325806cafab756894 100644
--- a/tests/libc/check_parsing_individual_headers.ml
+++ b/tests/libc/check_parsing_individual_headers.ml
@@ -14,7 +14,7 @@ let blacklist libc_dir =
(* only goes down one level, which is enough for the libc *)
let collect_headers () =
- let libc_dir = Kernel.Share.get_dir ~mode:`Must_exist "libc" in
+ let libc_dir = Kernel.Share.get_dir "libc" in
let libc_dir_files = Array.to_list (Sys.readdir (libc_dir :> string)) in
let contents =
List.map (Filename.concat (libc_dir :> string)) libc_dir_files
diff --git a/tests/misc/share_directory.t/directories.ml b/tests/misc/share_directory.t/directories.ml
index 4b22ebb1bd6fcaefce14c8189f24f28505fba651..7dd3fb54bc9cb2b00c12d0a85f7077b8a16ade0e 100644
--- a/tests/misc/share_directory.t/directories.ml
+++ b/tests/misc/share_directory.t/directories.ml
@@ -19,27 +19,21 @@ let run_all () =
Kernel.feedback "IS_SET %b" (Share.is_set ()) ;
Self.feedback "path (dir)" ;
- never_fail_get (Share.get_dir ~mode:`Must_exist) "path" ;
never_fail_get Share.get_dir "path" ;
Self.feedback "path/file.txt (file)" ;
- never_fail_get (Share.get_file ~mode:`Must_exist) "path/file.txt" ;
never_fail_get Share.get_file "path/file.txt" ;
Self.feedback "foo (dir)" ;
- never_fail_get (Share.get_dir ~mode:`Must_exist) "foo" ;
never_fail_get Share.get_dir "foo" ;
Self.feedback "foo.txt (file)" ;
- never_fail_get (Share.get_file ~mode:`Must_exist) "foo.txt" ;
never_fail_get Share.get_file "foo.txt" ;
Self.feedback "path (file)" ;
- never_fail_get (Share.get_file ~mode:`Must_exist) "path" ;
never_fail_get Share.get_file "path" ;
Self.feedback "path/file.txt" ;
- never_fail_get (Share.get_dir ~mode:`Must_exist) "path/file.txt" ;
never_fail_get Share.get_dir "path/file.txt"
diff --git a/tests/misc/share_directory.t/run.t b/tests/misc/share_directory.t/run.t
index e6a93fda668b524e48239f87587a6eceafe968a9..8d599ebbd000c37cafdcaf5909a2b0eaff663a7a 100644
--- a/tests/misc/share_directory.t/run.t
+++ b/tests/misc/share_directory.t/run.t
@@ -5,22 +5,16 @@ Basic case
[kernel] IS_SET false
[dirs] path (dir)
[dirs] Found: _build/install/default/share/frama-c/share/dirs/path
- [dirs] Found: _build/install/default/share/frama-c/share/dirs/path
[dirs] path/file.txt (file)
[dirs] Found: _build/install/default/share/frama-c/share/dirs/path/file.txt
- [dirs] Found: _build/install/default/share/frama-c/share/dirs/path/file.txt
[dirs] foo (dir)
[dirs] User Error: Could not find directory foo in Frama-C/directories share
- [dirs] Found: _build/install/default/share/frama-c/share/dirs/foo
[dirs] foo.txt (file)
[dirs] User Error: Could not find file foo.txt in Frama-C/directories share
- [dirs] Found: _build/install/default/share/frama-c/share/dirs/foo.txt
[dirs] path (file)
[dirs] User Error: _build/install/default/share/frama-c/share/dirs/path is expected to be a file
- [dirs] User Error: _build/install/default/share/frama-c/share/dirs/path is expected to be a file
[dirs] path/file.txt
[dirs] User Error: _build/install/default/share/frama-c/share/dirs/path/file.txt is expected to be a directory
- [dirs] User Error: _build/install/default/share/frama-c/share/dirs/path/file.txt is expected to be a directory
With option
$ cp -r share copied
@@ -28,19 +22,13 @@ With option
[kernel] IS_SET true
[dirs] path (dir)
[dirs] Found: copied/path
- [dirs] Found: copied/path
[dirs] path/file.txt (file)
[dirs] Found: copied/path/file.txt
- [dirs] Found: copied/path/file.txt
[dirs] foo (dir)
[dirs] User Error: Could not find directory foo in Frama-C/directories share
- [dirs] Found: copied/foo
[dirs] foo.txt (file)
[dirs] User Error: Could not find file foo.txt in Frama-C/directories share
- [dirs] Found: copied/foo.txt
[dirs] path (file)
[dirs] User Error: copied/path is expected to be a file
- [dirs] User Error: copied/path is expected to be a file
[dirs] path/file.txt
[dirs] User Error: copied/path/file.txt is expected to be a directory
- [dirs] User Error: copied/path/file.txt is expected to be a directory
diff --git a/tests/misc/user_directories.unix.t/directories.ml b/tests/misc/user_directories.unix.t/directories.ml
index 83d54bde7fcfd2e60214737bc3e6cab1dc63cc89..bcd43afd2f5d0c8a253b1e19b6035d46f34a5b81 100644
--- a/tests/misc/user_directories.unix.t/directories.ml
+++ b/tests/misc/user_directories.unix.t/directories.ml
@@ -19,15 +19,17 @@ module Session = Self.Session
let run_all () =
if OnlyCache.get ()
- then
- ignore @@ Cache.get_dir ~mode:`Create_path "created"
+ then begin
+ ignore @@ Cache.get_dir ~create_path:true "created" ;
+ ignore @@ Cache.get_file "created" (* < fails *)
+ end
else
try
- ignore @@ Cache.get_dir ~mode:`Create_path "created" ;
- ignore @@ Config.get_dir ~mode:`Create_path "created" ;
- ignore @@ State.get_dir ~mode:`Create_path "created" ;
- ignore @@ Session.get_dir ~mode:`Create_path "created" ;
- ignore @@ Session.get_file ~mode:`Create_path "created_filepath/file" ;
+ ignore @@ Cache.get_dir ~create_path:true "created" ;
+ ignore @@ Config.get_dir ~create_path:true "created" ;
+ ignore @@ State.get_dir ~create_path:true "created" ;
+ ignore @@ Session.get_dir ~create_path:true "created" ;
+ ignore @@ Session.get_file ~create_path:true "created_filepath/file" ;
(* Here: ~mode:`Normalize_only *)
diff --git a/tests/misc/user_directories.unix.t/run.t b/tests/misc/user_directories.unix.t/run.t
index ca5529bfe44258bde3bb36408fb0fe07e46ad79a..3020a327dce0d8eb319aea28fcf9585653ea646a 100644
--- a/tests/misc/user_directories.unix.t/run.t
+++ b/tests/misc/user_directories.unix.t/run.t
@@ -177,21 +177,33 @@ Customized via options plug-in level
Customized plug-in option > plug-in var
$ HOME=home FRAMAC_DIRS_CACHE=cache_bad dune exec -- frama-c -dirs-cache-only -dirs-cache cache
[dirs] Warning: created cache directory `cache/created'
+ [dirs] User Error: cache/created is expected to be a file, found a directory
+ [kernel] Plug-in dirs aborted: invalid user input.
+ [1]
$ rm -rf home cache
Customized plug-in var > kernel option
$ HOME=home FRAMAC_DIRS_CACHE=cache dune exec -- frama-c -dirs-cache-only -cache cache_bad
[dirs] Warning: created cache directory `cache/created'
+ [dirs] User Error: cache/created is expected to be a file, found a directory
+ [kernel] Plug-in dirs aborted: invalid user input.
+ [1]
$ rm -rf home cache
Customized kernel option > kernel var
$ HOME=home FRAMAC_CACHE=cache_bad dune exec -- frama-c -dirs-cache-only -cache cache
[dirs] Warning: created cache directory `cache/dirs/created'
+ [dirs] User Error: cache/dirs/created is expected to be a file, found a directory
+ [kernel] Plug-in dirs aborted: invalid user input.
+ [1]
$ rm -rf home cache
Customized kernel var > xdg var
$ HOME=home XDG_CACHE_HOME=cache_bad FRAMAC_CACHE=cache dune exec -- frama-c -dirs-cache-only
[dirs] Warning: created cache directory `cache/dirs/created'
+ [dirs] User Error: cache/dirs/created is expected to be a file, found a directory
+ [kernel] Plug-in dirs aborted: invalid user input.
+ [1]
$ rm -rf home cache
Bad home value
@@ -214,7 +226,7 @@ File already exists were a directory is expected
$ mkdir cache
$ touch cache/created
$ HOME=home dune exec -- frama-c -dirs-cache cache
- [dirs] User Error: cannot create directory as file cache/created already exists
+ [dirs] User Error: cache/created is expected to be a directory
[kernel] Plug-in dirs aborted: invalid user input.
[1]
$ rm -rf cache