diff --git a/src/plugins/wp/GuiConfig.ml b/src/plugins/wp/GuiConfig.ml
index 51eb58da11637ed283a1dc370c84aafbeadfe1e2..6e92c3e98ec00f2563539dffde0e9119e458270c 100644
--- a/src/plugins/wp/GuiConfig.ml
+++ b/src/plugins/wp/GuiConfig.ml
@@ -181,7 +181,7 @@ class dp_button ~(available:available) =
| [] -> ERGO
| spec::others ->
match VCS.prover_of_name spec with
- | None | Some (Why3ide|Qed) -> NONE
+ | None | Some Qed -> NONE
| Some (AltErgo|Tactical) -> ERGO
| Some Coq -> COQ
| Some (Why3 s) ->
diff --git a/src/plugins/wp/GuiList.ml b/src/plugins/wp/GuiList.ml
index 19e5a4fdd7ed853316e83b42b7dcbdae2a301329..c9f72fcb75347e219a9100376a3f6afdaeabfc04 100644
--- a/src/plugins/wp/GuiList.ml
+++ b/src/plugins/wp/GuiList.ml
@@ -147,7 +147,7 @@ class pane (enabled:GuiConfig.enabled) =
ignore (list#add_column_text ~title:"Model" [] render) ;
List.iter
self#create_prover
- [ VCS.Qed ; VCS.Tactical ; VCS.AltErgo ; VCS.Coq ; VCS.Why3ide ] ;
+ [ VCS.Qed ; VCS.Tactical ; VCS.AltErgo ; VCS.Coq ] ;
ignore (list#add_column_empty) ;
list#set_selection_mode `MULTIPLE ;
enabled#connect self#configure ;
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 28bb37c4c63cf8326a3e6cb7f56a4a5ff89b67e0..5862f52bcd7d5e69f0583f5e2d73fe1247844ed2 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -239,9 +239,11 @@ class behavior
Task.spawn server thread ;
Task.launch server in
match prover with
+ (*
| VCS.Why3ide ->
let iter f = Wpo.iter ~on_goal:f () in
schedule (ProverWhy3ide.prove ~callback:result ~iter)
+ *)
| VCS.Tactical ->
begin
match mode , ProverScript.get w with
@@ -301,12 +303,12 @@ class behavior
match popup_target with
| Some(w,Some p) -> (popup_target <- None ; self#prove ~mode w p)
| _ -> popup_target <- None
-
+(*
method private popup_why3ide () =
match popup_target with
| Some(w,_) -> (popup_target <- None ; self#prove w VCS.Why3ide)
| _ -> popup_target <- None
-
+*)
method private add_popup_delete popup =
begin
popup#add_separator ;
@@ -331,11 +333,13 @@ class behavior
[ "Run",BatchMode ; "Open Altgr-Ergo on Fail",EditMode ; "Open Altgr-Ergo",EditMode ] ;
self#add_popup_proofmodes popup_coq
[ "Check Proof",BatchMode ; "Edit on Fail",EditMode ; "Edit Proof",EditMode ] ;
+ (*
List.iter
(fun menu ->
menu#add_item ~label:"Open Why3ide" ~callback:self#popup_why3ide ;
self#add_popup_delete menu ;
) [ popup_qed ; popup_why3 ; popup_ergo ; popup_coq ] ;
+ *)
end
method private popup w p =
@@ -344,7 +348,7 @@ class behavior
popup_target <- Some (w,p) ;
match p with
| None | Some Tactical -> popup_tip#run ()
- | Some (Qed|Why3ide) -> popup_qed#run ()
+ | Some Qed -> popup_qed#run ()
| Some Coq -> popup_coq#run ()
| Some AltErgo -> popup_ergo#run ()
| Some (Why3 _) -> popup_why3#run ()
diff --git a/src/plugins/wp/GuiProver.ml b/src/plugins/wp/GuiProver.ml
index 1ed614ee5f2eab4fb5e7a1d5813a17ac5a3caf8c..12301055031fc7542f127790f6edbc1fd4db9b3b 100644
--- a/src/plugins/wp/GuiProver.ml
+++ b/src/plugins/wp/GuiProver.ml
@@ -26,7 +26,7 @@ let ko_status = `Share "theme/default/unknown.png"
let wg_status = `Share "theme/default/invalid.png"
let filter = function
- | VCS.Qed | VCS.Tactical | VCS.Why3ide | VCS.Coq -> false
+ | VCS.Qed | VCS.Tactical | VCS.Coq -> false
| VCS.Why3 _ | VCS.AltErgo -> true
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProverWhy3.ml b/src/plugins/wp/ProverWhy3.ml
index 61230201355a42ea080a7dcd676971d9832c62cf..6c92361439bfb00f0bca1fcd47263e867a96d920 100644
--- a/src/plugins/wp/ProverWhy3.ml
+++ b/src/plugins/wp/ProverWhy3.ml
@@ -392,7 +392,7 @@ let assemble_wpo wpo =
end
| Wpo.Function (kf,_behv) ->
let model = Model.get_model () in
- let file = Wpo.DISK.file_kf ~kf ~model ~prover:VCS.Why3ide in
+ let file = Wpo.DISK.file_kf ~kf ~model ~prover:(VCS.Why3 "") in
let age = try FunFile.find kf with Not_found -> -1 in
begin if age < Wpo.age wpo then
let age_max = ref (-1) in
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index 55503473e6756ac20edb0b964c66418b6cb230f0..a66cdf5321f7905578151da8d263fc024f254772 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -31,7 +31,7 @@ let dkey_success_only = Wp_parameters.register_category "success-only"
type prover =
| Why3 of string (* Prover via WHY *)
- | Why3ide
+ (* | Why3ide *)
| AltErgo (* Alt-Ergo *)
| Coq (* Coq and Coqide *)
| Qed (* Qed Solver *)
@@ -54,16 +54,16 @@ let prover_of_name = function
| "coq" | "coqide" -> Some Coq
| "script" -> Some Tactical
| "tip" -> Some Tactical
- | "why3ide" -> Some Why3ide
+ (* | "why3ide" -> Some Why3ide *)
| s ->
match Extlib.string_del_prefix "why3:" s with
| Some "" -> None
- | Some "ide" -> Some Why3ide
+ (* | Some "ide" -> Some Why3ide*)
| Some s' -> Some (Why3 s')
| None -> Some (Why3 s)
let name_of_prover = function
- | Why3ide -> "why3ide"
+ (* | Why3ide -> "why3ide" *)
| Why3 s -> "why3:" ^ s
| AltErgo -> "alt-ergo"
| Coq -> "coq"
@@ -75,7 +75,7 @@ let title_of_prover = function
| Why3 "z3" -> "Z3"
| Why3 ("alt-ergo" | "altergo") -> "Alt-Ergo (why3)"
| Why3 s -> Printf.sprintf "Why3 (%s)" s
- | Why3ide -> "Why3 (ide)"
+ (* | Why3ide -> "Why3 (ide)" *)
| AltErgo -> "Alt-Ergo"
| Coq -> "Coq"
| Qed -> "Qed"
@@ -102,7 +102,7 @@ let sanitize_why3 s =
let filename_for_prover = function
| Why3 s -> sanitize_why3 s
- | Why3ide -> "Why3_ide"
+ (* | Why3ide -> "Why3_ide" *)
| AltErgo -> "Alt-Ergo"
| Coq -> "Coq"
| Qed -> "Qed"
@@ -110,7 +110,7 @@ let filename_for_prover = function
let language_of_prover = function
| Why3 _ -> L_why3
- | Why3ide -> L_why3
+ (* | Why3ide -> L_why3 *)
| Coq -> L_coq
| AltErgo -> L_altergo
| Qed | Tactical -> L_why3
@@ -128,7 +128,7 @@ let mode_of_prover_name = function
let is_auto = function
| Qed | AltErgo | Why3 _ -> true
- | Tactical | Why3ide | Coq -> false
+ | Tactical | Coq -> false
let cmp_prover p q =
match p,q with
@@ -145,13 +145,9 @@ let cmp_prover p q =
| Coq , _ -> (-1)
| _ , Coq -> 1
| Why3 p , Why3 q -> String.compare p q
- | Why3 _, _ -> (-1)
- | _, Why3 _ -> 1
- | Why3ide, Why3ide -> 0
let pp_prover fmt = function
| AltErgo -> Format.pp_print_string fmt "Alt-Ergo"
- | Why3ide -> Format.pp_print_string fmt "Why3ide"
| Coq -> Format.pp_print_string fmt "Coq"
| Why3 smt ->
if Wp_parameters.debug_atleast 1 then
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 7d9eb27c8d224079b9b15ff9d151f0b8fce7b1fd..fb29085fdb99139307d7e52905a504ffb7e11036 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -28,7 +28,6 @@
type prover =
| Why3 of string (* Prover via WHY *)
- | Why3ide
| AltErgo (* Alt-Ergo *)
| Coq (* Coq and Coqide *)
| Qed (* Qed Solver *)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index f1970bf98877f1dcc5e6182448ce166f374bc115..b20427d8549f8af88dcb751ba51374eb1940ea54 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -988,7 +988,7 @@ controlled by the following options:
(default is: \texttt{1000}).
\end{description}
-\subsection{Decision Procedures Interface}
+\subsection{Prover Selection}
\label{wp-provers}
The generated proof obligations are submitted to external decision
@@ -1103,41 +1103,69 @@ then save the proof scripts in order to replay them in batch mode.
\item[\tt -wp-coq-project='<name>'] override the \verb+_CoqProject+ file name
for Emacs and Proof General.
\end{description}
-
\hrule
-\paragraph{Why3.}
-Since \textsf{WP} version \verb+0.7+ (Fluorine), native support for \textsf{Why3}
-and \textsf{Why3-Ide} are provided. The older system \textsf{Why}
-\verb+2.x+ is \emph{no} longer supported.
+
+\pagebreak
+\paragraph{Why-3.}
+Native support for \textsf{Why-3} is provided (for versions 1.0 and newer).
+\\
+Support for \textsf{Why-3 IDE} is no longer provided.
\begin{description}
-\item[\tt -wp-prover "why3ide"] runs \textsf{Why3-Ide} with all
- generated goals. On exit, the \textsf{WP} plug-in reads back your
- \textsf{Why3} session and updates the proof obligation status accordingly.
-\item[\tt -wp-prover "<p>"] runs a \textsf{Why3} prover named \texttt{<p>}.
-\item[\tt -wp-prover "why3:<p>"] useful alias when \texttt{"<p>"} can
- be ambiguous. It is actually different to run \texttt{alt-ergo} or \texttt{coq}
- directly from \textsf{WP} or through \textsf{Why3}.
-\item[\tt -wp-detect] lists the provers available with \textsf{Why3}.
- This command calls \texttt{why3 --list-provers} but you have to
- configure \textsf{Why3} on your own before, for instance by using
- \texttt{why3config}. Consult the \textsf{Why3} user manual for details.
- The listed prover names can be directly used with the \texttt{-wp-prover} option.
-\item[\tt -wp-why3='<cmd>'] override the \verb+why3+ command.
+\item[\tt -wp-prover "why3:<p>"] runs a \textsf{Why-3} prover named \texttt{<p>}, and
+ exactly behaves like invoking \verb+why3 prover -P <p>+. The list of prover
+ names \verb+<p>+ must be extracted from the \verb+[alias]+ section of your \textsf{Why-3}
+ configuration, which \verb+frama-c -wp-detect+ does for you (see below).
+\item[\tt -wp-prover "<p>"] can also be used instead of \verb+-wp-prover "why3:<p>"+
+ when \verb+<p>+ is not natively supported by \textsf{WP}, like \texttt{alt-ergo},
+ \texttt{altgr-ergo}, \texttt{coq}, \texttt{coqide}, \texttt{script} and \texttt{tip}.
+\item[\tt -wp-detect] lists the provers available for \textsf{Why-3}.
+ This command can only work if \textsf{why3} API was installed before building and
+ installing \textsf{Frama-C}.
+ The option reads your \textsf{Why-3} configuration and prints the available
+ provers with their \verb+-wp-prover <p>+ code names.
+\item[\tt -wp-why3='<cmd>'] overrides the path to the \verb+why3+ command.
\end{description}
-\paragraph{Sessions.}
-Your \textsf{Why3} session is saved in the \texttt{"project.session"}
-sub-directory of \texttt{-wp-out}. You may run
-\texttt{why3ide} by hand by issuing the following command:
-\begin{shell}
-# why3ide -I <frama-c-share>/wp <out>/project.session
-\end{shell}
+\paragraph{Example of using Why-3.}
+Suppose you have the following configuration:
+
+\begin{logs}
+# frama-c -wp-detect
+[wp] Why3 provers detected:
+ - Alt-Ergo 2.0.0 [why3:alt-ergo,altergo]
+ - CVC4 1.6 [cvc4]
+ - CVC4 1.6 (counterexamples) [cvc4-ce]
+ - Coq 8.9.0 [why3:coq]
+ - Z3 4.6.0 [z3]
+ - Z3 4.6.0 (counterexamples) [z3-ce]
+ - Z3 4.6.0 (noBV) [z3-nobv]
+\end{logs}
-Proof recovering features of \textsf{Why3} are fully available, and
-you can interleave proving from \textsf{WP} with manual runs of
-\texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
-separated from those managed by the native \textsf{WP} interface with
-\textsf{Coq}.
+Then, to use (for instance) \textsf{CVC4 1.6},
+you can use \verb+-wp-prover cvc4+ (since this name is not conflicting
+with any native prover). Alternatively, you can also use the less ambiguous
+name \verb+-wp-prover why3:cvc4+ if you prefer.
+Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use \verb+-wp-prover z3-nobv+
+or \verb+-wp-prover why3:z3-nobv+.
+
+However, to use \textsf{Alt-Ergo 2.0.0} \emph{via} \textsf{Why-3}, you shall use
+\verb+-wp-prover why3:alt-ergo+, since \verb+-wp-prover alt-ergo+ would select
+the native support of \textsf{Alt-Ergo} prover. Finally, since \textsf{Why-3} also provides the alias
+\verb+altergo+ for this prover, \verb+-wp-prover altergo+ will also run it \emph{via} \textsf{Why-3}.
+
+%% \paragraph{Sessions.}
+%% Your \textsf{Why3} session is saved in the \texttt{"project.session"}
+%% sub-directory of \texttt{-wp-out}. You may run
+%% \texttt{why3ide} by hand by issuing the following command:
+%% \begin{shell}
+%% # why3ide -I <frama-c-share>/wp <out>/project.session
+%% \end{shell}
+
+%% Proof recovering features of \textsf{Why3} are fully available, and
+%% you can interleave proving from \textsf{WP} with manual runs of
+%% \texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
+%% separated from those managed by the native \textsf{WP} interface with
+%% \textsf{Coq}.
\subsection{Generated Proof Obligations}
Your proof obligations are generated and saved to several text
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index bc18054056ee79ce17a0b201df3c98f2e3c78cb5..530e74c3d0f64be6e5b0fe16ba8c15cc93921d70 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -36,7 +36,6 @@ let dispatch ?(config=VCS.default) mode prover wpo =
| Coq -> ProverCoq.prove mode wpo
| Why3 prover -> ProverWhy3.prove ?timeout:config.timeout ~prover wpo
| Qed | Tactical -> Task.return VCS.no_result
- | _ -> Task.failed "Prover '%a' not available" VCS.pp_prover prover
end
let started ?start wpo =
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index ad824c977d63875b53b78de4814e3d564ae4d038..f17abda0620a3a385be354a642079943e11a644a 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -513,8 +513,10 @@ let compute_provers ~mode =
(fun pname prvs ->
match VCS.prover_of_name pname with
| None -> prvs
+ (*
| Some VCS.Why3ide ->
mode.why3ide <- true; prvs
+ *)
| Some VCS.Tactical ->
mode.tactical <- true ;
if pname = "tip" then mode.update <- true ;
@@ -626,8 +628,10 @@ let do_wp_proofs_iter iter =
let spawned = mode.why3ide || mode.tactical || mode.provers <> [] in
begin
if spawned then do_list_scheduled iter ;
+ (*
if mode.why3ide then
launch (ProverWhy3ide.prove ~callback:do_why3_result ~iter) ;
+ *)
spawn_wp_proofs_iter ~mode iter ;
if spawned then
begin
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test.ml b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
index 320ad154cdac77a26b1768685510442f460ebc05..ae5dcae5a7fcbf01f1c728a8947e98dc0deb6944 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test.ml
@@ -24,7 +24,7 @@ let run () =
List.fold_right
(fun pname prvs -> match VCS.prover_of_name pname with
| None -> prvs
- | Some VCS.Why3ide | Some VCS.Tactical -> prvs
+ | Some VCS.Tactical -> prvs
| Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
["qed"] []
in
diff --git a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
index a10fb172d38336400c6fc3eb46e0ca9acd6f0916..ae0f98a6d4a7abfcd196df32c00668ce32545ea7 100644
--- a/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
+++ b/src/plugins/wp/tests/wp/stmtcompiler_test_rela.ml
@@ -23,7 +23,7 @@ let run () =
List.fold_right
(fun pname prvs -> match VCS.prover_of_name pname with
| None -> prvs
- | Some VCS.Why3ide | Some VCS.Tactical -> prvs
+ | Some VCS.Tactical -> prvs
| Some prv -> (VCS.mode_of_prover_name pname, prv) :: prvs)
["alt-ergo"] []
in
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 782b9a5425dfb48bfc7d165900d6733b75a2b27b..90d1fd2dbd29a70d99de4594de954babd0ef4af6 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -109,7 +109,6 @@ struct
| Qed -> "qed"
| AltErgo -> "mlw"
| Why3 _ -> "why"
- | Why3ide -> "why"
| Coq -> "v"
| Tactical -> "tac"
in
@@ -121,7 +120,6 @@ struct
| Qed -> "qed"
| AltErgo -> "mlw"
| Why3 _ -> "why"
- | Why3ide -> "why"
| Coq -> "v"
| Tactical -> "tac"
in
@@ -539,7 +537,7 @@ struct
match r.verdict with VCS.Computing _ -> false | _ -> true
let class_of_prover = function
- | Qed | Tactical | AltErgo | Coq | Why3ide -> None
+ | Qed | Tactical | AltErgo | Coq -> None
| Why3 dp ->
let cp =
try String.sub dp 0 (String.index dp ':')