diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 9aecb292da713a7214e26574f10a62229de8f029..7448601a76488d7a93c75987b7b33f8a9e6d434e 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -138,8 +138,9 @@ let () =
 
 (* Load Frama-c from disk if required *)
 let load_binary () =
-  let filename = Kernel.LoadState.get () in
-  if filename <> "" then begin
+  let filepath = Kernel.LoadState.get () in
+  if filepath <> Filepath.Normalized.unknown then begin
+    let filename = Filepath.Normalized.to_pretty_string filepath in
     try
       Project.load_all filename
     with Project.IOError s ->
diff --git a/src/kernel_services/cmdline_parameters/parameter_builder.ml b/src/kernel_services/cmdline_parameters/parameter_builder.ml
index d74de525bfa58a548f5990215ab66750e7423ef6..d20cc20285af3175eabfb4202058616734e426ae 100644
--- a/src/kernel_services/cmdline_parameters/parameter_builder.ml
+++ b/src/kernel_services/cmdline_parameters/parameter_builder.ml
@@ -442,6 +442,91 @@ struct
   module Empty_string(X: Parameter_sig.Input_with_arg) =
     String(struct include X let default = empty_string end)
 
+  (* ************************************************************************ *)
+  (** {3 Filepath} *)
+  (* ************************************************************************ *)
+
+  module Fc_Filepath = Filepath
+
+  module Filepath
+      (X: sig
+         include Parameter_sig.Input_with_arg
+         val existence : Parameter_sig.existence
+       end) =
+  struct
+
+    exception No_file
+    exception File_exists
+
+    include Build
+        (struct
+          include Datatype.Filepath
+          include X
+          let default () = Filepath.Normalized.unknown
+          let functor_name = "Filepath"
+        end)
+
+    let check_existence existence fp =
+      match existence with
+      | Parameter_sig.Indifferent -> ()
+      | Parameter_sig.Must_exist ->
+        if not (Sys.file_exists (Filepath.Normalized.to_pretty_string fp)) then
+          raise No_file
+      | Parameter_sig.Must_not_exist ->
+        if Sys.file_exists (Filepath.Normalized.to_pretty_string fp) then
+          raise File_exists
+
+    let existence = X.existence
+
+    let convert f oldstr newstr =
+      let oldfp = Filepath.Normalized.to_pretty_string oldstr in
+      let newfp = Filepath.Normalized.to_pretty_string newstr in
+      f oldfp newfp
+
+    let set fp = check_existence existence fp ; set fp
+
+    let set_str s = set (Filepath.Normalized.of_string s)
+
+    let add_option name =
+      Cmdline.add_option
+        name
+        ~argname:X.arg_name
+        ~help:X.help
+        ~visible:is_visible
+        ~ext_help:!Parameter_customize.optional_help_ref
+        ~plugin:P.shortname
+        ~group
+        stage
+        (Cmdline.String set_str)
+
+    let parameter_get fp = Filepath.Normalized.to_pretty_string (get fp)
+    let parameter_add_set_hook f = add_set_hook (convert f)
+    let parameter_add_update_hook f = add_update_hook (convert f)
+
+    let parameter =
+      let accessor =
+        Typed_parameter.String
+          ({ Typed_parameter.get = parameter_get;
+             set = set_str;
+             add_set_hook = parameter_add_set_hook;
+             add_update_hook = parameter_add_update_hook },
+           fun () -> [])
+      in
+      let p =
+	Typed_parameter.create ~name ~help:X.help ~accessor ~is_set
+      in
+      add_parameter !Parameter_customize.group_ref stage p;
+      add_option X.option_name;
+      Parameter_customize.reset ();
+      if is_dynamic then
+	let plugin = empty_string in
+	Dynamic.register
+          ~plugin X.option_name Typed_parameter.ty ~journalize:false p
+      else
+	p
+
+  end
+
   (* ************************************************************************ *)
   (** {3 Collections} *)
   (* ************************************************************************ *)
diff --git a/src/kernel_services/cmdline_parameters/parameter_sig.mli b/src/kernel_services/cmdline_parameters/parameter_sig.mli
index bb827691793567e0bbe804f712a2fb7293d5a96b..a36076d68471974e040e4d0cebef792d3d185d74 100644
--- a/src/kernel_services/cmdline_parameters/parameter_sig.mli
+++ b/src/kernel_services/cmdline_parameters/parameter_sig.mli
@@ -321,6 +321,24 @@ module type Specific_dir = sig
 
 end
 
+type existence = Must_exist | Must_not_exist | Indifferent
+
+(** signature for normalized pathnames. *)
+module type Filepath = sig
+
+  exception No_file
+  (** raised by {!set} if no file exists and [existence] is [Must_exist]. *)
+
+  exception File_exists
+  (** raised by {!set} if some file exists and [existence] is
+      [Must_nos_exist]. *)
+
+  val existence: existence
+
+  include S with type t = Filepath.Normalized.t
+
+end
+
 (* ************************************************************************** *)
 (** {3 Collections} *)
 (* ************************************************************************** *)
@@ -515,6 +533,13 @@ module type Builder = sig
   (** @plugin development guide *)
   module Empty_string(X: Input_with_arg): String
 
+  module Fc_Filepath = Filepath
+
+  module Filepath(X: sig
+      include Input_with_arg
+      val existence: existence
+    end): Filepath
+
   exception Cannot_build of string
   module Make_set
     (E:
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 10241320736c4495275430db1a8a6ac2bbecc563..f686cd7684e27896afc96eae7409215a3f6d11be 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -445,6 +445,14 @@ module Parameter = struct
         let modname = "String"
       end)
 
+  module Filepath =
+    Common
+      (struct
+        type t = Datatype.Filepath.t
+        let ty = Datatype.Filepath.ty
+        let modname = "Filepath"
+      end)
+
   module StringSet = struct
     include Common
         (struct include Datatype.String.Set let modname = "StringSet" end)
diff --git a/src/kernel_services/plugin_entry_points/dynamic.mli b/src/kernel_services/plugin_entry_points/dynamic.mli
index c837a15601e045eb08dfe2a936ba8c4960687689..3650174dc2a424590dc3ba3473e6db44c1abc3be 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.mli
+++ b/src/kernel_services/plugin_entry_points/dynamic.mli
@@ -118,6 +118,9 @@ module Parameter : sig
   (** String parameters. *)
   module String : Common with type t = string
 
+  (** Filepath parameters. *)
+  module Filepath : Common with type t = Datatype.Filepath.t
+
   (** Set of string parameters. *)
   module StringSet : sig
     include Common with type t = Datatype.String.Set.t
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 41dcb5d8d089e8d56b26ceba6a29e28d14e31de2..3bcff739e6a5064f21a7fd18923c3992c43c6ce3 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -716,10 +716,11 @@ let () = Parameter_customize.set_cmdline_stage Cmdline.Loading
    reset *) 
 (*let () = Parameter_customize.do_not_projectify ()*)
 module LoadState =
-  P.Empty_string
+  P.Filepath
     (struct
        let option_name = "-load"
        let arg_name = "filename"
+       let existence = Parameter_sig.Must_exist
        let help = "load a previously-saved session from file <filename>"
      end)
 
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index 7976e6c86673f65f73788c64e6a77b384b0a0fed..0b43666bb0891fda4c20fae462daa956571e9dec 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -299,7 +299,7 @@ module BigIntsHex: Parameter_sig.Int
 module SaveState: Parameter_sig.String
   (** Behavior of option "-save" *)
 
-module LoadState: Parameter_sig.String
+module LoadState: Parameter_sig.Filepath
   (** Behavior of option "-load" *)
 
 module LoadModule: Parameter_sig.String_list
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index f24bdbcfb2680fd819c456b99b0c6d7ca87c8dd9..01d5831cbe50b7cc0048d60f594a888d4a58ad32 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -534,7 +534,7 @@ struct
 
     let pp_source fmt = function
       | None -> ()
-      | Some src -> Format.fprintf fmt "%a:" Filepath.pp_pos src
+      | Some src -> Format.fprintf fmt "%a:" Fc_Filepath.pp_pos src
   end
 
   (* Output must be synchronized with functions [prefix_*] in module Log. *)
diff --git a/src/libraries/utils/filepath.ml b/src/libraries/utils/filepath.ml
index 0e774657a818b0b5f91cafba14f4b21197480427..eb86c85f6945e397d7e3b1af0e3959c71faa5500 100644
--- a/src/libraries/utils/filepath.ml
+++ b/src/libraries/utils/filepath.ml
@@ -224,6 +224,7 @@ module Normalized = struct
   let pretty fmt p = Format.fprintf fmt "%s" (pretty p)
   let pp_abs fmt p = Format.fprintf fmt "%s" p
   let unknown = normalize ""
+  let is_unknown fp = equal fp unknown
 end
 
 type position =
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 6ea46d821541a1de524e1baad38bbadcf6339b54..74eef31bbdbb8d6f2ff340258beffeef3539cd65 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -120,6 +120,9 @@ module Normalized: sig
 
   (** Unknown filepath, used as 'dummy' for [Datatype.Filepath]. *)
   val unknown: t
+
+  (** @since Frama-C+dev *)
+  val is_unknown: t -> bool
 end
 
 (** Describes a position in a source file.
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 877191a8d974c87bdc90c050a25ebcf2e32609da..1c7b3d303cc981c5a84a939d39327c9ae7f12276 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -984,7 +984,7 @@ let base_output () =
               | dir ->
                   make_output_dir dir ; dir in
       base_output := Some output;
-      Filepath.add_symbolic_dir "WPOUT" output ;
+      Fc_Filepath.add_symbolic_dir "WPOUT" output ;
       output
   | Some output -> output
 
@@ -1026,7 +1026,7 @@ let has_print_generated () = has_dkey cat_print_generated
 
 let print_generated ?header file =
   let header = match header with
-    | None -> Filepath.Normalized.to_pretty_string (Datatype.Filepath.of_string file)
+    | None -> Fc_Filepath.Normalized.to_pretty_string (Datatype.Filepath.of_string file)
     | Some head -> head in
   debug ~dkey:cat_print_generated "%S@\n%t@." header
     begin fun fmt ->