diff --git a/src/kernel_internals/runtime/special_hooks.ml b/src/kernel_internals/runtime/special_hooks.ml
index 5b21630d6ba2b12acb71c8225808b1d16d058161..ea0bc0bba1122acb9aecf4d823d43d5999c042fc 100644
--- a/src/kernel_internals/runtime/special_hooks.ml
+++ b/src/kernel_internals/runtime/special_hooks.ml
@@ -106,22 +106,23 @@ let () = Extlib.safe_at_exit time
(* Save Frama-c on disk if required *)
let save_binary error_extension =
let filename = Kernel.SaveState.get () in
- if filename <> "" then begin
+ if not (Filepath.Normalized.is_unknown filename) then begin
Kernel.SaveState.clear ();
let realname =
match error_extension with
| None -> filename
| Some err_ext ->
- let s = filename ^ err_ext in
+ let s = (filename:>string) ^ err_ext in
Kernel.warning
"attempting to save on non-zero exit code: \
modifying filename into `%s'." s;
- s
+ Filepath.Normalized.of_string s
in
try
Project.save_all realname
with Project.IOError s ->
- Kernel.error "problem while saving to file %s (%s)." realname s
+ Kernel.error "problem while saving to file %a (%s)."
+ Filepath.Normalized.pretty realname s
end
let () =
(* implement a refinement of the behavior described in BTS #1388:
@@ -140,11 +141,11 @@ let () =
let load_binary () =
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
+ Project.load_all filepath
with Project.IOError s ->
- Kernel.abort "problem while loading file %s (%s)" filename s
+ Kernel.abort "problem while loading file %a (%s)"
+ Filepath.Normalized.pretty filepath s
end
let () = Cmdline.run_after_loading_stage load_binary
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 34b768c639c58304f241386fab6ded359df90534..1590e44022fb7b4c9423c25c5137d9f268c5ea17 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -744,10 +744,12 @@ let saveload = add_group "Saving or Loading Data"
let () = Parameter_customize.set_group saveload
let () = Parameter_customize.do_not_projectify ()
module SaveState =
- P.Empty_string
+ P.Filepath
(struct
let option_name = "-save"
let arg_name = "filename"
+ let existence = Filepath.Indifferent
+ let file_kind = "Frama-C state"
let help = "at exit, save the session into file <filename>"
end)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index d887e0b363270a01a5e2eb2daf754cc9f4c54f95..d39ea5ecc84ccf582c169925714bb6f935de2049 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -309,7 +309,7 @@ module BigIntsHex: Parameter_sig.Int
(** {2 Save/Load} *)
(* ************************************************************************* *)
-module SaveState: Parameter_sig.String
+module SaveState: Parameter_sig.Filepath
(** Behavior of option "-save" *)
module LoadState: Parameter_sig.Filepath
diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml
index 0c436d88610e6560541d59e1fac57c53bd8e30d3..f416ee377f170503df31f9176f437ebbf2a321f5 100644
--- a/src/libraries/project/project.ml
+++ b/src/libraries/project/project.ml
@@ -520,7 +520,7 @@ let magic = 9 (* magic number *)
let save_projects selection projects filename =
if Cmdline.use_obj then begin
- let cout = open_out_bin filename in
+ let cout = open_out_bin (filename : Filepath.Normalized.t :> string) in
output_value cout Fc_config.version;
output_value cout magic;
output_value cout !Graph.Blocks.cpt_vertex;
@@ -541,30 +541,30 @@ let save_projects selection projects filename =
abort "saving a file is not supported in the 'no obj' mode"
let unjournalized_save selection project filename =
- guarded_feedback selection 2 "saving project %S into file %S"
- project.unique_name filename;
+ guarded_feedback selection 2 "saving project %S into file %a"
+ project.unique_name Filepath.Normalized.pretty filename;
save_projects selection (Q.singleton project) filename
let journalized_save =
let lbl = Datatype.optlabel_func in
Journal.register "Project.save"
(lbl "selection" dft_sel State_selection.ty
- (lbl "project" current ty (Datatype.func Datatype.string Datatype.unit)))
+ (lbl "project" current ty (Datatype.func Datatype.Filepath.ty Datatype.unit)))
unjournalized_save
let save ?(selection=State_selection.full) ?(project=current()) filename =
journalized_save selection project filename
let unjournalized_save_all selection filename =
- guarded_feedback selection 2 "saving the current session into file %S"
- filename;
+ guarded_feedback selection 2 "saving the current session into file %a"
+ Filepath.Normalized.pretty filename;
save_projects selection projects filename
let journalized_save_all =
let lbl = Datatype.optlabel_func in
Journal.register "Project.save_all"
(lbl "selection" dft_sel State_selection.ty
- (Datatype.func Datatype.string Datatype.unit))
+ (Datatype.func Datatype.Filepath.ty Datatype.unit))
unjournalized_save_all
let save_all ?(selection=State_selection.full) filename =
@@ -686,12 +686,13 @@ end
let load_projects ~project_under_copy selection ?name filename =
if Cmdline.use_obj then begin
- let cin = open_in_bin filename in
+ let cin = open_in_bin (filename : Filepath.Normalized.t :> string) in
let gen_read f cin =
try f cin with
| End_of_file ->
close_in cin;
- abort "unexpected end of file while loading '%s'" filename
+ abort "unexpected end of file while loading '%a'"
+ Filepath.Normalized.pretty filename
| Failure s -> close_in cin; raise (IOError s)
in
let read = gen_read input_value in
@@ -745,8 +746,8 @@ let load_projects ~project_under_copy selection ?name filename =
abort "loading a file is not supported in the 'no obj' mode"
let unjournalized_load ~project_under_copy selection name filename =
- guarded_feedback selection 2 "loading the project saved in file %S"
- filename;
+ guarded_feedback selection 2 "loading the project saved in file %a"
+ Filepath.Normalized.pretty filename;
match load_projects ~project_under_copy selection ?name filename with
| [ p ] -> p
| [] | _ :: _ :: _ -> assert false
@@ -756,7 +757,7 @@ let journalized_load =
Journal.register "Project.load"
(lbl "selection" dft_sel State_selection.ty
(lbl "name" (fun () -> None)
- (Datatype.option Datatype.string) (Datatype.func Datatype.string ty)))
+ (Datatype.option Datatype.string) (Datatype.func Datatype.Filepath.ty ty)))
(unjournalized_load ~project_under_copy:None)
let load ?(selection=State_selection.full) ?name filename =
@@ -764,7 +765,8 @@ let load ?(selection=State_selection.full) ?name filename =
let unjournalized_load_all selection filename =
remove_all ();
- guarded_feedback selection 2 "loading the session saved in file %S" filename;
+ guarded_feedback selection 2 "loading the session saved in file %a"
+ Filepath.Normalized.pretty filename;
try
ignore (load_projects ~project_under_copy:None selection filename)
with IOError _ as e ->
@@ -775,7 +777,7 @@ let journalized_load_all =
let lbl = Datatype.optlabel_func in
Journal.register "Project.load_all"
(lbl "selection" dft_sel State_selection.ty
- (Datatype.func Datatype.string Datatype.unit))
+ (Datatype.func Datatype.Filepath.ty Datatype.unit))
unjournalized_load_all
let load_all ?(selection=State_selection.full) filename =
@@ -789,8 +791,9 @@ let unjournalized_create_by_copy selection src last name =
guarded_feedback selection 2 "creating project %S by copying project %S"
name (src.unique_name);
let filename =
- try Extlib.temp_file_cleanup_at_exit "frama_c_create_by_copy" ".sav"
- with Extlib.Temp_file_error s -> abort "cannot create temporary file: %s" s
+ Filepath.Normalized.of_string (
+ try Extlib.temp_file_cleanup_at_exit "frama_c_create_by_copy" ".sav"
+ with Extlib.Temp_file_error s -> abort "cannot create temporary file: %s" s)
in
save ~selection ~project:src filename;
try
@@ -798,12 +801,12 @@ let unjournalized_create_by_copy selection src last name =
unjournalized_load
~project_under_copy:(Some src) selection (Some name) filename
in
- Extlib.safe_remove filename;
+ Extlib.safe_remove (filename:>string);
if last then last_created_by_copy_ref := Some prj;
Create_by_copy_hook.apply (src, prj);
prj
with e ->
- Extlib.safe_remove filename;
+ Extlib.safe_remove (filename:>string);
raise e
let journalized_create_by_copy =
@@ -826,9 +829,9 @@ let create_by_copy
module Undo = struct
let short_filename = "frama_c_undo_restore"
- let filename = ref ""
+ let filename = ref Filepath.Normalized.unknown
- let clear_breakpoint () = Extlib.safe_remove !filename
+ let clear_breakpoint () = Extlib.safe_remove (!filename:>string)
let restore () =
if Cmdline.use_obj then begin
@@ -844,7 +847,7 @@ module Undo = struct
let breakpoint () =
if Cmdline.use_obj then begin
clear_breakpoint ();
- filename :=
+ filename := Filepath.Normalized.of_string
(try Extlib.temp_file_cleanup_at_exit short_filename ".sav"
with Extlib.Temp_file_error s ->
abort "cannot create temporary file: %s" s);
diff --git a/src/libraries/project/project.mli b/src/libraries/project/project.mli
index 14979ee597d10370a0a0ff9780ba52431f926bf2..09f56a7279cd85f318f2243810ba29721f33baa6 100644
--- a/src/libraries/project/project.mli
+++ b/src/libraries/project/project.mli
@@ -209,14 +209,14 @@ val register_before_remove_hook: (t -> unit) -> unit
exception IOError of string
-val save: ?selection:State_selection.t -> ?project:t -> string -> unit
+val save: ?selection:State_selection.t -> ?project:t -> Filepath.Normalized.t -> unit
(** Save a given project in a file. Default project is [current ()].
@raise IOError if the project cannot be saved.
@modify Carbon-20101201 replace the optional arguments [only] and
[except] by a single one [selection].
@plugin development guide *)
-val load: ?selection:State_selection.t -> ?name:string -> string -> t
+val load: ?selection:State_selection.t -> ?name:string -> Filepath.Normalized.t -> t
(** Load a file into a new project given by its name.
More precisely, [load only except name file]:
{ol
@@ -232,13 +232,13 @@ val load: ?selection:State_selection.t -> ?name:string -> string -> t
[except] by a single one [selection].
@plugin development guide *)
-val save_all: ?selection:State_selection.t -> string -> unit
+val save_all: ?selection:State_selection.t -> Filepath.Normalized.t -> unit
(** Save all the projects in a file.
@modify Carbon-20101201 replace the optional arguments [only] and
[except] by a single one [selection].
@raise IOError a project cannot be saved. *)
-val load_all: ?selection:State_selection.t -> string -> unit
+val load_all: ?selection:State_selection.t -> Filepath.Normalized.t -> unit
(** First remove all the existing project, then load all the projects from a
file. For each project to load, the specification is the same than
{!Project.load}. Furthermore, after loading, all the hooks registered by
diff --git a/src/plugins/gui/file_manager.ml b/src/plugins/gui/file_manager.ml
index 6444790e3374ae1c51acce3e624a6d815d3818ee..26e2c27b8334c93916cb4a832d51d059c57b8fe2 100644
--- a/src/plugins/gui/file_manager.ml
+++ b/src/plugins/gui/file_manager.ml
@@ -33,7 +33,7 @@ let add_files (host_window: Design.main_window_extension_points) =
host_window#reset ()
end)
-let filename: string option ref = ref None
+let filename: Filepath.Normalized.t option ref = ref None
(* [None] for opening the 'save as' dialog box;
[Some f] for saving in file [f] *)
@@ -94,7 +94,7 @@ let save_file_as (host_window: Design.main_window_extension_points) =
| `SAVE ->
Extlib.may
(save_in host_window (dialog :> GWindow.window_skel))
- dialog#filename
+ (Extlib.opt_map Filepath.Normalized.of_string dialog#filename)
| `DELETE_EVENT | `CANCEL -> ());
dialog#destroy ()
@@ -102,7 +102,7 @@ let save_file (host_window: Design.main_window_extension_points) =
match !filename with
| None -> save_file_as host_window
| Some f ->
- save_in host_window (host_window#main_window :> GWindow.window_skel) f
+ save_in host_window (host_window#main_window :> GWindow.window_skel) f
(** Load a project file *)
let load_file (host_window: Design.main_window_extension_points) =
@@ -118,7 +118,7 @@ let load_file (host_window: Design.main_window_extension_points) =
begin match dialog#filename with
| None -> ()
| Some f ->
- Project.load_all f
+ Project.load_all (Filepath.Normalized.of_string f)
end
| `DELETE_EVENT | `CANCEL -> ());
dialog#destroy ()
diff --git a/src/plugins/gui/project_manager.ml b/src/plugins/gui/project_manager.ml
index 07bd71c0e447c9bc4996292e1300df302b8e1001..27bb43daed33d3205ac8c3fe78cf4771221bdae2 100644
--- a/src/plugins/gui/project_manager.ml
+++ b/src/plugins/gui/project_manager.ml
@@ -76,7 +76,7 @@ let delete_project project =
end
module Filenames = Hashtbl.Make(Project)
-let filenames : string Filenames.t = Filenames.create 7
+let filenames : Filepath.Normalized.t Filenames.t = Filenames.create 7
let save_in
(host_window: Design.main_window_extension_points) parent project name =
@@ -102,7 +102,7 @@ let save_project_as (main_ui: Design.main_window_extension_points) project =
| `SAVE ->
Extlib.may
(save_in main_ui (dialog :> GWindow.window_skel) project)
- dialog#filename
+ (Extlib.opt_map Filepath.Normalized.of_string dialog#filename)
| `DELETE_EVENT | `CANCEL -> ());
dialog#destroy ()
@@ -130,7 +130,7 @@ let load_project (host_window: Design.main_window_extension_points) =
begin match dialog#filename with
| None -> ()
| Some f ->
- (try ignore (Project.load f)
+ (try ignore (Project.load (Filepath.Normalized.of_string f))
with Project.IOError s | Failure s ->
host_window#error
~reset:true ~parent:(dialog:>GWindow.window_skel)
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
index 67ec006f68be6abff406e2b5ca6ed9700e9a7d06..132508b04be8825902dc73774c4278a0f19a42d0 100644
--- a/src/plugins/server/kernel_main.ml
+++ b/src/plugins/server/kernel_main.ml
@@ -69,7 +69,7 @@ let () =
()
in
let load _rq file =
- try Project.load_all file; None
+ try Project.load_all (Filepath.Normalized.of_string file); None
with Project.IOError err -> Some err
in
Request.register_sig signature load
diff --git a/tests/misc/save_comments.ml b/tests/misc/save_comments.ml
index d31f7249a68f6b69d8ac986c9df26a0135c022fa..c885ff86e080ca3d2461d86ee4501046281cefba 100644
--- a/tests/misc/save_comments.ml
+++ b/tests/misc/save_comments.ml
@@ -28,7 +28,10 @@ let run () =
File.pretty_ast ~fmt ();
Format.printf "Printing default project second time:@.";
File.pretty_ast ~fmt ();
- let file = Extlib.temp_file_cleanup_at_exit "save_comments_test" ".sav" in
+ let file =
+ Filepath.Normalized.of_string
+ (Extlib.temp_file_cleanup_at_exit "save_comments_test" ".sav")
+ in
let name = "saved_project" in
find_comment ();
Project.save file;
diff --git a/tests/saveload/load_one.ml b/tests/saveload/load_one.ml
index 40864219da9835c8b0ac9da8d505c7662a3f79fc..c59e9cd3b7874dde5250c1f4d9a0e2f095ec327a 100644
--- a/tests/saveload/load_one.ml
+++ b/tests/saveload/load_one.ml
@@ -4,10 +4,11 @@ let main () =
let sparecode () =
Sparecode.Register.get ~select_annot:false ~select_slice_pragma:false
in
+ let fp = Filepath.Normalized.of_string "tests/saveload/result/load_one.sav" in
let p = sparecode () in
- Project.save "tests/saveload/result/load_one.sav";
+ Project.save fp;
Project.remove ~project:p ();
- let p = Project.load "tests/saveload/result/load_one.sav" in
+ let p = Project.load fp in
Project.on p (fun () -> !Db.Value.compute (); ignore (sparecode ())) ()
let () = Db.Main.extend main
diff --git a/tests/saveload/multi_project.ml b/tests/saveload/multi_project.ml
index 591674248cfc950290f9ffce13d3325b6fc3dfa3..4a7bd87831f8f3dff90580f39dff13bb9b039ad3 100644
--- a/tests/saveload/multi_project.ml
+++ b/tests/saveload/multi_project.ml
@@ -7,12 +7,13 @@ let check name test =
let main () =
ignore (Project.create_by_copy ~last:false "foo");
ignore (Project.create "foobar");
- Project.save_all "foo.sav";
+ let fp = Filepath.Normalized.of_string "foo.sav" in
+ Project.save_all fp;
check "foo" (<>);
check "foobar" (=);
check "default" (<>);
Kernel.Files.set [];
- Project.load_all "foo.sav";
+ Project.load_all fp;
Extlib.safe_remove "foo.sav";
ignore (Project.create_by_copy ~last:false "bar");
assert