diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index e9bb77dc5b58e7db6a8c749cb56b436ddcc6f753..95ac91b54a78f1b936e758e5604d9945eb848792 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -114,7 +114,7 @@ let dump_buffer buffer = function
let n = Buffer.length buffer in
if n > 0 then
Command.write_file log (fun out -> Buffer.output_buffer out buffer)
- else if Wp_parameters.is_out () then
+ else if Wp_parameters.has_out () then
Extlib.safe_remove log
let echo_buffer buffer =
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 8e212b42b0c27d5fc02750d6d5e3274c24c9fed7..bd4235548ac9a83f57cdaae89a3f19ca2459ccd2 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1147,10 +1147,10 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
parse_mode ~origin ~fallback:"-wp-cache" (Sys.getenv origin)
with Not_found ->
try
- parse_mode ~origin:"-wp-cache" ~fallback:"'none'"
+ parse_mode ~origin:"-wp-cache" ~fallback:"none"
(Wp_parameters.Cache.get())
with Not_found ->
- if Wp_parameters.Session.Dir_name.is_set ()
+ if Wp_parameters.has_session ()
then Update else NoCache
end)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 7b4d1efe744adb0261e2d04bd7b245dd09272c6a..3f93fa21f7a9e0628163176d4edf3f9325aa2618 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -21,7 +21,10 @@
(**************************************************************************)
open Factory
-let job_key= Wp_parameters.register_category "trace-job"
+
+let dkey_main = Wp_parameters.register_category "main"
+let dkey_raised = Wp_parameters.register_category "raised"
+let dkey_shell = Wp_parameters.register_category "shell"
(* --------- Command Line ------------------- *)
@@ -296,6 +299,49 @@ let do_progress goal msg =
pp goal.Wpo.po_sid msg ;
end
+(* ------------------------------------------------------------------------ *)
+(* --- Caching --- *)
+(* ------------------------------------------------------------------------ *)
+
+let do_report_cache_usage mode =
+ if not (Wp_parameters.has_dkey dkey_shell) &&
+ not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
+ then
+ let hits = ProverWhy3.get_hits () in
+ let miss = ProverWhy3.get_miss () in
+ if hits <= 0 && miss <= 0 then
+ Wp_parameters.result "[Cache] not used"
+ else
+ Wp_parameters.result "[Cache]%t"
+ begin fun fmt ->
+ let sep = ref " " in
+ let pp_cache fmt n job =
+ if n > 0 then
+ ( Format.fprintf fmt "%s%s:%d" !sep job n ; sep := ", " ) in
+ match mode with
+ | ProverWhy3.NoCache -> ()
+ | ProverWhy3.Replay ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "missed" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Offline ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "failed" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Update | ProverWhy3.Cleanup ->
+ pp_cache fmt hits "found" ;
+ pp_cache fmt miss "updated" ;
+ Format.pp_print_newline fmt () ;
+ | ProverWhy3.Rebuild ->
+ pp_cache fmt hits "replaced" ;
+ pp_cache fmt miss "updated" ;
+ Format.pp_print_newline fmt () ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Prover Results --- *)
+(* -------------------------------------------------------------------------- *)
+
let do_wpo_stat goal prover res =
let s = get_pstat prover in
let open VCS in
@@ -441,6 +487,8 @@ let do_report_scheduled () =
Wp_parameters.result "%d goal%s generated" !exercised plural
else
let proved = GOALS.cardinal !proved in
+ let mode = ProverWhy3.get_mode () in
+ if mode <> ProverWhy3.NoCache then do_report_cache_usage mode ;
Wp_parameters.result "%t"
begin fun fmt ->
Format.fprintf fmt "Proved goals: %4d / %d@\n" proved !scheduled ;
@@ -458,58 +506,6 @@ let do_list_scheduled_result () =
clear_scheduled () ;
end
-(* ------------------------------------------------------------------------ *)
-(* --- Caching --- *)
-(* ------------------------------------------------------------------------ *)
-
-let dkey_cache = Wp_parameters.register_category "cache"
-
-let do_report_cache_usage mode =
- let hits = ProverWhy3.get_hits () in
- let miss = ProverWhy3.get_miss () in
- let removed = ProverWhy3.get_removed () in
- if hits <= 0 && miss <= 0 then
- Wp_parameters.result "[Cache] not used"
- else
- Wp_parameters.result "[Cache]%t"
- begin fun fmt ->
- let sep = ref " " in
- let pp_cache fmt n job =
- if n > 0 then
- ( Format.fprintf fmt "%s%s:%d" !sep job n ; sep := ", " ) in
- match mode with
- | ProverWhy3.NoCache -> ()
- | ProverWhy3.Replay ->
- pp_cache fmt hits "found" ;
- pp_cache fmt miss "missed" ;
- Format.pp_print_newline fmt () ;
- | ProverWhy3.Offline ->
- pp_cache fmt hits "found" ;
- pp_cache fmt miss "failed" ;
- Format.pp_print_newline fmt () ;
- | ProverWhy3.Update ->
- pp_cache fmt hits "found" ;
- pp_cache fmt miss "updated" ;
- Format.pp_print_newline fmt () ;
- | ProverWhy3.Cleanup ->
- pp_cache fmt hits "found" ;
- pp_cache fmt miss "missed" ;
- pp_cache fmt removed "removed" ;
- Format.pp_print_newline fmt () ;
- | ProverWhy3.Rebuild ->
- pp_cache fmt (hits+miss) "updated" ;
- Format.pp_print_newline fmt () ;
- end
-
-(* registered at frama-c (normal) exit *)
-let do_cache_cleanup () =
- begin
- let mode = ProverWhy3.get_mode () in
- ProverWhy3.cleanup_cache ~mode ;
- if Wp_parameters.has_dkey dkey_cache
- then do_report_cache_usage mode ;
- end
-
(* ------------------------------------------------------------------------ *)
(* --- Proving --- *)
(* ------------------------------------------------------------------------ *)
@@ -693,6 +689,19 @@ let do_wp_proofs () = do_wp_proofs_iter (fun f -> Wpo.iter ~on_goal:f ())
let do_wp_proofs_for goals = do_wp_proofs_iter (fun f -> Bag.iter f goals)
+(* registered at frama-c (normal) exit *)
+let do_cache_cleanup () =
+ begin
+ let mode = ProverWhy3.get_mode () in
+ ProverWhy3.cleanup_cache ~mode ;
+ let removed = ProverWhy3.get_removed () in
+ if removed > 0 &&
+ not (Wp_parameters.has_dkey dkey_shell) &&
+ not (Wp_parameters.has_dkey VCS.dkey_no_cache_info)
+ then
+ Wp_parameters.result "[Cache] removed:%d" removed
+ end
+
(* ------------------------------------------------------------------------ *)
(* --- Secondary Entry Points --- *)
(* ------------------------------------------------------------------------ *)
@@ -877,13 +886,15 @@ let pp_wp_parameters fmt =
Format.pp_print_newline fmt () ;
end
-let dkey_shell = Wp_parameters.register_category "shell"
-
let () = Cmdline.run_after_setting_files
(fun _ ->
if Wp_parameters.has_dkey dkey_shell then
Log.print_on_output pp_wp_parameters)
+(* -------------------------------------------------------------------------- *)
+(* --- Prover Configuration & Detection --- *)
+(* -------------------------------------------------------------------------- *)
+
let () = Cmdline.run_after_configuring_stage Why3Provers.configure
let do_prover_detect () =
@@ -915,8 +926,6 @@ let rec try_sequence jobs () = match jobs with
| head :: tail ->
Extlib.try_finally ~finally:(try_sequence tail) head ()
-let dkey_raised = Wp_parameters.register_category "raised"
-
let sequence jobs () =
if Wp_parameters.has_dkey dkey_raised
then List.iter (fun f -> f ()) jobs
@@ -932,12 +941,12 @@ let tracelog () =
end
let main = sequence [
- (fun () -> Wp_parameters.debug ~dkey:job_key "Start WP plugin...@.") ;
+ (fun () -> Wp_parameters.debug ~dkey:dkey_main "Start WP plugin...@.") ;
do_prover_detect ;
cmdline_run ;
tracelog ;
Wp_parameters.reset ;
- (fun () -> Wp_parameters.debug ~dkey:job_key "Stop WP plugin...@.") ;
+ (fun () -> Wp_parameters.debug ~dkey:dkey_main "Stop WP plugin...@.") ;
]
let () = Cmdline.at_normal_exit do_cache_cleanup
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index dadeb120b00dcd110e99dcd63b1eb270116346e2..863bcebb4efd5720cafe73649a5b455303df55fe 100644
--- a/src/plugins/wp/tests/wp_plugin/removed.i
+++ b/src/plugins/wp/tests/wp_plugin/removed.i
@@ -1,5 +1,5 @@
/* run.config_qualif
- CMD: @frama-c@ -wp-share ./share -wp-msg-key success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache offline
+ CMD: @frama-c@ -wp-share ./share -wp-msg-key no-cache-info,success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache offline
OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 7092834874e4e70f2e90b8641eb250e0816438b8..7a867069661811e172c4368b74c8207599948166 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -20,7 +20,8 @@
(* *)
(**************************************************************************)
-module Fc_config = Config
+module Fc_Config = Config
+
let () = Plugin.is_share_visible ()
let () = Plugin.is_session_visible ()
include Plugin.Register
@@ -962,7 +963,7 @@ module Check =
let () = on_reset Print.clear
(* -------------------------------------------------------------------------- *)
-(* --- OS environment variables --- *)
+(* --- Overflows --- *)
(* -------------------------------------------------------------------------- *)
let active_unless_rte option =
@@ -974,24 +975,13 @@ let active_unless_rte option =
let get_overflows () = Overflows.get () && active_unless_rte "-wp-overflows"
-let dkey = register_category "env"
-
-let get_env ?default var =
- try
- let varval = Sys.getenv var in
- debug ~dkey "ENV %s=%S" var varval ; varval
- with Not_found ->
- debug ~dkey "ENV %s not set." var ;
- match default with
- | Some varval ->
- debug ~dkey "ENV %s default(%S)" var varval ; varval
- | None ->
- debug ~dkey "ENV %s undefined." var ;
- raise Not_found
+(* -------------------------------------------------------------------------- *)
+(* --- Output Dir --- *)
+(* -------------------------------------------------------------------------- *)
let dkey = register_category "prover"
-let is_out () = !Fc_config.is_gui || OutputDir.get() <> ""
+let has_out () = OutputDir.get () <> ""
let make_output_dir dir =
if Sys.file_exists dir then
@@ -1046,7 +1036,7 @@ let base_output () =
| None -> let output =
match OutputDir.get () with
| "" ->
- if !Fc_config.is_gui
+ if !Fc_Config.is_gui
then make_gui_dir ()
else make_tmp_dir ()
| dir ->
@@ -1056,13 +1046,6 @@ let base_output () =
output
| Some output -> output
-let get_session () = Session.dir ~error:false ()
-
-let get_session_dir d =
- let base = get_session () in
- let path = Printf.sprintf "%s/%s" base d in
- make_output_dir path ; path
-
let get_output () =
let base = base_output () in
let project = Project.current () in
@@ -1077,6 +1060,23 @@ let get_output_dir d =
let path = Printf.sprintf "%s/%s" base d in
make_output_dir path ; path
+(* -------------------------------------------------------------------------- *)
+(* --- Session dir --- *)
+(* -------------------------------------------------------------------------- *)
+
+let default = Sys.getcwd () ^ "/.frama-c"
+
+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_dir d =
+ let base = get_session () in
+ let path = Printf.sprintf "%s/%s" base d in
+ make_output_dir path ; path
+
let cat_print_generated = register_category "print-generated"
let has_print_generated () = has_dkey cat_print_generated
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 0df6e3b814b7752ed59636f1ec5c79cf66dc0936..825c4377f8f0e867338c8c29c19ae3436dc2282b 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -144,10 +144,10 @@ module ReportName: Parameter_sig.String
module MemoryContext: Parameter_sig.Bool
module Check: Parameter_sig.Bool
-(** {2 Environment Variables} *)
+(** {2 Getters} *)
-val get_env : ?default:string -> string -> string
-val is_out : unit -> bool (* -wp-out <dir> positioned *)
+val has_out : unit -> bool
+val has_session : unit -> bool
val get_session : unit -> string
val get_session_dir : string -> string
val get_output : unit -> string