diff --git a/src/plugins/wp/GuiList.ml b/src/plugins/wp/GuiList.ml
index 2187eebd8fb069c96669ee8221314ea47178297b..17d2f761fce3d0b0203071e2d2d0ba99fc66f515 100644
--- a/src/plugins/wp/GuiList.ml
+++ b/src/plugins/wp/GuiList.ml
@@ -52,7 +52,7 @@ let render_prover_result p =
let icn_running = icn_stock "gtk-execute" in
let open VCS in
let icon_of_verdict = function
- | Checked | NoResult -> icn_none
+ | NoResult -> icn_none
| Valid -> icn_valid
| Invalid -> icn_invalid
| Unknown -> icn_unknown
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index c74179056de2168a65eeb510ea8f241ef86fc42b..eec80f957002a65c8570297a0f659c8f5e52fac7 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -125,7 +125,7 @@ class prover ~(console:Wtext.text) ~prover =
self#set_status `EXECUTE ;
self#set_action ~tooltip:"Interrrupt Prover" ~icon:`STOP ~callback () ;
Pretty_utils.ksfprintf self#set_label "%a (...)" VCS.pp_prover prover ;
- | VCS.Valid | VCS.Checked ->
+ | VCS.Valid ->
let callback () = self#run wpo in
self#set_status ok_status ;
self#set_action ~tooltip:"Run Prover" ~icon:`MEDIA_PLAY ~callback () ;
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index a7b3155076a91558a47d2f88fba993dedbfe003b..73c77b5b71d37ffa4fbb17639893672e2e17a7e6 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -316,7 +316,7 @@ let tactic_of_json js =
(* -------------------------------------------------------------------------- *)
let json_of_verdict = function
- | VCS.NoResult | VCS.Checked | VCS.Computing _ -> `String "none"
+ | VCS.NoResult | VCS.Computing _ -> `String "none"
| VCS.Valid -> `String "valid"
| VCS.Unknown -> `String "unknown"
| VCS.Timeout -> `String "timeout"
diff --git a/src/plugins/wp/ProverCoq.ml b/src/plugins/wp/ProverCoq.ml
index 2313a5ba1117fd4cacfcbd59a0e10aa9ebf63f78..446fceadc1b41cdb2535aa24fab4ef83316af348 100644
--- a/src/plugins/wp/ProverCoq.ml
+++ b/src/plugins/wp/ProverCoq.ml
@@ -435,10 +435,9 @@ class runcoq includes source =
self#timeout (coq_timeout ()) ;
Task.call
(fun () ->
- if not (Wp_parameters.Check.get ()) then
- let name = Filename.basename source in
- Wp_parameters.feedback ~ontty:`Transient
- "[Coq] Compiling '%s'." name) ()
+ let name = Filename.basename source in
+ Wp_parameters.feedback ~ontty:`Transient
+ "[Coq] Compiling '%s'." name) ()
>>= self#run ~logout ~logerr
>>= fun r ->
if r = 127 then Task.failed "Command '%s' not found" cmd
@@ -523,13 +522,6 @@ type coq_wpo = {
cw_includes : included list ; (* -R ... ... *)
}
-let make_check w =
- Command.print_file w.cw_script
- begin fun fmt ->
- Command.pp_from_file fmt w.cw_goal ;
- Format.fprintf fmt "Proof.@\nAdmitted.@\n@." ;
- end
-
let make_script w script closing =
Command.print_file w.cw_script
begin fun fmt ->
@@ -541,10 +533,6 @@ let try_script w script closing =
make_script w script closing ;
(new runcoq w.cw_includes w.cw_script)#check
-let check_script w =
- make_check w ;
- (new runcoq w.cw_includes w.cw_script)#check
-
let rec try_hints w = function
| [] -> Task.return false
| (kind,script,closing) :: hints ->
@@ -618,8 +606,6 @@ let prove_session ~mode w =
end
>>= Task.call (fun r -> if r then VCS.valid else VCS.unknown)
-exception Admitted_not_proved
-
let gen_session w =
begin
make_script w " ...\n" "Qed." ;
@@ -627,19 +613,9 @@ let gen_session w =
Task.return VCS.no_result
end
-let check_session w =
- compile_headers w.cw_includes false w.cw_headers >>=
- (fun () -> check_script w) >>> function
- | Task.Result true -> Task.return VCS.checked
- | Task.Failed e -> Task.raised e
- | Task.Canceled | Task.Timeout _ | Task.Result false ->
- Task.raised Admitted_not_proved
-
let prove_session ~mode w =
if Wp_parameters.Generate.get () then
gen_session w
- else if Wp_parameters.Check.get () then
- check_session w
else
prove_session ~mode w
diff --git a/src/plugins/wp/ProverErgo.ml b/src/plugins/wp/ProverErgo.ml
index 8aa0d51c86a9951765ec593afe0680df58c14916..9ad747a9afb3196f58a6a8712e520b6d7a873866 100644
--- a/src/plugins/wp/ProverErgo.ml
+++ b/src/plugins/wp/ProverErgo.ml
@@ -396,37 +396,21 @@ class altergo ~config ~pid ~gui ~file ~lines ~logout ~logerr =
VCS.result
~time:(if gui then 0.0 else timer)
~steps verdict
- with
- | Not_found when Wp_parameters.Check.get () ->
- if r = 0 then VCS.checked
- else
- begin
- if Wp_parameters.verbose_atleast 1 then begin
- ProverTask.pp_file ~message:"Alt-Ergo (stdout)" ~file:logout ;
- ProverTask.pp_file ~message:"Alt-Ergo (stderr)" ~file:logerr ;
- end;
- VCS.failed "Alt-Ergo type-checking failed."
- end
- | Not_found ->
- begin
- if Wp_parameters.verbose_atleast 1 then begin
- ProverTask.pp_file ~message:"Alt-Ergo (stdout)" ~file:logout ;
- ProverTask.pp_file ~message:"Alt-Ergo (stderr)" ~file:logerr ;
- end;
- if r = 0 then VCS.failed "Unexpected Alt-Ergo output"
- else VCS.kfailed "Alt-Ergo exits with status [%d]." r
- end
+ with Not_found ->
+ begin
+ if Wp_parameters.verbose_atleast 1 then begin
+ ProverTask.pp_file ~message:"Alt-Ergo (stdout)" ~file:logout ;
+ ProverTask.pp_file ~message:"Alt-Ergo (stderr)" ~file:logerr ;
+ end;
+ if r = 0 then VCS.failed "Unexpected Alt-Ergo output"
+ else VCS.kfailed "Alt-Ergo exits with status [%d]." r
+ end
method prove =
files <- lines ;
if gui then ergo#set_command (Wp_parameters.AltGrErgo.get ()) ;
- if Wp_parameters.Check.get () then
- ergo#add ["-type-only"]
- else
- begin
- ergo#add_parameter ~name:"-proof" Wp_parameters.ProofTrace.get ;
- ergo#add_parameter ~name:"-model" Wp_parameters.ProofTrace.get ;
- end ;
+ ergo#add_parameter ~name:"-proof" Wp_parameters.ProofTrace.get ;
+ ergo#add_parameter ~name:"-model" Wp_parameters.ProofTrace.get ;
let flags = List.filter
(fun p -> p <> "qlet")
(Wp_parameters.AltErgoFlags.get ()) in
diff --git a/src/plugins/wp/ProverTask.ml b/src/plugins/wp/ProverTask.ml
index ff94ff83913efe8501a727709571dc8976991043..c1c45be5d62bba655bacdcc1b17665ad4c7ca5ad 100644
--- a/src/plugins/wp/ProverTask.ml
+++ b/src/plugins/wp/ProverTask.ml
@@ -28,7 +28,6 @@ open Task
let dkey_prover = Wp_parameters.register_category "prover"
-
(* -------------------------------------------------------------------------- *)
(* --- Export Printer --- *)
(* -------------------------------------------------------------------------- *)
@@ -315,7 +314,8 @@ let schedule task =
Task.spawn server (Task.thread task)
let silent _ = ()
-let spawn ?(monitor=silent) ?pool (jobs : ('a * bool Task.task) list) =
+let spawn ?(monitor=silent) ?pool ~all
+ (jobs : ('a * bool Task.task) list) =
if jobs <> [] then
begin
let step = ref 0 in
@@ -323,7 +323,7 @@ let spawn ?(monitor=silent) ?pool (jobs : ('a * bool Task.task) list) =
let canceled = ref false in
let callback a r =
if r then
- begin if not !canceled && not (Wp_parameters.RunAllProvers.get()) then
+ begin if not all && not !canceled then
begin
canceled := true ;
monitor (Some a) ;
diff --git a/src/plugins/wp/ProverTask.mli b/src/plugins/wp/ProverTask.mli
index a585b37e0d507af82f3fc5e76777a628efe023a3..4f0bc09934e924175358840fe95a8bc3cb697930 100644
--- a/src/plugins/wp/ProverTask.mli
+++ b/src/plugins/wp/ProverTask.mli
@@ -85,8 +85,10 @@ val schedule : 'a Task.task -> unit
val spawn :
?monitor:('a option -> unit) ->
?pool:Task.pool ->
+ all:bool ->
('a * bool Task.task) list -> unit
+
(** Spawn all the tasks over the server and retain the first 'validated' one.
The callback [monitor] is called with [Some] at first success, and [None]
- if none succeed.
- An option [pool] task can be passed to register the associated threads. *)
+ if none succeed. An option [pool] task can be passed to register
+ the associated threads. *)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 7f1b75155612e1354543f1ed4626cb21d41d0424..b4074ed1bb1b9f989a06f9e145794ec2aee52a6c 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -1338,7 +1338,7 @@ let steps_seized steps steplimit =
let promote ~timeout ~steplimit (res : VCS.result) =
match res.verdict with
- | VCS.NoResult | VCS.Computing _ | VCS.Checked -> VCS.no_result
+ | VCS.NoResult | VCS.Computing _ -> VCS.no_result
| VCS.Failed -> res
| VCS.Invalid | VCS.Valid | VCS.Unknown ->
if not (steps_fits res.prover_steps steplimit) then
@@ -1404,9 +1404,6 @@ let build_proof_task ?timeout ?steplimit ~prover wpo () =
(* Always generate common task *)
let context = Wpo.get_context wpo in
let task = WpContext.on_context context task_of_wpo wpo in
- if Wp_parameters.Check.get ()
- then Task.return VCS.checked (* Why3 tasks are type-checked *)
- else
if Wp_parameters.Generate.get ()
then Task.return VCS.no_result (* Only generate *)
else
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index db0cb3b658414c06416f3db62e8175d14ad769b7..57a3b380532de56912efee0266b89e7686af6f38 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -194,7 +194,6 @@ type verdict =
| Timeout
| Stepout
| Computing of (unit -> unit) (* kill function *)
- | Checked
| Valid
| Failed
@@ -209,7 +208,7 @@ type result = {
}
let is_verdict r = match r.verdict with
- | Valid | Checked | Unknown | Invalid | Timeout | Stepout | Failed -> true
+ | Valid | Unknown | Invalid | Timeout | Stepout | Failed -> true
| NoResult | Computing _ -> false
let is_valid = function { verdict = Valid } -> true | _ -> false
@@ -276,7 +275,6 @@ let result ?(cached=false) ?(solver=0.0) ?(time=0.0) ?(steps=0) verdict =
let no_result = result NoResult
let valid = result Valid
-let checked = result Checked
let invalid = result Invalid
let unknown = result Unknown
let timeout t = result ~time:(float t) Timeout
@@ -317,7 +315,6 @@ let pp_res ~extended fmt r =
match r.verdict with
| NoResult -> Format.pp_print_string fmt (if extended then "No Result" else "-")
| Computing _ -> Format.pp_print_string fmt "Computing"
- | Checked -> Format.fprintf fmt "Typechecked"
| Invalid -> Format.pp_print_string fmt "Invalid"
| Valid when Wp_parameters.has_dkey dkey_success_only ->
Format.pp_print_string fmt "Valid"
@@ -340,7 +337,6 @@ let compare p q =
| Timeout | Stepout -> 3
| Valid -> 4
| Invalid -> 5
- | Checked -> 6
in
let r = rank q.verdict - rank p.verdict in
if r <> 0 then r else
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index dae1064fb0193d38be30c6ea79a6703160110a66..6f37aab30d325c087aed06bd1a7f19eb5e800cbd 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -80,7 +80,6 @@ type verdict =
| Timeout
| Stepout
| Computing of (unit -> unit) (* kill function *)
- | Checked
| Valid
| Failed
@@ -96,7 +95,6 @@ type result = {
val no_result : result
val valid : result
-val checked : result
val invalid : result
val unknown : result
val stepout : int -> result
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 59e5e5497e988ef267c4b24d1047d6dac4ea5204..78092c65d91230a40272035b3714575a84da6e1a 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -97,27 +97,28 @@ let prove wpo ?config ?mode ?start ?progress ?result prover =
let spawn wpo ~delayed
?config ?start ?progress ?result ?success ?pool provers =
if provers<>[] then
- let do_monitor on_success wpo = function
- | None -> on_success wpo None
- | Some prover ->
- let r = Wpo.get_result wpo VCS.Qed in
- let prover =
- if VCS.( r.verdict == Valid ) then VCS.Qed else prover in
- on_success wpo (Some prover)
- in
let monitor = match success with
| None -> None
- | Some on_success -> Some (do_monitor on_success wpo)
- in
+ | Some on_success ->
+ Some
+ begin function
+ | None -> on_success wpo None
+ | Some prover ->
+ let r = Wpo.get_result wpo VCS.Qed in
+ let prover =
+ if VCS.( r.verdict == Valid ) then VCS.Qed else prover in
+ on_success wpo (Some prover)
+ end in
let process (mode,prover) =
prove wpo ?config ~mode ?start ?progress ?result prover in
- let canceled =
- match success with None -> None | Some f -> Some (fun _ -> f wpo None) in
- ProverTask.spawn ?monitor ?pool
- (List.map (fun mp -> snd mp ,
- if delayed then Task.later ?canceled process mp
- else process mp)
- provers)
+ let all = Wp_parameters.RunAllProvers.get() in
+ ProverTask.spawn ?monitor ?pool ~all
+ (List.map
+ (fun mp ->
+ let prover = snd mp in
+ let task = if delayed then Task.later process mp else process mp in
+ prover , task
+ ) provers)
else
let process = simplify ?start ?result wpo in
let thread = Task.thread process in
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 509dbcb3e7b582fa822dc615dc4d4cf3802d41c0..bb74fcb202c8fec48019a0470cc5b149210a9eaa 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -351,7 +351,7 @@ let do_wpo_stat goal prover res =
let smoke = Wpo.is_smoke_test goal in
let verdict = VCS.verdict ~smoke res in
match verdict with
- | Checked | NoResult | Computing _ | Unknown ->
+ | NoResult | Computing _ | Unknown ->
s.unknown <- succ s.unknown
| Stepout | Timeout ->
s.interrupted <- succ s.interrupted
@@ -369,15 +369,6 @@ let do_wpo_stat goal prover res =
let do_wpo_result goal prover res =
if VCS.is_verdict res then
begin
- if Wp_parameters.Check.get () then
- begin
- let open VCS in
- let ontty = if res.verdict = Checked then `Feedback else `Message in
- Wp_parameters.feedback ~ontty
- "[%a] Goal %s : %a"
- VCS.pp_prover prover (Wpo.get_gid goal)
- VCS.pp_result res ;
- end ;
if prover = VCS.Qed then do_progress goal "Qed" ;
do_wpo_stat goal prover res ;
end
diff --git a/src/plugins/wp/tests/wp_plugin/bit_test.c b/src/plugins/wp/tests/wp_plugin/bit_test.c
index b0b19bf9b8c72db53bc2885dc90e402987c6cb08..96f24adfa142c51f5be4046ccd5abddc23671f08 100644
--- a/src/plugins/wp/tests/wp_plugin/bit_test.c
+++ b/src/plugins/wp/tests/wp_plugin/bit_test.c
@@ -3,7 +3,7 @@
*/
/* run.config_qualif
- OPT: -wp-driver tests/wp_plugin/bit_test.driver -wp-prover why3:alt-ergo -wp-check
+ OPT: -wp-driver tests/wp_plugin/bit_test.driver -wp-prover why3:alt-ergo
*/
/*@
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 4b57d2f03e09e31030018d51fd55a39abec3216b..81b49ed20d473590181d159b37f404a4564e5395 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -4,7 +4,7 @@
*/
/* run.config_qualif
- OPT: -wp-msg-key print-generated -wp-model Typed -wp-check -then -wp -wp-model Typed+ref -wp-check
+ OPT: -wp-msg-key print-generated -wp-model Typed -then -wp -wp-model Typed+ref
*/
//@ predicate P(integer a);
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
index 6ee9e8566582a39abf57d083d4198404b1643284..f6a082b42cc33bbd5b6ac2c421762b4aea213966 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
@@ -4,9 +4,9 @@
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
-[wp] [Alt-Ergo] Goal typed_bit_test_check1_ensures_ko : Typechecked
-[wp] [Alt-Ergo] Goal typed_bit_test_check2_ensures_ko : Typechecked
-[wp] [Alt-Ergo] Goal typed_bit_test_check3_ensures_ko : Typechecked
+[wp] [Alt-Ergo] Goal typed_bit_test_check1_ensures_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bit_test_check2_ensures_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_bit_test_check3_ensures_ko : Unsuccess
[wp] Proved goals: 0 / 3
Alt-Ergo: 0 (unsuccess: 3)
------------------------------------------------------------
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 43185ba1c3656c14646138ccf74ce2429e2ce6c6..45defe11c252e1fdb22342768b34b459e48ce881 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
@@ -77,7 +77,7 @@ end
let x = get t (shift_sint32 a i) in
region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
end
-[wp] [Alt-Ergo] Goal typed_f_ensures : Typechecked
+[wp] [Alt-Ergo] Goal typed_f_ensures : Unsuccess
[wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1)
------------------------------------------------------------
@@ -115,7 +115,7 @@ end
let x = get t (shift_sint32 a i) in
region (base a) <= 0 -> is_sint32 i -> is_sint32 x -> P_P x
end
-[wp] [Alt-Ergo] Goal typed_f_ensures : Typechecked
+[wp] [Alt-Ergo] Goal typed_f_ensures : Unsuccess
---------------------------------------------
--- Context 'typed_ref_f' Cluster 'Compound'
---------------------------------------------
@@ -187,7 +187,7 @@ end
let x = get1 t (shift_sint321 a i) in
region1 (base1 a) <=' 0 -> is_sint321 i -> is_sint321 x -> P_P1 x
end
-[wp] [Alt-Ergo] Goal typed_ref_f_ensures : Typechecked
+[wp] [Alt-Ergo] Goal typed_ref_f_ensures : Unsuccess
[wp] Proved goals: 0 / 2
Alt-Ergo: 0 (unsuccess: 2)
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/rte.i b/src/plugins/wp/tests/wp_plugin/rte.i
index 1b63b3768c83f5e7f9f053f2bf203a2a879e0851..65e8988e572951b8de7ff768207b7c4e88fdfa86 100644
--- a/src/plugins/wp/tests/wp_plugin/rte.i
+++ b/src/plugins/wp/tests/wp_plugin/rte.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp -wp-prover none -wp-check -wp-share ./share -wp-msg-key shell -wp-msg-key rte
+ CMD: @frama-c@ -wp -wp-prover none -wp-share ./share -wp-msg-key shell -wp-msg-key rte
OPT: -wp-rte -no-warn-invalid-bool -then -print -no-unicode
OPT: -wp-rte -no-warn-signed-overflow -then -print -no-unicode
OPT: -wp-rte -warn-unsigned-overflow -then -print -no-unicode
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index 219694d2e8f0dc6aa4ca8ac2f483363d67b3e970..630ee22a7c0fbbb51949b9e9c0d396ac59c3b013 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -992,16 +992,6 @@ module OutputDir =
Defaults to some temporary directory."
end)
-let () = Parameter_customize.set_group wp_po
-let () = Parameter_customize.do_not_save ()
-module Check =
- Action(struct
- let option_name = "-wp-check"
- let help =
- "Check the syntax and type of the produced file, instead of proving."
- end)
-let () = on_reset Print.clear
-
(* -------------------------------------------------------------------------- *)
(* --- Overflows --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index af829e5f8a25afdb231df07af0bf601ccca86593..2d763525c655e7c69d4cf1652953ee0335537fff 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -146,7 +146,6 @@ module Report: Parameter_sig.String_list
module ReportJson: Parameter_sig.String
module ReportName: Parameter_sig.String
module MemoryContext: Parameter_sig.Bool
-module Check: Parameter_sig.Bool
module SmokeTests: Parameter_sig.Bool
(** {2 Getters} *)