From a417261e71804ca7500aee36ec01fa87ba7cca84 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 30 Sep 2020 15:03:50 +0200
Subject: [PATCH] [Filepath] add "/" when concatenating paths via
Filepath.Normalized.concat
---
src/kernel_services/plugin_entry_points/plugin.ml | 6 +++---
src/libraries/utils/filepath.ml | 2 +-
src/libraries/utils/filepath.mli | 8 ++++++--
src/plugins/wp/wp_parameters.ml | 6 +++---
4 files changed, 13 insertions(+), 9 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index a02122eaa14..27a3b48fbf2 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -368,7 +368,7 @@ struct
try
List.fold_left
(fun dummy d ->
- let name = Datatype.Filepath.concat d ("/" ^ s) in
+ let name = Datatype.Filepath.concat d s in
if Sys.file_exists (name :> string)
then raise (Found name)
else dummy)
@@ -389,7 +389,7 @@ struct
let filepath =
match base_dirs () with
| [] -> assert false
- | d :: _ -> Datatype.Filepath.concat d ("/" ^ s)
+ | d :: _ -> Datatype.Filepath.concat d s
in
match mode with
| `Must_exist ->
@@ -417,7 +417,7 @@ struct
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
+ let filepath = Datatype.Filepath.concat base_dir s_basename in
match mode with
| `Must_exist ->
if Sys.file_exists (filepath :> string)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 4e02418356f..8264a4583a8 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -237,7 +237,7 @@ module Normalized = struct
type t = string
let of_string ?existence ?base_name s = normalize ?existence ?base_name s
- let concat ?existence t s = normalize ?existence (t ^ s)
+ let concat ?existence t s = normalize ?existence (t ^ "/" ^ s)
let to_pretty_string s = pretty s
let equal : t -> t -> bool = (=)
let compare = String.compare
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 41c56ec8167..d876c02227c 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -103,8 +103,12 @@ module Normalized: sig
*)
val of_string: ?existence:existence -> ?base_name:string -> string -> t
- (** @return the normalized path resulting from the concatenation of the given
- path and string. *)
+ (** [concat ~existence dir file] returns the normalized path
+ resulting from the concatenation of [dir] ^ "/" ^ [file].
+ The resulting path must respect [existence].
+
+ @since Frama-C+dev
+ *)
val concat: ?existence:existence -> t -> string -> t
(** [to_pretty_string p] returns [p] prettified,
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 85a91ef2373..c9861dd56ff 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1189,12 +1189,12 @@ let get_output () =
let name = Project.get_unique_name project in
if name = "default" then base
else
- let dir = Datatype.Filepath.concat base ("/" ^ name) in
+ let dir = Datatype.Filepath.concat base name in
make_output_dir (dir :> string) ; dir
let get_output_dir d =
let base = get_output () in
- let path = Datatype.Filepath.concat base ("/" ^ d) in
+ let path = Datatype.Filepath.concat base d in
make_output_dir (path :> string) ; path
(* -------------------------------------------------------------------------- *)
@@ -1218,7 +1218,7 @@ let get_session ~force () =
let get_session_dir ~force d =
let base = get_session ~force () in
- let path = Datatype.Filepath.concat base ("/" ^ d) in
+ let path = Datatype.Filepath.concat base d in
if force then make_output_dir (path :> string) ; path
(* -------------------------------------------------------------------------- *)
--
GitLab