diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 9545120970c27c80baf0b83d1a3402b7aab98bae..05e69ee8fa429acacd8f148a514344fe93374df2 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/src/plugins/wp/ProofSession.ml
@@ -29,7 +29,8 @@ type script =
let files : (string,script) Hashtbl.t = Hashtbl.create 32
-let jsonfile = Printf.sprintf "%s/%s.json"
+let jsonfile (dir:Datatype.Filepath.t) =
+ Format.sprintf "%s/%s.json" (dir :> string)
let filename ~force wpo =
let dscript = Wp_parameters.get_session_dir ~force "script" in
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index 446fceadc1b41cdb2535aa24fab4ef83316af348..4e864a4579f58e4501e81622308ad3af028ebc9b 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -34,7 +34,7 @@ let dkey = Wp_parameters.register_category "prover"
let cluster_file c =
let dir = WpContext.directory () in
let base = cluster_id c in
- Printf.sprintf "%s/%s.v" dir base
+ Printf.sprintf "%s/%s.v" (dir :> string) base
(* -------------------------------------------------------------------------- *)
(* --- External Coq Libraries --- *)
@@ -314,8 +314,8 @@ and assemble_coqlib coqcc c =
begin
let tgtdir = Wp_parameters.get_output_dir "coqwp" in
let source = Printf.sprintf "%s/%s" c.c_source c.c_file in
- let target = Printf.sprintf "%s/%s" tgtdir c.c_file in
- let dir = Printf.sprintf "%s/%s" tgtdir c.c_path in
+ let target = Printf.sprintf "%s/%s" (tgtdir :> string) c.c_file in
+ let dir = Printf.sprintf "%s/%s" (tgtdir :> string) c.c_path in
if need_recompile ~source ~target then
begin
Wp_parameters.make_output_dir dir ;
@@ -333,7 +333,7 @@ let assemble_goal ~pid axioms prop =
let title = Pretty_utils.to_string WpPropId.pretty pid in
let model = WpContext.directory () in
let id = WpPropId.get_propid pid in
- let file = Printf.sprintf "%s/%s.coq" model id in
+ let file = Printf.sprintf "%s/%s.coq" (model :> string) id in
let goal = cluster ~id ~title () in
let deps = Command.print_file file
begin fun fmt ->
@@ -359,7 +359,7 @@ let assemble_goal ~pid axioms prop =
end in
let coqcc = { marked = Marked.empty ; includes = [] ; sources = [] } in
List.iter (assemble coqcc) deps ;
- let includes = (model , "") :: List.rev coqcc.includes in
+ let includes = ((model :> string) , "") :: List.rev coqcc.includes in
let sources = List.rev coqcc.sources in
includes , sources , file
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index a1f4594ddba1101cda469be56dd43fe3d88e5875..e18c2ffc06e29089fe8f6f19333c1e323a57868b 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -72,7 +72,7 @@ let rec locate_error files file line =
let cluster_file c =
let dir = WpContext.directory () in
let base = cluster_id c in
- Printf.sprintf "%s/%s.ergo" dir base
+ Format.sprintf "%s/%s.ergo" (dir :> string) base
(* -------------------------------------------------------------------------- *)
(* --- Exporting Formulae to Alt-Ergo --- *)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 299e199eefd4857fd3f8d4f793da7b06d49b10c9..b92024e34de4387a9d6ae4a6607141ae8bd19403 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -50,7 +50,7 @@ let get_why3_env = Env.memoize
let config = Why3Provers.config () in
let main = Why3.Whyconf.get_main config in
let ld =
- (WpContext.directory ())::
+ (WpContext.directory () :> string)::
((Wp_parameters.Share.get_dir ~mode:`Must_exist "why3") :> string)::
(Why3.Whyconf.loadpath main) in
Why3.Env.create_env ld
@@ -790,7 +790,7 @@ class visitor (ctx:context) c =
then
let tgtdir = WpContext.directory () in
let why3src = Filename.basename source in
- let target = Printf.sprintf "%s/%s" tgtdir why3src in
+ let target = Printf.sprintf "%s/%s" (tgtdir :> string) why3src in
Command.copy source target
in
let iter_file opt =
@@ -1238,6 +1238,7 @@ let mark_cache ~mode hash =
let cleanup_cache ~mode =
if mode = Cleanup && (!hits > 0 || !miss > 0) then
let dir = Wp_parameters.get_session_dir ~force:false "cache" in
+ let dir = (dir :> string) in
try
if Sys.file_exists dir && Sys.is_directory dir then
Array.iter
@@ -1361,6 +1362,7 @@ let get_cache_result ~mode hash =
| NoCache | Rebuild -> VCS.no_result
| Update | Cleanup | Replay | Offline ->
let dir = Wp_parameters.get_session_dir ~force:false "cache" in
+ let dir = (dir :> string) in
if not (Sys.file_exists dir && Sys.is_directory dir) then
VCS.no_result
else
@@ -1382,11 +1384,11 @@ let set_cache_result ~mode hash prover result =
| Rebuild | Update | Cleanup ->
let dir = Wp_parameters.get_session_dir ~force:true "cache" in
let hash = Lazy.force hash in
- let file = Printf.sprintf "%s/%s.json" dir hash in
+ let file = Format.sprintf "%s/%s.json" (dir :> string) hash in
try
mark_cache ~mode hash ;
ProofScript.json_of_result (VCS.Why3 prover) result
- |> Json.save_file file
+ |> Json.save_file (file :> string)
with err ->
Wp_parameters.warning ~current:false ~once:true
"can not update cache (%s)" (Printexc.to_string err)
diff --git a/src/plugins/wp/RegionDump.ml b/src/plugins/wp/RegionDump.ml
index a52e783d1632901362639588427f6d36db0bf5cc..0a476427ebd5dbb79d3f42eded70068ffe7fb203 100644
--- a/src/plugins/wp/RegionDump.ml
+++ b/src/plugins/wp/RegionDump.ml
@@ -283,7 +283,9 @@ let dump ~dir kf map =
if Wp.has_dkey dot_key || Wp.has_dkey pdf_key then
begin
let name = Kf.get_name kf in
- let file = Printf.sprintf "%s/%s.dot" dir name in
+ let file =
+ Format.asprintf "%a/%s.dot" Datatype.Filepath.pretty dir name
+ in
let dot = Dotgraph.open_dot ~attr:[`LR] ~name ~file () in
dotgraph dot map ;
Dotgraph.close dot ;
diff --git a/src/plugins/wp/RegionDump.mli b/src/plugins/wp/RegionDump.mli
index fc77043cb8df91d571c4bbd4818d0fb09d1620a7..d332b9cb40c10db3fd15d61ad8b05a2772c8412d 100644
--- a/src/plugins/wp/RegionDump.mli
+++ b/src/plugins/wp/RegionDump.mli
@@ -23,4 +23,4 @@
(* Dump region graphs to dir according to -wp options.
By default, does nothing. *)
-val dump : dir:string -> Kernel_function.t -> Region.map -> unit
+val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> Region.map -> unit
diff --git a/src/plugins/wp/cfgDump.ml b/src/plugins/wp/cfgDump.ml
index b09e210f1b63df1fe4b9aa8d7a18ba0cedd16a9b..90c0924ba5d8ce03e4f3a8febd9bfaad56e256bc 100644
--- a/src/plugins/wp/cfgDump.ml
+++ b/src/plugins/wp/cfgDump.ml
@@ -40,7 +40,7 @@ struct
| None -> Kernel_function.get_name kf
| Some bname -> Kernel_function.get_name kf ^ "_" ^ bname
in
- let file = Filename.concat (Wp_parameters.get_output ()) name in
+ let file = Filename.concat (Wp_parameters.get_output () :> string) name in
Wp_parameters.feedback "CFG %a -> %s@." Kernel_function.pretty kf name ;
let fout = open_out (file ^ ".dot") in
fc := Some (fout,file) ;
diff --git a/src/plugins/wp/wpContext.mli b/src/plugins/wp/wpContext.mli
index 356eeaf759cb88e701e51c39a7e6215266df67ff..7693815595f66aa61dc739c8059173b0a812c50f 100644
--- a/src/plugins/wp/wpContext.mli
+++ b/src/plugins/wp/wpContext.mli
@@ -84,7 +84,8 @@ val get_model : unit -> model
val get_scope : unit -> scope
val get_context : unit -> context
-val directory : unit -> string (** Current model in ["-wp-out"] directory *)
+val directory : unit -> Datatype.Filepath.t
+(** Current model in ["-wp-out"] directory *)
module type Entries =
sig
diff --git a/src/plugins/wp/wpReached.ml b/src/plugins/wp/wpReached.ml
index 0c970996f3592219991ac60b48945e7eb8858721..98acfad8ecbdd9dcf19e600ffe29b1efa795a5b6 100644
--- a/src/plugins/wp/wpReached.ml
+++ b/src/plugins/wp/wpReached.ml
@@ -224,7 +224,7 @@ module N = Dotgraph.Node(Nmap)
let dump ~dir kf reached =
let name = Kernel_function.get_name kf in
- let file = Printf.sprintf "%s/%s.dot" dir name in
+ let file = Format.asprintf "%a/%s.dot" Datatype.Filepath.pretty dir name in
let dot = G.open_dot ~file ~name () in
N.define dot
(fun a na ->
diff --git a/src/plugins/wp/wpReached.mli b/src/plugins/wp/wpReached.mli
index 3de8854af0698118c6a6c5841fd5ef039e933451..2f7bc0283bc0c5cc24c0cdd7d6984cf1c3d40c95 100644
--- a/src/plugins/wp/wpReached.mli
+++ b/src/plugins/wp/wpReached.mli
@@ -47,6 +47,6 @@ val smoking : reached -> Cil_types.stmt -> bool
This is restricted to assignments, returns and calls not dominated
another smoking statement. *)
-val dump : dir:string -> Kernel_function.t -> reached -> unit
+val dump : dir:Datatype.Filepath.t -> Kernel_function.t -> reached -> unit
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 7d8a2e381c2f113d42356837e80079a93d62a117..8755b87107f3042d4e09bbe381fffafe685a2ae7 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -1094,8 +1094,8 @@ let base_output () =
make_output_dir dir ; dir in
base_output := Some output;
Fc_Filepath.add_symbolic_dir "WPOUT" output ;
- output
- | Some output -> output
+ Datatype.Filepath.of_string output
+ | Some output -> Datatype.Filepath.of_string output
let get_output () =
let base = base_output () in
@@ -1103,13 +1103,13 @@ let get_output () =
let name = Project.get_unique_name project in
if name = "default" then base
else
- let dir = base ^ "/" ^ name in
- make_output_dir dir ; dir
+ 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 = Printf.sprintf "%s/%s" base d in
- make_output_dir path ; path
+ let path = Datatype.Filepath.concat base ("/" ^ d) in
+ make_output_dir (path :> string) ; path
(* -------------------------------------------------------------------------- *)
(* --- Session dir --- *)
@@ -1132,8 +1132,8 @@ let get_session ~force () =
let get_session_dir ~force d =
let base = get_session ~force () in
- let path = Format.asprintf "%s/%s" (base :> string) d in
- if force then make_output_dir path ; path
+ let path = Datatype.Filepath.concat base ("/" ^ d) in
+ if force then make_output_dir (path :> string) ; path
(* -------------------------------------------------------------------------- *)
(* --- Print Generated --- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 3103707f18528f0d19d886fd4cb2927b7aba9c0b..fd0df0a2628df88f611165a8413c9b9dc33e2b5d 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -156,9 +156,9 @@ module SmokeDeadcall: Parameter_sig.Bool
val has_out : unit -> bool
val has_session : unit -> bool
val get_session : force:bool -> unit -> Datatype.Filepath.t
-val get_session_dir : force:bool -> string -> string
-val get_output : unit -> string
-val get_output_dir : string -> string
+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 get_overflows : unit -> bool
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index c3c6df38b3fa2fb326f0fb4f33bc4939f2e3b2e4..21f7f3a9fa1b25a40763c3172b6f9f529ac61746 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -88,7 +88,7 @@ struct
let mid = Wp_parameters.get_output_dir (WpContext.MODEL.id model) in
let buffer = Buffer.create 80 in
let fmt = Format.formatter_of_buffer buffer in
- Format.fprintf fmt "%s/%s" mid id ;
+ Format.fprintf fmt "%s/%s" (mid :> string) id ;
(match prover with None -> () | Some p ->
Format.fprintf fmt "_%s" (filename_for_prover p)) ;
(match suffix with None -> () | Some s ->
@@ -143,14 +143,14 @@ struct
let cache_log ~pid ~model ~prover ~result =
(*TODO: put a cache here *)
let dir = Wp_parameters.get_output () in
- let file = Printf.sprintf "%s/log.txt" dir in
+ let file = Printf.sprintf "%s/log.txt" (dir :> string) in
Command.print_file file (pretty ~pid ~model ~prover ~result) ;
file
let cache_descr pretty =
(*TODO: put a cache here *)
let dir = Wp_parameters.get_output () in
- let file = Printf.sprintf "%s/goal.txt" dir in
+ let file = Printf.sprintf "%s/goal.txt" (dir :> string) in
Command.print_file file (fun fmt -> pretty fmt) ; file
end