diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index a02122eaa141ba335726ccd72c76267f023e2bd4..27a3b48fbf2adf47570dd02d043655ec241de3a3 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 4e02418356f54681e995a49fb8bb5a9baca1d319..8264a4583a8b7ac7ff6aa08780e178a44d83c46b 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 41c56ec816717618e136353f659045276feadad5..d876c02227cdf527e281a28a86ccf8a89b279f15 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 85a91ef237393229e0aefb1a077ff92e76f8fe13..c9861dd56ffaffaa30307dd4dddbc5bb39fc0148 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
 
 (* -------------------------------------------------------------------------- *)