diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index c4d82ec1ddebe78e7601bcfaebcb2a6a3d6487a3..b9d1954e66c90885377d0a694dabc8257fcbf32b 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -137,6 +137,19 @@ ifeq ($(FRAMAC_INTERNAL),yes)
Wp_DEFAULT_TESTS: create_share_link
endif
+# --------------------------------------------------------------------------
+# --- Qualif Tests ---
+# --------------------------------------------------------------------------
+
+wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt
+ ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+
+wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt
+ FRAMAC_WP_MODE=update ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+
+wp-qualif-cleanup: ./bin/toplevel.opt ./bin/ptests.opt
+ FRAMAC_WP_MODE=cleanup ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+
# --------------------------------------------------------------------------
# --- Dynamic Plugin ---
# --------------------------------------------------------------------------
diff --git a/src/plugins/wp/ProofSession.ml b/src/plugins/wp/ProofSession.ml
index 7c24fa9e7d9b2e6741d42ff775534390bc125ec5..5c51f11f39d94bbf16660abdcc585c0a178e3bba 100644
--- a/src/plugins/wp/ProofSession.ml
+++ b/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 ;
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 295acb36142011bdd3c2092804ae9ec7934b61d0..e3f3b6659e42f7391963d23be06e5b775cfcaaff 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/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
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index e9b9477243ea904b45bf416c80c619b64a3a8375..e2371df94b2bf5afa62ce0dc71ee146b43d8319a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -304,7 +304,8 @@ let do_progress goal msg =
(* ------------------------------------------------------------------------ *)
let do_report_cache_usage mode =
- if not (Wp_parameters.has_dkey dkey_shell) &&
+ if !exercised > 0 &&
+ not (Wp_parameters.has_dkey dkey_shell) &&
not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
then
let hits = ProverWhy3.get_hits () in
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 838af174f9304c7c29ae2f637aecb8f9b77290eb..f393582db884e9aee47f4da8f61053bd5b6285a1 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,3 +1,3 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache offline @PTEST_FILE@
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay @PTEST_FILE@
LOG: @PTEST_NAME@.@PTEST_NUMBER@.report.json
OPT:
diff --git a/src/plugins/wp/tests/wp_plugin/nosession.i b/src/plugins/wp/tests/wp_plugin/nosession.i
new file mode 100644
index 0000000000000000000000000000000000000000..7f7238c4b0e08395fc2d4c1685556bbeb6b7bd9d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/nosession.i
@@ -0,0 +1,12 @@
+/* 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; }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..21dad7a45d6492664cfd7d5c8ecd4aed040ddadf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nosession.res.oracle
@@ -0,0 +1,8 @@
+# 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
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 7a867069661811e172c4368b74c8207599948166..54249649895013f4b56a7bf7cc421d5129875e68 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/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
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 825c4377f8f0e867338c8c29c19ae3436dc2282b..3429afff23bf26b541eeea063d58f526cfc04854 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/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