Merge branch 'feature/andre/filepath-concat-separator' into 'master'

[Filepath] add "/" when concatenating paths via Filepath.Normalized.concat

See merge request frama-c/frama-c!2867

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)

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

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,

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
 
 (* -------------------------------------------------------------------------- *)