diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml index 6ee44be08b9fc929a2c29c88efe3cb2a48d37373..2be6085f39d0531180e0d190ca4231cb4b06c2b6 100644 --- a/src/libraries/stdlib/extlib.ml +++ b/src/libraries/stdlib/extlib.ml @@ -233,17 +233,27 @@ external address_of_value: 'a -> int = "address_of_value" [@@noalloc] hence interrupting the process, might not work: child processes still need to run some daemons, such as [flush_all] which is registered by default. *) -let rec mkdir ?(parents=false) name perm = - try Unix.mkdir name perm - with - | Unix.Unix_error (Unix.ENOENT,_,_) when parents -> - let parent_name = Filename.dirname name in - if name <> parent_name then - begin - mkdir ~parents parent_name perm; - Unix.mkdir name perm - end - | e -> raise e +let rec mkdir ?(parents=false) (name: Filepath.Normalized.t) perm = + if Filepath.exists name then + if not (Filepath.is_dir name) then + failwith (Format.asprintf "mkdir: %a exists but is not a directory" + Filepath.Normalized.pretty name) + else false + else begin + begin + try Unix.mkdir (name:>string) perm + with + | Unix.Unix_error (Unix.ENOENT,_,_) when parents -> + let parent_name = Filepath.dirname name in + if name <> parent_name then + begin + ignore (mkdir ~parents parent_name perm); + Unix.mkdir (name:>string) perm + end + | e -> raise e + end; + true + end let pid = Unix.getpid () let safe_at_exit f = diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli index 3b158d16c21a20457d0077ca7939f34b4e6a0257..e4c49118dd544b25d994c141d5d54700adede7d7 100644 --- a/src/libraries/stdlib/extlib.mli +++ b/src/libraries/stdlib/extlib.mli @@ -256,7 +256,7 @@ external address_of_value: 'a -> int = "address_of_value" [@@noalloc] (** {2 System commands} *) (* ************************************************************************* *) -val mkdir : ?parents:bool -> string -> Unix.file_perm -> unit +val mkdir : ?parents:bool -> Filepath.Normalized.t -> Unix.file_perm -> bool (** [mkdir ?parents name perm] creates directory [name] with permission [perm]. If [parents] is true, recursively create parent directories if needed. [parents] defaults to false. @@ -264,8 +264,13 @@ val mkdir : ?parents:bool -> string -> Unix.file_perm -> unit and then fail to create the children, e.g. if [perm] does not allow user execution of the created directory. This will leave the filesystem in a modified state before raising an exception. + Returns [true] if the directory was created, [false] otherwise. @raise Unix.Unix_error if cannot create [name] or its parents. - @since 19.0-Potassium *) + @since 19.0-Potassium + @since Frama-C+dev added check for existence of path (error if exists + but not a directory, otherwise do nothing if directory already exists). + Changed type of [name] argument and return type. +*) val safe_at_exit : (unit -> unit) -> unit (** Register function to call with [Stdlib.at_exit], but only