diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 909e27a9e3abee09ace72472c12e9b23ab4579c3..8e212b42b0c27d5fc02750d6d5e3274c24c9fed7 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1090,15 +1090,8 @@ type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
let hits = ref 0
let miss = ref 0
let removed = ref 0
-let cleanup = Hashtbl.create 0 (* used entries *)
-
-let reset () =
- begin
- hits := 0 ;
- miss := 0 ;
- removed := 0 ;
- Hashtbl.clear cleanup ;
- end
+let cleanup = Hashtbl.create 0
+(* used entries, never to be reset since cleanup is performed at exit *)
let get_hits () = !hits
let get_miss () = !miss
@@ -1108,7 +1101,7 @@ let mark_cache ~mode hash =
if mode = Cleanup then Hashtbl.replace cleanup hash ()
let cleanup_cache ~mode =
- if mode = Cleanup then
+ if mode = Cleanup && (!hits > 0 || !miss > 0) then
let dir = Wp_parameters.get_session_dir "cache" in
try
if Sys.is_directory dir then
@@ -1181,38 +1174,41 @@ let task_hash wpo drv prover task =
let time_fits time = function
| None | Some 0 -> true
- | Some limit ->
- time < float limit
+ | Some limit -> time <= float limit
-let step_fits steps = function
+let steps_fits steps = function
| None | Some 0 -> true
| Some limit -> steps <= limit
+let time_seized time = function
+ | None | Some 0 -> false
+ | Some limit -> float limit <= time
+
+let steps_seized steps steplimit =
+ steps <> 0 &&
+ match steplimit with
+ | None | Some 0 -> false
+ | Some limit -> limit <= steps
+
let promote ~timeout ~steplimit (res : VCS.result) =
match res.verdict with
| VCS.NoResult | VCS.Computing _ | VCS.Checked -> VCS.no_result
| VCS.Failed -> res
| VCS.Invalid | VCS.Valid | VCS.Unknown ->
- if not (step_fits res.prover_steps steplimit) then
+ if not (steps_fits res.prover_steps steplimit) then
{ res with verdict = Stepout }
else
if not (time_fits res.prover_time timeout) then
{ res with verdict = Timeout }
else res
- | Timeout ->
- if not (step_fits res.prover_steps steplimit) then
+ | VCS.Timeout | VCS.Stepout ->
+ if steps_seized res.prover_steps steplimit then
{ res with verdict = Stepout }
else
- if time_fits res.prover_time timeout then
- VCS.no_result
- else res
- | Stepout ->
- if step_fits res.prover_steps steplimit then
- VCS.no_result
- else
- if not (time_fits res.prover_time timeout) then
+ if time_seized res.prover_time timeout then
{ res with verdict = Timeout }
- else res
+ else (* can be run a longer time or widely *)
+ VCS.no_result
let get_cache_result ~mode hash =
match mode with
@@ -1288,8 +1284,6 @@ let prove ?timeout ?steplimit ~prover wpo =
then
begin
incr hits ;
- if mode = Cleanup then
- set_cache_result ~mode hash prover result ;
Task.return result
end
else
diff --git a/src/plugins/wp/ProverWhy3.mli b/src/plugins/wp/ProverWhy3.mli
index 70df0ed53b72d95ed503b1ee6a8f1766aa0d1977..e107c669a1514fc99be25823adee3dc9c7eaf2c6 100644
--- a/src/plugins/wp/ProverWhy3.mli
+++ b/src/plugins/wp/ProverWhy3.mli
@@ -32,8 +32,6 @@ val prove : ?timeout:int -> ?steplimit:int -> prover:Why3Provers.t ->
type mode = NoCache | Update | Replay | Rebuild | Offline | Cleanup
val get_mode : unit -> mode
-
-val reset : unit -> unit (** Reset cache statistics *)
val get_hits : unit -> int
val get_miss : unit -> int
val get_removed : unit -> int
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index df7d9606a5f819cbcdb79ebb0b6bf6b179c68ba8..8b30fba2dd614ba363e7558222a01d0c76fa6c33 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -230,7 +230,6 @@ let clear_scheduled () =
exercised := 0 ;
proved := GOALS.empty ;
provers := PM.empty ;
- ProverWhy3.reset () ;
end
let get_pstat p =
@@ -502,6 +501,7 @@ let do_report_cache_usage mode =
Format.pp_print_newline fmt () ;
end
+(* registered at frama-c (normal) exit *)
let do_cache_cleanup () =
begin
let mode = ProverWhy3.get_mode () in
@@ -680,7 +680,6 @@ let do_wp_proofs_iter iter =
begin
if spawned then do_list_scheduled iter ;
spawn_wp_proofs_iter ~mode iter ;
- do_cache_cleanup () ;
if spawned then
begin
do_list_scheduled_result () ;
@@ -916,40 +915,9 @@ let do_prover_detect () =
) provers
(* ------------------------------------------------------------------------ *)
-(* --- Main Entry Point --- *)
+(* --- Main Entry Points --- *)
(* ------------------------------------------------------------------------ *)
-(*
-(* This filter can be changed to make exceptions interrupting
- the sequence immediately *)
-let catch_exn (_:exn) =
- not (Wp_parameters.has_dkey "raised")
-
-(* This order can be changed *)
-let reraised_exn (first:exn) (_last:exn) = Some first
-
-(* Don't use Extlib.try_finally:
- No exception is used for control here.
- Backtrace is dumped here for debugging purpose.
- We just record one of the raised exceptions (to be raised again),
- while ensuring all tasks are finally executed. *)
-let protect err job =
- try job ()
- with e when catch_exn e ->
- let b = Printexc.get_raw_backtrace () in
- Wp_parameters.failure "%s@\n%s"
- (Printexc.to_string e)
- (Printexc.raw_backtrace_to_string b) ;
- match !err with
- | None -> err := Some e
- | Some previous -> err := reraised_exn previous e
-
-let sequence jobs =
- let err = ref None in
- List.iter (protect err) jobs ;
- match !err with None -> () | Some e -> raise e
-*)
-
let rec try_sequence jobs () = match jobs with
| [] -> ()
| head :: tail ->
@@ -980,4 +948,7 @@ let main = sequence [
(fun () -> Wp_parameters.debug ~dkey:job_key "Stop WP plugin...@.") ;
]
+let () = Cmdline.at_normal_exit do_cache_cleanup
let () = Db.Main.extend main
+
+(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/tests/wp_plugin/convert.i b/src/plugins/wp/tests/wp_plugin/convert.i
index 380f6dc6405686b87144779477816abc64802aea..630c406f9676e288b6fedf7f56b5bd86006d5d1b 100644
--- a/src/plugins/wp/tests/wp_plugin/convert.i
+++ b/src/plugins/wp/tests/wp_plugin/convert.i
@@ -3,9 +3,8 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-timeout 100 -wp-steps 500 -wp-share ./share -wp-msg-key shell,success-only -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@
- OPT: -wp-prover alt-ergo -wp-report=tests/qualif.report
- OPT: -wp-prover why3:alt-ergo -wp-report=tests/qualif-why3.report
+ OPT:
+ OPT: -wp-prover native:alt-ergo -wp-report=tests/native.report
*/
// --------------------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 226489bb68d4f81e8d2c708953bfabaf6fdbe63b..0f90c5deb366647d57c2b869aaeac6de026b9c5d 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -4,8 +4,7 @@
*/
/* run.config_qualif
- CMD: @frama-c@ -wp-share ./share -wp-msg-key cluster,shell -wp-par 1 -wp-timeout 100 -wp-steps 500
- OPT: -wp-model Typed -wp -wp-check -then -wp-model Typed+ref -wp -wp-check
+ OPT: -wp-msg-key cluster -wp-model Typed -wp-check -then -wp -wp-model Typed+ref -wp-check
*/
//@ predicate P(integer a);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
index 521d75998371f7b6d43197b4d990e7210f625971..324363205674edba699cb8e9bfe8af0293e73744 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/model.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/model.i (no preprocessing)
-[kernel] tests/wp_plugin/model.i:11: Warning:
+[kernel] tests/wp_plugin/model.i:10: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -82,7 +82,7 @@ end
Function f
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/model.i, line 13) in 'f':
+Goal Post-condition (file tests/wp_plugin/model.i, line 12) in 'f':
Let x = Mint_0[shift_sint32(p, k)].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
@@ -199,7 +199,7 @@ end
Function f
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/model.i, line 13) in 'f':
+Goal Post-condition (file tests/wp_plugin/model.i, line 12) in 'f':
Let x = Mint_0[shift_sint32(p, k)].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
@@ -210,7 +210,7 @@ Prove: P_P(x).
------------------------------------------------------------
-Goal Post-condition (file tests/wp_plugin/model.i, line 13) in 'f':
+Goal Post-condition (file tests/wp_plugin/model.i, line 12) in 'f':
Let x = Mint_0[shift_sint32(p, k)].
Assume {
Type: is_sint32(k) /\ is_sint32(x).
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
index 1174aab59452145b6eda8e73f843ae20a8ce1513..005e353f3645b93e49541f2cc2e122d63877dbdf 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 500 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -8,7 +8,9 @@
[wp] Proved goals: 2 / 2
Qed: 0
Alt-Ergo 2.0.0: 2
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/convert.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/convert.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Lemma - 2 2 100%
+Lemma - 2 (1..12) 2 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/41595c57ce7e98269d53becbfeb7bcb3.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/41595c57ce7e98269d53becbfeb7bcb3.json
new file mode 100644
index 0000000000000000000000000000000000000000..5f72202be45140fd54f9735aeb95dd628189a2fb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/41595c57ce7e98269d53becbfeb7bcb3.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0062,
+ "steps": 7 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/997da10e0a56b9a3ff392e4d0e7b52b7.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/997da10e0a56b9a3ff392e4d0e7b52b7.json
new file mode 100644
index 0000000000000000000000000000000000000000..9c4815d94cdba728365d7ed298f6fe9bfa6d0ed0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.0.session/cache/997da10e0a56b9a3ff392e4d0e7b52b7.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0087,
+ "steps": 7 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
index cf1e24e7a662e3f60447a08cfde4b9fb9cd6d9f8..3dd881b83a080a87062470970a66d63508976476 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/convert.1.res.oracle
@@ -1,11 +1,20 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 500 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/convert.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 2 goals scheduled
-[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_ceil : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_lemma_floor : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_lemma_ceil : Valid
+[wp] [Alt-Ergo (Native)] Goal typed_lemma_floor : Valid
[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo 2.0.0: 2
-[kernel] System error: tests/qualif-why3.report: No such file or directory
+ Qed: 0
+ Alt-Ergo: 2
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/convert.1.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/convert.1.report.json'
+-------------------------------------------------------------
+Axiomatics WP Alt-Ergo Total Success
+Lemma - - (20..32) 2 100%
+-------------------------------------------------------------
+-------------------------------------------------------------
+Axiomatics WP Alt-Ergo (Native) Total Success
+Lemma - 2 (20..32) 2 100%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
index a86ad7dc115ee32e11c03761f33f4cd198468d2e..8569ce3a25eb9a34fa3d72c80219e0aab42f8b97 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/model.res.oracle
@@ -1,6 +1,6 @@
-# frama-c -wp -wp-timeout 100 -wp-steps 500 [...]
+# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/model.i (no preprocessing)
-[kernel] tests/wp_plugin/model.i:11: Warning:
+[kernel] tests/wp_plugin/model.i:10: Warning:
parsing obsolete ACSL construct 'logic declaration'. 'an axiomatic block' should be used instead.
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
@@ -50,7 +50,13 @@ theory Axiomatic
end
[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures : Typechecked
[wp] Proved goals: 0 / 1
- Alt-Ergo 2.0.0: 0 (unknown: 1)
+ Alt-Ergo 2.0.0: 0 (unsuccess: 1)
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/model.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/model.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+f - - 1 0.0%
+-------------------------------------------------------------
[wp] Running WP plugin...
[wp] 2 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_f_ensures : Typechecked
@@ -98,4 +104,10 @@ theory Axiomatic1
end
[wp] [Alt-Ergo 2.0.0] Goal typed_ref_f_ensures : Typechecked
[wp] Proved goals: 0 / 2
- Alt-Ergo 2.0.0: 0 (unknown: 2)
+ Alt-Ergo 2.0.0: 0 (unsuccess: 2)
+[wp] Report in: 'tests/wp_plugin/oracle_qualif/model.0.report.json'
+[wp] Report out: 'tests/wp_plugin/result_qualif/model.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+f - - 2 0.0%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.0.session/cache/4dc341b2d4deefe644f427eea94616b0.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.0.session/cache/4dc341b2d4deefe644f427eea94616b0.json
new file mode 100644
index 0000000000000000000000000000000000000000..16d19ceb388989d8142fd2c2a7248345ad165cd2
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/removed.0.session/cache/4dc341b2d4deefe644f427eea94616b0.json
@@ -0,0 +1 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_plugin/removed.i b/src/plugins/wp/tests/wp_plugin/removed.i
index e865b65ae689e3fc680dfc6ff64320ce00d84e81..dadeb120b00dcd110e99dcd63b1eb270116346e2 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-timeout 100 -wp-steps 500
+ 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
OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
*/