[wp] remove obsolete prover-why3

headers/header_spec.txt

@@ -1442,8 +1442,6 @@ src/plugins/wp/ProverSearch.ml: CEA_WP
 src/plugins/wp/ProverSearch.mli: CEA_WP
 src/plugins/wp/ProverTask.ml: CEA_WP
 src/plugins/wp/ProverTask.mli: CEA_WP
-src/plugins/wp/ProverWhy3.ml: CEA_WP
-src/plugins/wp/ProverWhy3.mli: CEA_WP
 src/plugins/wp/REVISION: .ignore
 src/plugins/wp/RefUsage.ml: CEA_WP
 src/plugins/wp/RefUsage.mli: CEA_WP

src/plugins/wp/ProverWhy3.mli

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of WP plug-in of Frama-C.                           *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2019                                               *)
-(*    CEA (Commissariat a l'energie atomique et aux energies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Task
-open VCS
-
-(* -------------------------------------------------------------------------- *)
-(* --- Why3 Multi-Theorem Prover                                          --- *)
-(* -------------------------------------------------------------------------- *)
-
-type goal =
-  {
-    file : string;
-    theory : string;
-    goal : string;
-  }
-
-val assemble_goal: Wpo.t -> (string list (* includes *) * goal) option
-(** None if the po is trivial *)
-
-val prove : ?timeout:int -> prover:Why3.Whyconf.prover -> Wpo.t -> result task
-(** The string must be a valid why3 prover identifier
-    Return NoResult if it is already proved by Qed
-*)
-(* -------------------------------------------------------------------------- *)
-(* --- Why3 Multi-Theorem Prover                                          --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Goal :
-sig
-  type t = goal
-  val compare : t -> t -> int
-  val pretty : Format.formatter -> t -> unit
-end
-
-
-val option_file: LogicBuiltins.doption
-val option_import: LogicBuiltins.doption
-
-(* -------------------------------------------------------------------------- *)

src/plugins/wp/prover.ml

@@ -38,9 +38,9 @@ let dispatch ?(config=VCS.default) mode prover wpo =
   in
   begin
     match prover with
+    | Why3 prover -> why3 prover
     | NativeAltErgo -> ProverErgo.prove ~config ~mode wpo
     | NativeCoq -> ProverCoq.prove mode wpo
-    | Why3 prover -> why3 prover
     | Qed | Tactical -> Task.return VCS.no_result
   end