[wp] create session dir only when necessary

src/plugins/wp/ProofSession.ml

@@ -30,12 +30,12 @@ type status =
 let files : (string,status) Hashtbl.t = Hashtbl.create 32
 
 let filename wpo =
-  let d = Wp_parameters.get_session_dir "script" in
+  let d = Wp_parameters.get_session_dir ~force:false "script" in
   Printf.sprintf "%s/%s.json" d wpo.po_gid
 
 let legacies wpo =
   let m = WpContext.MODEL.id wpo.po_model in
-  let d = Wp_parameters.get_session_dir m in
+  let d = Wp_parameters.get_session_dir ~force:false m in
   List.map (Printf.sprintf "%s/%s.json" d) [
     wpo.po_gid ;
     wpo.po_leg ;

src/plugins/wp/ProverWhy3.ml

@@ -1149,9 +1149,9 @@ let mark_cache ~mode hash =
 
 let cleanup_cache ~mode =
   if mode = Cleanup && (!hits > 0 || !miss > 0) then
-    let dir = Wp_parameters.get_session_dir "cache" in
+    let dir = Wp_parameters.get_session_dir ~force:false "cache" in
     try
-      if Sys.is_directory dir then
+      if Sys.file_exists dir && Sys.is_directory dir then
         Array.iter
           (fun f ->
              if Filename.check_suffix f ".json" then
@@ -1270,24 +1270,27 @@ let get_cache_result ~mode hash =
   match mode with
   | NoCache | Rebuild -> VCS.no_result
   | Update | Cleanup | Replay | Offline ->
-      let dir = Wp_parameters.get_session_dir "cache" 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 dir = Wp_parameters.get_session_dir ~force:false "cache" in
+      if not (Sys.file_exists dir && Sys.is_directory dir) then
+        VCS.no_result
       else
-        try
-          mark_cache ~mode hash ;
-          Json.load_file file |> ProofScript.result_of_json
-        with err ->
-          Wp_parameters.warning ~current:false ~once:true
-            "invalid cache entry (%s)" (Printexc.to_string err) ;
-          VCS.no_result
+        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
+        else
+          try
+            mark_cache ~mode hash ;
+            Json.load_file file |> ProofScript.result_of_json
+          with err ->
+            Wp_parameters.warning ~current:false ~once:true
+              "invalid cache entry (%s)" (Printexc.to_string err) ;
+            VCS.no_result
 
 let set_cache_result ~mode hash prover result =
   match mode with
   | NoCache | Replay | Offline -> ()
   | Rebuild | Update | Cleanup ->
-      let dir = Wp_parameters.get_session_dir "cache" in
+      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
       try

src/plugins/wp/tests/wp_plugin/nosession.i

+/* run.config
+   DONTRUN:
+*/
+
+/* run.config_qualif
+   CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp-msg-key shell
+   OPT: -wp -wp-prover alt-ergo -wp-session shall_not_exists_dir -wp-cache offline
+   COMMENT: The session directory shall not be created
+ */
+
+//@ ensures \false ;
+void f(void) { return; }

src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/nosession.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Failed] Goal typed_f_ensures
+[wp] Proved goals:    0 / 1

src/plugins/wp/wp_parameters.ml

@@ -1070,12 +1070,23 @@ let has_session () =
   Session.Dir_name.is_set () ||
   ( Sys.file_exists default && Sys.is_directory default )
 
-let get_session () = Session.dir ~error:false ()
+let get_session ~force () =
+  if force then
+    Session.dir ~error:false ()
+  else
+  if Session.Dir_name.is_set () then
+    Session.Dir_name.get ()
+  else
+    Session.dir ~error:false ()
 
-let get_session_dir d =
-  let base = get_session () in
+let get_session_dir ~force d =
+  let base = get_session ~force () in
   let path = Printf.sprintf "%s/%s" base d in
-  make_output_dir path ; path
+  if force then make_output_dir path ; path
+
+(* -------------------------------------------------------------------------- *)
+(* --- Print Generated                                                    --- *)
+(* -------------------------------------------------------------------------- *)
 
 let cat_print_generated = register_category "print-generated"
 
@@ -1094,3 +1105,5 @@ let print_generated ?header file =
             Format.pp_print_string fmt s;
             Format.pp_print_newline fmt ())
     end
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/wp_parameters.mli

@@ -148,8 +148,8 @@ module Check: Parameter_sig.Bool
 
 val has_out : unit -> bool
 val has_session : unit -> bool
-val get_session : unit -> string
-val get_session_dir : string -> string
+val get_session : force:bool -> unit -> string
+val get_session_dir : force:bool -> string -> string
 val get_output : unit -> string
 val get_output_dir : string -> string
 val make_output_dir : string -> unit