From 64dfb1e751b922c03ee7ca01fbf80272ded42d16 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 9 Oct 2023 15:06:59 +0200
Subject: [PATCH] use new Filepath functions in more places
---
src/kernel_internals/runtime/machdep.ml | 1 -
src/kernel_services/ast_queries/file.ml | 10 +--
.../ast_queries/json_compilation_database.ml | 18 ++--
.../plugin_entry_points/plugin.ml | 15 ++--
src/libraries/stdlib/extlib.ml | 2 +-
src/libraries/stdlib/extlib.mli | 5 +-
src/libraries/utils/command.ml | 30 +++----
src/libraries/utils/command.mli | 16 ++--
src/libraries/utils/filepath.mli | 3 +-
src/libraries/utils/json.mli | 4 +-
src/libraries/utils/json.mll | 10 +--
src/plugins/aorai/aorai_register.ml | 8 +-
src/plugins/api-generator/api_generator.ml | 11 +--
src/plugins/markdown-report/md_gen.ml | 2 +-
src/plugins/markdown-report/sarif_gen.ml | 4 +-
src/plugins/report/classify.ml | 4 +-
src/plugins/server/server_doc.ml | 3 +-
src/plugins/wp/Cache.ml | 36 ++++----
src/plugins/wp/ProofSession.ml | 54 ++++++------
src/plugins/wp/ProofSession.mli | 8 +-
src/plugins/wp/ProverTask.ml | 4 +-
src/plugins/wp/ProverTask.mli | 4 +-
src/plugins/wp/ProverWhy3.ml | 51 ++++++-----
src/plugins/wp/VC.mli | 1 -
src/plugins/wp/gui/GuiProver.ml | 4 +-
src/plugins/wp/register.ml | 17 ++--
src/plugins/wp/wpApi.ml | 2 +-
src/plugins/wp/wpReport.ml | 7 +-
src/plugins/wp/wp_parameters.ml | 88 +++++++++----------
src/plugins/wp/wp_parameters.mli | 6 +-
src/plugins/wp/wpo.ml | 2 +-
src/plugins/wp/wpo.mli | 6 +-
32 files changed, 218 insertions(+), 218 deletions(-)
diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml
index f7734b1c823..dd5fc51f669 100644
--- a/src/kernel_internals/runtime/machdep.ml
+++ b/src/kernel_internals/runtime/machdep.ml
@@ -345,7 +345,6 @@ let gen_all_defines fmt mach =
let generate_machdep_header mach =
let debug = Kernel.(is_debug_key_enabled dkey_pp) in
let temp = Extlib.temp_dir_cleanup_at_exit ~debug "__fc_machdep" in
- let temp = Filepath.Normalized.of_string temp in
let file = Filepath.Normalized.concat temp "__fc_machdep.h" in
let chan = open_out (file:>string) in
let fmt = Format.formatter_of_out_channel chan in
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index ec24f15d0b6..687b5071deb 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -480,9 +480,9 @@ let adjust_pwd fp cpp_command =
let dir =
match Json_compilation_database.get_dir fp with
| None -> cwd
- | Some d -> (d:>string)
+ | Some d -> d
in
- if cwd <> dir then Some dir, "cd " ^ dir ^ " && " ^ cpp_command
+ if cwd <> dir then Some dir, "cd " ^ (dir :> string) ^ " && " ^ cpp_command
else None, cpp_command
else None, cpp_command
@@ -567,7 +567,7 @@ let build_cpp_cmd = function
in
let workdir, cpp_command_with_chdir = adjust_pwd f cpp_command in
if workdir <> None then
- Parse_env.set_workdir ppf (Option.get workdir);
+ Parse_env.set_workdir ppf ((Option.get workdir) :> string);
Kernel.feedback ~dkey:Kernel.dkey_pp
"preprocessing with \"%s\""
cpp_command_with_chdir;
@@ -595,10 +595,10 @@ let abort_with_detailed_pp_message f cpp_command =
else ""
in
Kernel.abort
- "failed to run: %s\n(PWD: %s)@\n\
+ "failed to run: %s\n(PWD: %a)@\n\
%sSee chapter \"Preparing the Sources\" in the Frama-C user manual \
for more details."
- cpp_command (Filepath.pwd ()) possible_cause
+ cpp_command Filepath.Normalized.pretty (Filepath.pwd ()) possible_cause
let parse_cabs cpp_command = function
| NoCPP f ->
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ml b/src/kernel_services/ast_queries/json_compilation_database.ml
index 12d3a3e1115..f55e58ce24d 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ml
@@ -297,18 +297,18 @@ let parse_compilation_entry jcdb_dir r =
update_flags_verbosely path (dirpath, flags)
let compute_flags_from_file () =
- let database = (Kernel.JsonCompilationDatabase.get () :> string) in
+ let database = Kernel.JsonCompilationDatabase.get () in
let jcdb_dir, jcdb_path =
- if Sys.is_directory database then
- database, Filename.concat database "compile_commands.json"
- else Filename.dirname database, database
+ if Filepath.is_dir database then
+ database, Filepath.Normalized.concat database "compile_commands.json"
+ else Filepath.dirname database, database
in
Kernel.feedback ~dkey:Kernel.dkey_compilation_db
- "using compilation database: %s" jcdb_path;
+ "using compilation database: %a" Datatype.Filepath.pretty jcdb_path;
begin
try
let r_list =
- Yojson.Basic.from_file jcdb_path |> Yojson.Basic.Util.to_list
+ Yojson.Basic.from_file (jcdb_path :> string) |> Yojson.Basic.Util.to_list
in
let is_build_database =
try
@@ -318,13 +318,13 @@ let compute_flags_from_file () =
let parse_entry =
if is_build_database then parse_build_entry else parse_compilation_entry
in
- List.iter (parse_entry jcdb_dir) r_list;
+ List.iter (parse_entry (jcdb_dir :> string)) r_list;
with
| Sys_error msg
| Yojson.Json_error msg
| Yojson.Basic.Util.Type_error (msg, _) ->
- Kernel.abort "could not parse compilation database: %s@ %s"
- database msg
+ Kernel.abort "could not parse compilation database: %a@ %s"
+ Datatype.Filepath.pretty database msg
end;
Flags.mark_as_computed ()
diff --git a/src/kernel_services/plugin_entry_points/plugin.ml b/src/kernel_services/plugin_entry_points/plugin.ml
index 1e416c731f6..909fd31f8cf 100644
--- a/src/kernel_services/plugin_entry_points/plugin.ml
+++ b/src/kernel_services/plugin_entry_points/plugin.ml
@@ -21,7 +21,6 @@
(**************************************************************************)
module CamlString = String
-module FramacFilepath = Filepath
let empty_string = ""
@@ -318,13 +317,13 @@ struct
end)
let mk_dir d =
- let d' = FramacFilepath.Normalized.of_string d in
+ let d' = Fc_Filepath.Normalized.of_string d in
try
- Extlib.mkdir ~parents:true d 0o755;
- L.warning "creating %s directory `%a'" O.option_name FramacFilepath.Normalized.pretty d';
+ if Extlib.mkdir ~parents:true d' 0o755 then
+ L.warning "created %s directory `%a'" O.option_name Fc_Filepath.Normalized.pretty d';
d
with Unix.Unix_error _ ->
- L.abort "cannot create %s directory `%a'" O.option_name FramacFilepath.Normalized.pretty d'
+ L.abort "cannot create %s directory `%a'" O.option_name Fc_Filepath.Normalized.pretty d'
let set filepath = Dir_name.set filepath
let get () = Dir_name.get ()
@@ -362,7 +361,7 @@ struct
List.fold_left
(fun dummy d ->
let name = Datatype.Filepath.concat d s in
- if FramacFilepath.exists name
+ if Fc_Filepath.exists name
then raise (Found name)
else dummy)
None
@@ -404,7 +403,7 @@ struct
| `Create_path ->
begin
(try
- if not (Sys.is_directory (filepath :> string))
+ if not (Fc_Filepath.is_dir filepath)
then
(* [filepath] already exists, and it is a file. *)
L.abort
@@ -424,7 +423,7 @@ struct
let filepath = Datatype.Filepath.concat base_dir s_basename in
match mode with
| `Must_exist ->
- if FramacFilepath.exists filepath
+ if Fc_Filepath.exists filepath
then filepath
else L.abort "there is no file %s in %s directories" (filepath :> string) O.option_name
| `Normalize_only ->
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 2be6085f39d..39b641d9fe1 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -316,7 +316,7 @@ let temp_dir_cleanup_at_exit ?(debug=false) base =
else
safe_remove_dir dir
end ;
- dir
+ Filepath.Normalized.of_string dir
with Unix.Unix_error(err,_,_) ->
if limit < 0 then
raise (Temp_file_error (Unix.error_message err))
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index e4c49118dd5..87fd1e03276 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -292,8 +292,9 @@ val temp_file_cleanup_at_exit: ?debug:bool -> string -> string -> string
@raise Temp_file_error if the temp file cannot be created.
*)
-val temp_dir_cleanup_at_exit: ?debug:bool -> string -> string
-(** @raise Temp_file_error if the temp dir cannot be created. *)
+val temp_dir_cleanup_at_exit: ?debug:bool -> string -> Filepath.Normalized.t
+(** @raise Temp_file_error if the temp dir cannot be created.
+ @since Frama-C+dev modify return type *)
val safe_remove: string -> unit
(** Tries to delete a file and never fails. *)
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index 1b33532dc3f..c0ef15d6202 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -27,10 +27,8 @@ let safe_close_in inc = try close_in inc with Sys_error _ -> ()
(* --- File Utilities --- *)
(* -------------------------------------------------------------------------- *)
-let filename parent child = Filename.concat parent child
-
-let pp_to_file f pp =
- let cout = open_out f in
+let pp_to_file (f: Filepath.Normalized.t) pp =
+ let cout = open_out (f :> string) in
let fout = Format.formatter_of_out_channel cout in
try
pp fout ;
@@ -41,8 +39,8 @@ let pp_to_file f pp =
safe_close_out cout ;
raise err
-let pp_from_file fmt file =
- let cin = open_in file in
+let pp_from_file fmt (file: Filepath.Normalized.t) =
+ let cin = open_in (file :> string) in
try
while true do
Db.yield () ;
@@ -65,13 +63,13 @@ let rec bincopy buffer cin cout =
else
( flush cout )
-let on_inc file job =
- let inc = open_in file in
+let on_inc (file: Filepath.Normalized.t) job =
+ let inc = open_in (file :> string) in
let finally () = safe_close_in inc in
Fun.protect ~finally (fun () -> job inc)
-let on_out file job =
- let out = open_out file in
+let on_out (file: Filepath.Normalized.t) job =
+ let out = open_out (file :> string) in
let finally () = safe_close_out out in
Fun.protect ~finally (fun () -> job out)
@@ -79,8 +77,8 @@ let copy src tgt =
on_inc src
(fun inc -> on_out tgt (fun out -> bincopy (Bytes.create 2048) inc out))
-let read_file file job =
- let inc = open_in file in
+let read_file (file: Filepath.Normalized.t) job =
+ let inc = open_in (file :> string) in
let finally () = safe_close_in inc in
Fun.protect ~finally (fun () -> job inc)
@@ -94,8 +92,8 @@ let read_lines file job =
with End_of_file -> ())
let write_file file job =
- assert (file <> "");
- let out = open_out file in
+ assert (not (Filepath.Normalized.is_empty file));
+ let out = open_out (file :> string) in
let finally () = flush out; safe_close_out out in
Fun.protect ~finally (fun () -> job out)
@@ -227,8 +225,8 @@ let command_generic ~async ?stdout ?stderr cmd args =
else
begin
let result = Result status in
- flush stdout outf ;
- flush stderr errf ;
+ flush stdout (Filepath.Normalized.of_string outf) ;
+ flush stderr (Filepath.Normalized.of_string errf) ;
delete () ;
deleted () ;
killed () ;
diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli
index 48293d2ae71..bdf1f030c40 100644
--- a/src/libraries/utils/command.mli
+++ b/src/libraries/utils/command.mli
@@ -26,14 +26,12 @@
(** {2 File Utilities} *)
(* ************************************************************************* *)
-val filename : string -> string -> string
-
-val pp_to_file : string -> (Format.formatter -> unit) -> unit
+val pp_to_file : Filepath.Normalized.t -> (Format.formatter -> unit) -> unit
(** [pp_to_file file pp] runs [pp] on a formatter that writes into [file].
The formatter is always properly flushed and closed on return.
Exceptions in [pp] are re-raised after closing. *)
-val pp_from_file : Format.formatter -> string -> unit
+val pp_from_file : Format.formatter -> Filepath.Normalized.t -> unit
(** [pp_from_file fmt file] dumps the content of [file] into the [fmt].
Exceptions in [pp] are re-raised after closing. *)
@@ -44,19 +42,19 @@ val bincopy : bytes -> in_channel -> out_channel -> unit
Recommended size is [2048].
*)
-val copy : string -> string -> unit
+val copy : Filepath.Normalized.t -> Filepath.Normalized.t -> unit
(** [copy source target] copies source file to target file using [bincopy]. *)
-val read_file : string -> (in_channel -> 'a) -> 'a
+val read_file : Filepath.Normalized.t -> (in_channel -> 'a) -> 'a
(** Properly close the channel and re-raise exceptions *)
-val read_lines : string -> (string -> unit) -> unit
+val read_lines : Filepath.Normalized.t -> (string -> unit) -> unit
(** Iter over all text lines in the file *)
-val write_file : string -> (out_channel -> 'a) -> 'a
+val write_file : Filepath.Normalized.t -> (out_channel -> 'a) -> 'a
(** Properly close the channel and re-raise exceptions *)
-val print_file : string -> (Format.formatter -> 'a) -> 'a
+val print_file : Filepath.Normalized.t -> (Format.formatter -> 'a) -> 'a
(** Properly flush and close the channel and re-raise exceptions *)
(* ************************************************************************* *)
diff --git a/src/libraries/utils/filepath.mli b/src/libraries/utils/filepath.mli
index 0813cca428b..c39e4cc408d 100644
--- a/src/libraries/utils/filepath.mli
+++ b/src/libraries/utils/filepath.mli
@@ -221,8 +221,9 @@ val pp_pos : Format.formatter -> position -> unit
symbolic links in directory names.
@since 25.0-Manganese
+ @before Frama-C+dev return type was string instead of Normalized.t.
*)
-val pwd : unit -> string
+val pwd : unit -> Normalized.t
(** Equivalent to [Sys.file_exists].
@since Frama-C+dev
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index 17da5974728..cbf326061cc 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -79,7 +79,7 @@ val load_channel : ?file:string -> in_channel -> t
val load_string : string -> t
(** Parses the Json in the string. *)
-val load_file : string -> t
+val load_file : Filepath.Normalized.t -> t
(** May also raise system exception. *)
(** {2 Printers} *)
@@ -90,7 +90,7 @@ val save_string : ?pretty:bool -> t -> string
val save_buffer : ?pretty:bool -> Buffer.t -> t -> unit
val save_channel : ?pretty:bool -> out_channel -> t -> unit
val save_formatter : ?pretty:bool -> Format.formatter -> t -> unit
-val save_file : ?pretty:bool -> string -> t -> unit
+val save_file : ?pretty:bool -> Filepath.Normalized.t -> t -> unit
(** {2 Accessors} *)
diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll
index 2017df4f369..82165703b20 100644
--- a/src/libraries/utils/json.mll
+++ b/src/libraries/utils/json.mll
@@ -153,10 +153,10 @@ let load_channel ?file inc =
end ;
load_lexbuf lexbuf
-let load_file file =
- let inc = open_in file in
+let load_file (file : Filepath.Normalized.t) =
+ let inc = open_in (file :> string) in
try
- let content = load_channel ~file inc in
+ let content = load_channel ~file:(file :> string) inc in
close_in inc ; content
with e ->
close_in inc ; raise e
@@ -230,8 +230,8 @@ let save_channel ?(pretty=true) out v =
let save_formatter ?(pretty=true) fmt v =
if pretty then pp fmt v else pp_dump fmt v
-let save_file ?(pretty=true) file v =
- let out = open_out file in
+let save_file ?(pretty=true) (file : Filepath.Normalized.t) v =
+ let out = open_out (file :> string) in
try
save_channel ~pretty out v ;
close_out out
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index 9f0069d251a..67739a849f8 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -63,14 +63,16 @@ let init_file_names () =
let pre = Filename.remove_extension name in
let pre = match opt_suf with None -> pre | Some s -> pre ^ s in
let rec fn p s n =
- if not (Sys.file_exists (p^(string_of_int n)^s)) then (p^(string_of_int n)^s)
+ let fp = Filepath.Normalized.of_string (p ^ (string_of_int n) ^ s) in
+ if not (Filepath.exists fp) then fp
else fn p s (n+1)
in
let name =
- if not (Sys.file_exists (pre^suf)) then pre^suf
+ let fp = Filepath.Normalized.of_string (pre^suf) in
+ if not (Filepath.exists fp) then fp
else fn pre suf 0
in
- Filepath.Normalized.of_string name
+ name
in
if Aorai_option.Ya.is_empty () then
Aorai_option.abort "empty Ya file name";
diff --git a/src/plugins/api-generator/api_generator.ml b/src/plugins/api-generator/api_generator.ml
index b35d7410118..c6a92a684d1 100644
--- a/src/plugins/api-generator/api_generator.ml
+++ b/src/plugins/api-generator/api_generator.ml
@@ -37,11 +37,13 @@ module TSC = Self.Action
let help = "Generate TypeScript API"
end)
-module OUT = Self.String
+module OUT = Self.Filepath
(struct
let option_name = "-server-tsc-out"
let arg_name = "path"
let default = "src"
+ let file_kind = "output-dir"
+ let existence = Filepath.Indifferent
let help = Printf.sprintf "Output directory (default is '%s')" default
end)
@@ -571,10 +573,9 @@ let generate () =
let path = pkg_path ~plugin:pkg.p_plugin ~package:pkg.p_package in
Self.feedback "Package %s" path ;
let out = OUT.get () in
- let file = Printf.sprintf "%s/%s/index.ts" out path in
- let dir = Filename.dirname file in
- if not (Sys.file_exists dir && Sys.is_directory dir) then
- Extlib.mkdir ~parents:true dir 0o755 ;
+ let dir = Filepath.Normalized.concat out path in
+ let file = Filepath.Normalized.concat dir "index.ts" in
+ ignore (Extlib.mkdir ~parents:true dir 0o755) ;
Command.print_file file (makePackage pkg path) ;
end
end
diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml
index 1e94eaa7fa1..50a13f227f5 100644
--- a/src/plugins/markdown-report/md_gen.ml
+++ b/src/plugins/markdown-report/md_gen.ml
@@ -618,7 +618,7 @@ let gen_report ~draft:is_draft () =
Mdr_params.Output.option_name
else
try
- Command.print_file (file:>string)
+ Command.print_file file
(fun fmt ->
Markdown.pp_pandoc fmt doc;
Format.pp_print_newline fmt ()) ;
diff --git a/src/plugins/markdown-report/sarif_gen.ml b/src/plugins/markdown-report/sarif_gen.ml
index 2ec752a73b5..a06849d8709 100644
--- a/src/plugins/markdown-report/sarif_gen.ml
+++ b/src/plugins/markdown-report/sarif_gen.ml
@@ -251,7 +251,7 @@ let gen_run remarks =
(key, (dir :> string))
) (Filepath.all_symbolic_dirs ())
in
- let pwd = Filepath.pwd () in
+ let pwd = (Filepath.pwd () :> string) in
let uriBases = ("PWD", pwd) :: symbolicDirs in
let uriBasesJson =
List.fold_left (fun acc (name, dir) ->
@@ -278,7 +278,7 @@ let generate () =
if not (Mdr_params.Output.is_empty ()) then
let file = Mdr_params.Output.get () in
try
- Command.write_file (file:>string)
+ Command.write_file file
(fun out ->
Yojson.Safe.pretty_to_channel ~std:true out json;
output_char out '\n') ;
diff --git a/src/plugins/report/classify.ml b/src/plugins/report/classify.ml
index 0d4e2538323..5e7ef8e3bc1 100644
--- a/src/plugins/report/classify.ml
+++ b/src/plugins/report/classify.ml
@@ -175,7 +175,7 @@ let configure file =
let path = Datatype.Filepath.of_string file in
R.feedback "Loading '%a'" Datatype.Filepath.pretty path;
try
- match Json.load_file file with
+ match Json.load_file path with
| `List values -> List.iter add_rule values
| _ -> failwith "Array expected"
with
@@ -521,7 +521,7 @@ let report_dump fmt =
let report_output file =
R.feedback "Output %a@." Filepath.Normalized.pretty file;
- Command.print_file (file:>string) report_dump
+ Command.print_file file report_dump
let report_number name nb opt =
if nb > 0 then R.feedback "%s%4d" name nb ;
diff --git a/src/plugins/server/server_doc.ml b/src/plugins/server/server_doc.ml
index 1169ad75c0d..6c2f0144037 100644
--- a/src/plugins/server/server_doc.ml
+++ b/src/plugins/server/server_doc.ml
@@ -322,8 +322,7 @@ let metadata page : json =
let pp_one_page ~root ~page ~title body =
let full_path = Filepath.Normalized.concat root page in
- let dir = Filename.dirname (full_path:>string) in
- if not (Sys.file_exists dir) then Extlib.mkdir ~parents:true dir 0o755;
+ ignore (Extlib.mkdir ~parents:true (Filepath.dirname full_path) 0o755);
try
let chan = open_out (full_path:>string) in
let fmt = Format.formatter_of_out_channel chan in
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 2751c487e98..5e7988978a2 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -69,14 +69,14 @@ let is_session_dir path =
let get_usable_dir ?(make=false) () =
let path = CACHEDIR.get () in
let parents = is_session_dir path in
- let path = (path :> string) in
- if not (Sys.file_exists path) && make then
- Extlib.mkdir ~parents path 0o755 ;
- if not (Sys.is_directory path) then begin
+ if not (Filepath.exists path) && make then
+ ignore (Extlib.mkdir ~parents path 0o755);
+ if not (Filepath.is_dir path) then begin
Wp_parameters.warning ~current:false ~once:true
- "Cache path is not a directory" ;
+ "Cache path %a is not a directory"
+ Filepath.Normalized.pretty path;
raise Not_found
- end ;
+ end;
path
let has_dir () =
@@ -173,19 +173,24 @@ let promote ?timeout ?steplimit (res : VCS.result) =
else (* can be run a longer time or widely *)
VCS.no_result
+let file_from_hash hash =
+ let dir = get_usable_dir ~make:true () in
+ let file = Printf.sprintf "%s/%s.json" (dir:>string) hash in
+ file
+
let get_cache_result ~mode hash =
match mode with
| NoCache | Rebuild -> VCS.no_result
| Update | Cleanup | Replay | Offline ->
try
- let dir = get_usable_dir ~make:true () in
let hash = Lazy.force hash in
- let file = Printf.sprintf "%s/%s.json" dir hash in
- if not (Sys.file_exists file) then VCS.no_result
+ let file = file_from_hash hash in
+ let path = Filepath.Normalized.of_string file in
+ if not (Filepath.exists path) then VCS.no_result
else
try
mark_cache ~mode hash ;
- Json.load_file file |> ProofScript.result_of_json
+ Json.load_file path |> ProofScript.result_of_json
with err ->
Wp_parameters.warning ~current:false ~once:true
"invalid cache entry (%s)" (Printexc.to_string err) ;
@@ -198,11 +203,11 @@ let set_cache_result ~mode hash prover result =
| Rebuild | Update | Cleanup ->
let hash = Lazy.force hash in
try
- let dir = get_usable_dir ~make:true () in
- let file = Printf.sprintf "%s/%s.json" dir hash in
+ let file = file_from_hash hash in
+ let path = Filepath.Normalized.of_string file in
mark_cache ~mode hash ;
ProofScript.json_of_result (VCS.Why3 prover) result
- |> Json.save_file file
+ |> Json.save_file path
with err ->
Wp_parameters.warning ~current:false ~once:true
"can not update cache (%s)" (Printexc.to_string err)
@@ -210,8 +215,7 @@ let set_cache_result ~mode hash prover result =
let clear_result ~digest prover goal =
try
let hash = digest prover goal in
- let dir = get_usable_dir ~make:true () in
- let file = Printf.sprintf "%s/%s.json" dir hash in
+ let file = file_from_hash hash in
Extlib.safe_remove file
with err ->
Wp_parameters.warning ~current:false ~once:true
@@ -221,7 +225,7 @@ let cleanup_cache () =
let mode = get_mode () in
if mode = Cleanup && (!hits > 0 || !miss > 0) then
try
- let dir = get_usable_dir () in
+ let dir = (get_usable_dir ():>string) in
if is_global_cache () then
Wp_parameters.warning ~current:false ~once:true
"Cleanup mode deactivated with global cache."
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 678d280f552..e94af595500 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/src/plugins/wp/ProofSession.ml
@@ -24,8 +24,8 @@ open Wpo
type script =
| NoScript
- | Script of string
- | Deprecated of string
+ | Script of Filepath.Normalized.t
+ | Deprecated of Filepath.Normalized.t
type mode =
| Batch
@@ -79,10 +79,10 @@ let saving_mode () =
| Update | Init -> true
| Batch | Dry -> false
-let files : (string,script) Hashtbl.t = Hashtbl.create 32
+let files : (Filepath.Normalized.t,script) Hashtbl.t = Hashtbl.create 32
-let jsonfile (dir:Datatype.Filepath.t) =
- Format.sprintf "%s/%s.json" (dir :> string)
+let jsonfile (dir:Datatype.Filepath.t) name =
+ Filepath.Normalized.concat dir (name ^ ".json")
let get_script_dir ~force =
Wp_parameters.get_session_dir ~force "script"
@@ -105,16 +105,16 @@ let get wpo =
try Hashtbl.find files f
with Not_found ->
let script =
- if Sys.file_exists f then Script f else
+ if Filepath.exists f then Script f else
try
- let f' = List.find Sys.file_exists (legacies wpo) in
+ let f' = List.find Filepath.exists (legacies wpo) in
Wp_parameters.warning ~current:false
"Deprecated script for '%s'" wpo.po_sid ;
Deprecated f'
with Not_found -> NoScript
in Hashtbl.add files f script ; script
-let pp_file fmt s = Filepath.Normalized.(pretty fmt (of_string s))
+let pp_file fmt s = Filepath.Normalized.(pretty fmt s)
let pp_script_for fmt wpo =
match get wpo with
@@ -129,21 +129,21 @@ let load wpo =
match get wpo with
| NoScript -> `Null
| Script f | Deprecated f ->
- if Sys.file_exists f then Json.load_file f else `Null
+ if Filepath.exists f then Json.load_file f else `Null
let remove wpo =
match get wpo with
| NoScript -> ()
| Script f ->
begin
- Extlib.safe_remove f ;
+ Extlib.safe_remove (f:>string) ;
Hashtbl.replace files f NoScript ;
end
| Deprecated f0 ->
begin
Wp_parameters.feedback
"Removed deprecated script for '%s'" wpo.po_sid ;
- Extlib.safe_remove f0 ;
+ Extlib.safe_remove (f0 :> string) ;
let f = filename ~force:false wpo in
Hashtbl.replace files f NoScript ;
end
@@ -171,7 +171,7 @@ let save ~stdout wpo js =
begin
Wp_parameters.feedback
"Upgraded script for '%s'" wpo.po_sid ;
- Extlib.safe_remove f0 ;
+ Extlib.safe_remove (f0 :> string) ;
let f = filename ~force:true wpo in
Json.save_file f js ;
Hashtbl.replace files f (Script f) ;
@@ -180,16 +180,15 @@ let save ~stdout wpo js =
let get_marks_dir ~force =
let scripts = Wp_parameters.get_session_dir ~force "script" in
let path = Datatype.Filepath.concat scripts ".marks" in
- if force then Wp_parameters.make_output_dir (path :> string) ;
+ if force then Wp_parameters.make_output_dir path ;
path
let remove_marks ~dry =
let marks = get_marks_dir ~force:false in
- let as_str = (marks :> string) in
- if Sys.file_exists as_str && Sys.is_directory as_str then
+ if Filepath.exists marks && Filepath.is_dir marks then
if dry
then Wp_parameters.feedback "[dry] remove marks"
- else Extlib.safe_remove_dir as_str
+ else Extlib.safe_remove_dir (marks :> string)
let reset_marks () =
remove_marks ~dry:false ;
@@ -197,35 +196,34 @@ let reset_marks () =
let mark goal =
let marks = get_marks_dir ~force:false in
- let as_str = (marks :> string) in
- if Sys.file_exists as_str && Sys.is_directory as_str then
+ if Filepath.exists marks && Filepath.is_dir marks then
let mark = Datatype.Filepath.concat marks (goal.po_sid ^ ".json") in
- if Sys.file_exists (mark :> string) then ()
+ if Filepath.exists mark then ()
else close_out @@ open_out (mark :> string)
module StringSet = Datatype.String.Set
let remove_unmarked_files ~dry =
- let dir = (get_script_dir ~force:false :> string) in
- if Sys.file_exists dir && Sys.is_directory dir then
- let marks = (get_marks_dir ~force:false :> string) in
- if Sys.file_exists marks && Sys.is_directory marks then
+ let dir = get_script_dir ~force:false in
+ if Filepath.exists dir && Filepath.is_dir dir then
+ let marks = get_marks_dir ~force:false in
+ if Filepath.exists marks && Filepath.is_dir marks then
begin
let files =
Array.fold_left
- (fun s f -> StringSet.add f s) StringSet.empty (Sys.readdir dir)
+ (fun s f -> StringSet.add f s) StringSet.empty (Filepath.readdir dir)
in
let marks =
Array.fold_left
- (fun s f -> StringSet.add f s) StringSet.empty (Sys.readdir marks)
+ (fun s f -> StringSet.add f s) StringSet.empty (Filepath.readdir marks)
in
let orphans = StringSet.diff files marks in
let orphans = StringSet.remove ".marks" orphans in
let remove file =
- let path = dir ^ "/" ^ file in
+ let path = Filepath.Normalized.concat dir file in
if dry
- then Wp_parameters.feedback "[dry] rm %s" path
- else Sys.remove path
+ then Wp_parameters.feedback "[dry] rm %a" Filepath.Normalized.pretty path
+ else Filepath.remove path
in
StringSet.iter remove orphans ;
remove_marks ~dry
diff --git a/src/plugins/wp/ProofSession.mli b/src/plugins/wp/ProofSession.mli
index 833cfea1038..390c2b29ef4 100644
--- a/src/plugins/wp/ProofSession.mli
+++ b/src/plugins/wp/ProofSession.mli
@@ -22,8 +22,8 @@
type script =
| NoScript
- | Script of string
- | Deprecated of string
+ | Script of Filepath.Normalized.t
+ | Deprecated of Filepath.Normalized.t
type mode =
| Batch
@@ -37,7 +37,7 @@ val set_mode : mode -> unit
val scratch_mode : unit -> bool
val saving_mode : unit -> bool
-val pp_file : Format.formatter -> string -> unit
+val pp_file : Format.formatter -> Filepath.Normalized.t -> unit
val pp_script_for : Format.formatter -> Wpo.t -> unit
val get : Wpo.t -> script
@@ -46,7 +46,7 @@ val save : stdout:bool -> Wpo.t -> Json.t -> unit
val load : Wpo.t -> Json.t
val remove : Wpo.t -> unit
-val filename : force:bool -> Wpo.t -> string
+val filename : force:bool -> Wpo.t -> Filepath.Normalized.t
val mark : Wpo.t -> unit
val reset_marks : unit -> unit
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index 76808660184..fbf8f5b414d 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -114,7 +114,7 @@ let dump_buffer buffer = function
if n > 0 then
Command.write_file log (fun out -> Buffer.output_buffer out buffer)
else if Wp_parameters.has_out () then
- Extlib.safe_remove log
+ Extlib.safe_remove (log :> string)
let echo_buffer buffer =
let n = Buffer.length buffer in
@@ -133,7 +133,7 @@ let location file line = {
}
let pp_file ~message ~file =
- if Sys.file_exists file then
+ if Filepath.exists file then
Log.print_on_output
begin fun fmt ->
let bar = String.make 60 '-' in
diff --git a/src/plugins/wp/ProverTask.mli b/src/plugins/wp/ProverTask.mli
index a37c089fdbe..8ff7feaf7f4 100644
--- a/src/plugins/wp/ProverTask.mli
+++ b/src/plugins/wp/ProverTask.mli
@@ -33,7 +33,7 @@ class printer : Format.formatter -> string ->
method printf : 'a. ('a,Format.formatter,unit) format -> 'a
end
-val pp_file : message:string -> file:string -> unit
+val pp_file : message:string -> file:Filepath.Normalized.t -> unit
(** never fails *)
class type pattern =
@@ -81,7 +81,7 @@ class virtual command : string ->
method validate_time : (float -> unit) -> unit
method validate_pattern : ?logs:logs -> ?repeat:bool ->
Str.regexp -> (pattern -> unit) -> unit
- method run : ?echo:bool -> ?logout:string -> ?logerr:string ->
+ method run : ?echo:bool -> ?logout:Filepath.Normalized.t -> ?logerr:Filepath.Normalized.t ->
unit -> int Task.task
end
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index d0bf28e123f..603c45806c5 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -793,26 +793,29 @@ class visitor (ctx:context) c =
method on_library thy =
let copy_file source =
if not (Datatype.Filepath.equal
- (Datatype.Filepath.of_string (Filename.dirname source))
+ (Filepath.dirname source)
(Wp_parameters.Share.get_dir "."))
then
let tgtdir = WpContext.directory () in
- let why3src = Filename.basename source in
- let target = Printf.sprintf "%s/%s" (tgtdir :> string) why3src in
+ let why3src = Filepath.basename source in
+ let target = Filepath.Normalized.concat tgtdir (why3src :> string) in
Command.copy source target
in
let iter_file opt =
match Str.split_delim regexp_col opt with
| [file] ->
+ let path = Filepath.Normalized.of_string file in
let filenoext = filenoext file in
- copy_file file;
+ copy_file path;
self#add_import_file [filenoext]
(String.capitalize_ascii filenoext);
| [file;lib] ->
- copy_file file;
+ let path = Filepath.Normalized.of_string file in
+ copy_file path;
self#add_import_file [filenoext file] lib;
| [file;lib;name] ->
- copy_file file;
+ let path = Filepath.Normalized.of_string file in
+ copy_file path;
self#add_import_file_as [filenoext file] lib name;
| _ -> why3_failure
"[driver] incorrect why3.file %S for library '%s'"
@@ -1226,7 +1229,7 @@ let call_prover_task ~timeout ~steps ~config prover call =
(* --- Batch Prover --- *)
(* -------------------------------------------------------------------------- *)
-let digest_task wpo drv ?script prover task =
+let digest_task wpo drv ?(script : Filepath.Normalized.t option) prover task =
let file = Wpo.DISK.file_goal
~pid:wpo.Wpo.po_pid
~model:wpo.Wpo.po_model
@@ -1241,14 +1244,14 @@ let digest_task wpo drv ?script prover task =
let hash = Digest.file fscript |> Digest.to_hex in
Format.fprintf fmt "(* WP Script %s *)@\n" hash ;
open_in fscript
- ) script in
+ ) (script :> string option) in
let _ = Why3.Driver.print_task_prepared ?old drv fmt task in
Option.iter close_in old ;
end ;
- Digest.file file |> Digest.to_hex
+ Digest.file (file :> string) |> Digest.to_hex
end
-let run_batch pconf driver ~config ?script ~timeout ~steplimit ~memlimit
+let run_batch pconf driver ~config ?(script : Filepath.Normalized.t option) ~timeout ~steplimit ~memlimit
prover task =
let steps = match steplimit with Some 0 -> None | _ -> steplimit in
let limit =
@@ -1273,7 +1276,7 @@ let run_batch pconf driver ~config ?script ~timeout ~steplimit ~memlimit
let command = Why3.Whyconf.get_complete_command pconf ~with_steps in
Wp_parameters.debug ~dkey "Prover command %S" command ;
let inplace = if script <> None then Some true else None in
- let call = Why3.Driver.prove_task_prepared ?old:script ?inplace
+ let call = Why3.Driver.prove_task_prepared ?old:(script :> string option) ?inplace
~command ~limit ~config driver task in
call_prover_task ~config ~timeout ~steps prover call
@@ -1293,33 +1296,35 @@ let editor_command pconf =
let scriptfile ~force ~ext wpo =
let dir = Wp_parameters.get_session_dir ~force "interactive" in
- Format.sprintf "%s/%s%s" (dir :> string) wpo.Wpo.po_sid ext
+ let filenoext = Filepath.Normalized.concat dir wpo.Wpo.po_sid in
+ Filepath.Normalized.concat filenoext ext
let updatescript ~script driver task =
- let backup = script ^ ".bak" in
- Sys.rename script backup ;
- let old = open_in backup in
+ let backup = Filepath.Normalized.concat script ".bak" in
+ Filepath.rename script backup ;
+ let old = open_in (backup :> string) in
Command.pp_to_file script
(fun fmt ->
ignore @@ Why3.Driver.print_task_prepared ~old driver fmt task
);
close_in old ;
- let d_old = Digest.file backup in
- let d_new = Digest.file script in
- if String.equal d_new d_old then Extlib.safe_remove backup
+ let d_old = Digest.file (backup :> string) in
+ let d_new = Digest.file (script :> string) in
+ if String.equal d_new d_old then Extlib.safe_remove (backup :> string)
let editor ~script ~merge ~config pconf driver task =
Task.sync editor_mutex
begin fun () ->
- Wp_parameters.feedback ~ontty:`Transient "Editing %S..." script ;
+ Wp_parameters.feedback ~ontty:`Transient "Editing %a..."
+ Filepath.Normalized.pretty script ;
if merge then updatescript ~script driver task ;
let command = editor_command pconf in
Wp_parameters.debug ~dkey "Editor command %S" command ;
call_prover_task ~config ~timeout:None ~steps:None pconf.prover @@
- Why3.Call_provers.call_editor ~command ~config script
+ Why3.Call_provers.call_editor ~command ~config (script :> string)
end
-let compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task =
+let compile ~(script : Filepath.Normalized.t) ~timeout ~memlimit ~config wpo pconf driver prover task =
let digest = digest_task wpo driver ~script in
let runner = run_batch ~config pconf driver ~script ~memlimit in
Cache.get_result ~digest ~runner ~timeout ~steplimit:None prover task
@@ -1328,7 +1333,7 @@ let prepare ~mode wpo driver task =
let ext = Filename.extension (Why3.Driver.file_of_task driver "S" "T" task) in
let force = mode <> VCS.Batch in
let script = scriptfile ~force wpo ~ext in
- if Sys.file_exists script then Some (script, true) else
+ if Filepath.exists script then Some (script, true) else
if force then
begin
Command.pp_to_file script
@@ -1354,7 +1359,7 @@ let interactive ~mode wpo pconf ~config driver prover task =
| Some (script, merge) ->
Wp_parameters.debug ~dkey "%s %a script %S@."
(if merge then "Found" else "New")
- Why3.Whyconf.print_prover prover script ;
+ Why3.Whyconf.print_prover prover (script :> string) ;
match mode with
| VCS.Batch ->
compile ~script ~timeout ~memlimit ~config wpo pconf driver prover task
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index af2675f9f24..44e0595325e 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -38,7 +38,6 @@ val get_description : t -> string
val get_property : t -> Property.t
val get_result : t -> prover -> result
val get_results : t -> (prover * result) list
-
val get_sequent : t -> Conditions.sequent
val get_formula: t -> Lang.F.pred
val is_trivial : t -> bool
diff --git a/src/plugins/wp/gui/GuiProver.ml b/src/plugins/wp/gui/GuiProver.ml
index 523508a224c..64c87a6af46 100644
--- a/src/plugins/wp/gui/GuiProver.ml
+++ b/src/plugins/wp/gui/GuiProver.ml
@@ -74,8 +74,8 @@ class prover ~(console:Wtext.text) ~prover =
begin
let fout = Wpo.get_file_logout wpo prover in
let ferr = Wpo.get_file_logerr wpo prover in
- let lout = Sys.file_exists fout in
- let lerr = Sys.file_exists ferr in
+ let lout = Filepath.exists fout in
+ let lerr = Filepath.exists ferr in
if lout || lerr then console#hrule ;
console#scroll () ;
console#printf "[%a] %a@." VCS.pp_prover prover VCS.pp_result res ;
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 472469818ed..ea772351921 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -294,7 +294,7 @@ let stats_to_json g (s : Stats.stats) : Json.t =
let source = fst (Property.location target) in
let script = match ProofSession.get g with
| NoScript -> []
- | Script file | Deprecated file -> [ "script", `String file ]
+ | Script file | Deprecated file -> [ "script", `String (file :> string) ]
in
let index =
match g.po_idx with
@@ -333,7 +333,7 @@ let stats_to_json g (s : Stats.stats) : Json.t =
let do_report_json () =
let file = Wp_parameters.ReportJson.get () in
- if file <> "" then
+ if not (Filepath.Normalized.is_empty file) then
let json = List.rev @@
GOALS.fold
(fun g json ->
@@ -612,19 +612,16 @@ let compute_auto ~script =
end
type session_scripts = {
- updated: (Wpo.t * string * Json.t) list;
- incomplete: (Wpo.t * string * Json.t) list;
- removed: (Wpo.t * string) list;
+ updated: (Wpo.t * Filepath.Normalized.t * Json.t) list;
+ incomplete: (Wpo.t * Filepath.Normalized.t * Json.t) list;
+ removed: (Wpo.t * Filepath.Normalized.t) list;
}
let do_collect_session goals =
let updated = ref [] in
let incomplete = ref [] in
let removed = ref [] in
- let file goal =
- Format.asprintf "%a"
- ProofSession.pp_file @@ ProofSession.filename ~force:false goal
- in
+ let file goal = ProofSession.filename ~force:false goal in
Bag.iter
begin fun goal ->
let results = Wpo.get_results goal in
@@ -686,7 +683,7 @@ let do_update_session script session =
let do_show_session updated_session session =
let show enabled kind dkey file =
if enabled then
- Wp_parameters.result ~dkey "[%s] %a" kind ProofSession.pp_file file
+ Wp_parameters.result ~dkey "[%s] %a" kind Filepath.Normalized.pretty file
in
(* Note: we display new (in)valid scripts only when updating *)
List.iter
diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml
index 7f63a336980..86e9fe85c95 100644
--- a/src/plugins/wp/wpApi.ml
+++ b/src/plugins/wp/wpApi.ml
@@ -231,7 +231,7 @@ let () = S.option gmodel ~name:"script"
~get:(fun wpo ->
match ProofSession.get wpo with
| NoScript -> None
- | Script a | Deprecated a -> Some a)
+ | Script a | Deprecated a -> Some (a :> string))
let () = S.column gmodel ~name:"saved"
~descr:(Md.plain "Saved Script")
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index 6e09d4fd1ab..32ab774e70e 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -891,8 +891,9 @@ let export_json gstat ?jinput ~joutput () =
Wp_parameters.feedback "Report out: '%s'" joutput ;
jinput
in
- if Sys.file_exists jfile then
- Json.load_file jfile
+ let jpath = Filepath.Normalized.of_string jfile in
+ if Filepath.exists jpath then
+ Json.load_file jpath
else `Null
with Json.Error(file,line,msg) ->
let source = Log.source ~file ~line in
@@ -900,7 +901,7 @@ let export_json gstat ?jinput ~joutput () =
`Null
in
rankify_fcstat gstat js ;
- Json.save_file joutput (json_of_fcstat gstat) ;
+ Json.save_file (Filepath.Normalized.of_string joutput) (json_of_fcstat gstat) ;
end
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 4be71f7e9d3..4211952b82f 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1108,10 +1108,11 @@ module Report =
let () = Parameter_customize.set_group wp_po
let () = Parameter_customize.do_not_save ()
module ReportJson =
- String(struct
+ Filepath(struct
let option_name = "-wp-report-json"
let arg_name ="file.json"
- let default = ""
+ let file_kind = "JSON report"
+ let existence = Fc_Filepath.Indifferent
let help = "Output proof results in JSON format."
end)
let () = on_reset ReportJson.clear
@@ -1163,10 +1164,11 @@ module CheckMemoryContext =
let () = Parameter_customize.set_group wp_po
module OutputDir =
- String(struct
+ Filepath(struct
+ let existence = Fc_Filepath.Indifferent
let option_name = "-wp-out"
let arg_name = "dir"
- let default = ""
+ let file_kind = "directory"
let help = "Set working directory for generated files.\n\
Defaults to some temporary directory."
end)
@@ -1177,29 +1179,21 @@ module OutputDir =
let dkey = register_category "output"
-let has_out () = OutputDir.get() <> ""
+let has_out () = Fc_Filepath.Normalized.is_empty (OutputDir.get ())
let make_output_dir dir =
- if Sys.file_exists dir then
- begin
- if not (Sys.is_directory dir) then
- abort "File '%s' is not a directory (WP aborted)" dir ;
- end
- else
- begin
- try
- Extlib.mkdir ~parents:true dir 0o770 ;
- debug ~dkey "Created output directory '%s'" dir
- with Unix.Unix_error (err,_,_) ->
- let msg = Unix.error_message err in
- abort
- "System Error (%s)@\nCan not create output directory '%s'"
- msg dir
- end
+ try
+ if Extlib.mkdir ~parents:true dir 0o770 then
+ debug ~dkey "Created output directory '%a'" Fc_Filepath.Normalized.pretty dir
+ with Unix.Unix_error (err,_,_) ->
+ let msg = Unix.error_message err in
+ abort
+ "System Error (%s)@\nCan not create output directory '%a'"
+ msg Fc_Filepath.Normalized.pretty dir
(*[LC] Do not projectify this reference : it is common to all projects *)
-let unique_tmp = ref None
-let make_tmp_dir () =
+let unique_tmp : Fc_Filepath.Normalized.t option ref = ref None
+let make_tmp_dir () : Fc_Filepath.Normalized.t =
match !unique_tmp with
| None ->
let tmp =
@@ -1208,7 +1202,7 @@ let make_tmp_dir () =
abort "Cannot create temporary file: %s" s
in
unique_tmp := Some tmp ;
- debug ~dkey "Created temporary directory '%s'" tmp ;
+ debug ~dkey "Created temporary directory '%a'" Fc_Filepath.Normalized.pretty tmp ;
tmp
| Some tmp -> tmp
@@ -1218,9 +1212,9 @@ let make_gui_dir () =
try Sys.getenv "USERPROFILE" (*Win32*) with Not_found ->
try Sys.getenv "HOME" (*Unix like*) with Not_found ->
"." in
- let dir = home ^ "/" ^ ".frama-c-wp" in
- if Sys.file_exists dir && Sys.is_directory dir then
- Extlib.safe_remove_dir dir;
+ let dir = Fc_Filepath.Normalized.of_string (home ^ "/" ^ ".frama-c-wp") in
+ if Fc_Filepath.exists dir && Fc_Filepath.is_dir dir then
+ Extlib.safe_remove_dir (dir:>string);
make_output_dir dir ; dir
with _ ->
make_tmp_dir ()
@@ -1229,18 +1223,22 @@ let make_gui_dir () =
let base_output = ref None
let base_output () =
match !base_output with
- | None -> let output =
- match OutputDir.get () with
- | "" ->
- if Fc_config.is_gui
- then make_gui_dir ()
- else make_tmp_dir ()
- | dir ->
- make_output_dir dir ; dir in
+ | None ->
+ let output =
+ let dir = OutputDir.get () in
+ if Fc_Filepath.Normalized.is_empty dir then
+ if Fc_config.is_gui
+ then make_gui_dir ()
+ else make_tmp_dir ()
+ else begin
+ make_output_dir dir ;
+ dir
+ end
+ in
base_output := Some output;
- Fc_Filepath.(add_symbolic_dir "WPOUT" (Normalized.of_string output)) ;
- Datatype.Filepath.of_string output
- | Some output -> Datatype.Filepath.of_string output
+ Fc_Filepath.(add_symbolic_dir "WPOUT" output) ;
+ output
+ | Some output -> output
let get_output () =
let base = base_output () in
@@ -1249,22 +1247,22 @@ let get_output () =
if name = "default" then base
else
let dir = Datatype.Filepath.concat base name in
- make_output_dir (dir :> string) ; dir
+ make_output_dir dir ; dir
let get_output_dir d =
let base = get_output () in
let path = Datatype.Filepath.concat base d in
- make_output_dir (path :> string) ; path
+ make_output_dir path ; path
(* -------------------------------------------------------------------------- *)
(* --- Session dir --- *)
(* -------------------------------------------------------------------------- *)
-let default = Fc_Filepath.pwd () ^ "/.frama-c"
+let default = Fc_Filepath.(Normalized.concat (pwd ()) "/.frama-c")
let has_session () =
Session.is_set () ||
- ( Sys.file_exists default && Sys.is_directory default )
+ ( Fc_Filepath.exists default && Fc_Filepath.is_dir default )
let get_session ~force () =
if force then
@@ -1278,7 +1276,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
- if force then make_output_dir (path :> string) ; path
+ if force then make_output_dir path ; path
(* -------------------------------------------------------------------------- *)
(* --- Print Generated --- *)
@@ -1290,11 +1288,11 @@ let has_print_generated () = has_dkey cat_print_generated
let print_generated ?header file =
let header = match header with
- | None -> Fc_Filepath.Normalized.to_pretty_string (Datatype.Filepath.of_string file)
+ | None -> Fc_Filepath.Normalized.to_pretty_string file
| Some head -> head in
debug ~dkey:cat_print_generated "%S@\n%t@." header
begin fun fmt ->
- if not (Sys.file_exists file) then
+ if not (Fc_Filepath.exists file) then
Format.pp_print_string fmt "<missing file>"
else
Command.read_lines file (fun s ->
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 8cca2d16776..58a9e4412bd 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -156,7 +156,7 @@ module TruncPropIdFileName: Parameter_sig.Int
module Print: Parameter_sig.Bool
module Status: Parameter_sig.Bool
module Report: Parameter_sig.String_list
-module ReportJson: Parameter_sig.String
+module ReportJson: Parameter_sig.Filepath
module OldReportJson: Parameter_sig.String
module ReportName: Parameter_sig.String
module MemoryContext: Parameter_sig.Bool
@@ -176,12 +176,12 @@ val get_session : force:bool -> unit -> Datatype.Filepath.t
val get_session_dir : force:bool -> string -> Datatype.Filepath.t
val get_output : unit -> Datatype.Filepath.t
val get_output_dir : string -> Datatype.Filepath.t
-val make_output_dir : string -> unit
+val make_output_dir : Datatype.Filepath.t -> unit
(** {2 Debugging Categories} *)
val has_print_generated: unit -> bool
-val print_generated: ?header:string -> string -> unit
+val print_generated: ?header:string -> Filepath.Normalized.t -> unit
(** print the given file if the debugging category
"print-generated" is set *)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index f2e85404600..a97ca54dec6 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -82,7 +82,7 @@ struct
Format.fprintf fmt "_%s" s) ;
Format.fprintf fmt ".%s" ext ;
Format.pp_print_flush fmt ();
- Buffer.contents buffer
+ Filepath.Normalized.of_string (Buffer.contents buffer)
let file_logout ~pid ~model ~prover =
let id = WpPropId.get_propid pid in
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 1ee9f70e038..c23d0a30f8c 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -35,7 +35,7 @@ type index =
module DISK :
sig
- val file_goal : pid:prop_id -> model:WpContext.model -> prover:prover -> string
+ val file_goal : pid:prop_id -> model:WpContext.model -> prover:prover -> Filepath.Normalized.t
end
module GOAL :
@@ -95,10 +95,10 @@ val get_label : t -> string
val get_model : t -> WpContext.model
val get_scope : t -> WpContext.scope
val get_context : t -> WpContext.context
-val get_file_logout : t -> prover -> string
+val get_file_logout : t -> prover -> Filepath.Normalized.t
(** only filename, might not exists *)
-val get_file_logerr : t -> prover -> string
+val get_file_logerr : t -> prover -> Filepath.Normalized.t
(** only filename, might not exists *)
val qed_time : t -> float
--
GitLab