diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex index 3d0330f4f5b5917ddd50e6ab4c77cfed1bbfa1a3..82d7691f3e1c8e13d0054e1314937c891a7ea2af 100644 --- a/src/plugins/wp/doc/manual/wp_plugin.tex +++ b/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: