Merge branch 'feature/wp/run-all-provers' into 'master'

Run all provers option

See merge request frama-c/frama-c!2469

src/plugins/wp/Changelog

@@ -20,6 +20,8 @@
 #   <Prover>: prover
 ###############################################################################
 
+- WP          [2019/12/04] Added option -wp-run-all-provers
+
 ##########################
 Plugin WP 20.0 (Calcium)
 ##########################

src/plugins/wp/ProverTask.ml

@@ -320,7 +320,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 then
+          begin if not !canceled && not (Wp_parameters.RunAllProvers.get()) then
               begin
                 canceled := true ;
                 monitor (Some a) ;

src/plugins/wp/doc/manual/wp_plugin.tex

@@ -995,6 +995,9 @@ Support for \textsf{Why-3 IDE} is no longer provided.
   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-(no)-run-all-provers] Run all specified provers on each goal not
+  proved by Qed. When a prover succeeds in proving the goal, the others are not
+  stopped. (default is: no).
 \item[\tt -wp-gen] only generates proof obligations, does not run provers.
   See option \texttt{-wp-out} to obtain the generated proof obligations.
 \item[\tt -wp-par <n>] limits the number of parallel process runs for
@@ -1241,7 +1244,7 @@ interactively or incrementally, it is often the case where most proof obligation
 from one \textsf{WP} execution to the other. To reduce this costs, a cache of prover results can be used
 and stored in your session.
 
-% The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers. 
+% The cache can only be used with \textsf{Why-3} provers, it does not work with native \textsf{Alt-Ergo} and \textsf{Coq} provers.
 There are different ways of using the cache, depending on your precise needs.
 The main option to control cache usage is \verb+-wp-cache+, documented below:
 

src/plugins/wp/wp_parameters.ml

@@ -567,6 +567,14 @@ module Provers = String_list
         "
     end)
 
+let () = Parameter_customize.set_group wp_prover
+module RunAllProvers =
+  False(struct
+    let option_name = "-wp-run-all-provers"
+    let help = "Run all specified provers on each goal not proved by Qed. \
+                Do not stop when a prover succeeds. (default: no)"
+  end)
+
 let () = Parameter_customize.set_group wp_prover
 module Cache = String
     (struct

src/plugins/wp/wp_parameters.mli

@@ -105,6 +105,7 @@ module PrecondWeakening : Parameter_sig.Bool
 module Detect: Parameter_sig.Bool
 module Generate:Parameter_sig.Bool
 module Provers: Parameter_sig.String_list
+module RunAllProvers: Parameter_sig.Bool
 module Cache: Parameter_sig.String
 module Drivers: Parameter_sig.String_list
 module Script: Parameter_sig.String