Merge branch 'feature/michele/782-wp' into 'master'

[wp] Use Filepath instead of mere strings.

Closes #782

See merge request frama-c/frama-c!2631

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

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
 

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                                     --- *)

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)

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 ;

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

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) ;

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

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 ->

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
 
 (* -------------------------------------------------------------------------- *)

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                                                    --- *)

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
 

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