From 5a9828530ca60c1dbee4bcd77fbb804818961ecf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 21 Sep 2020 13:12:50 +0200
Subject: [PATCH] [wp] added documentation
---
src/plugins/wp/Changelog | 3 +
src/plugins/wp/doc/manual/wp.bib | 33 +++++++++++
src/plugins/wp/doc/manual/wp_plugin.tex | 65 +++++++--------------
src/plugins/wp/doc/manual/wp_simplifier.tex | 10 ----
4 files changed, 56 insertions(+), 55 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 389007c7c91..51c39384588 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,9 @@
Plugin WP <next-release>
#########################
+- WP [2020-09-21] Added support for Why3 Coq interactive prover
+- WP [2020-09-21] New option -wp-interactive <mode>
+- WP [2020-09-21] New option -wp-interactive-timeout <seconds>
- WP [2020-09-17] New experimental option: -wp-check-model-hypotheses
Generates requires in contracts for model hypotheses
- WP [2020-09-17] Hypotheses: assigned memory locations
diff --git a/src/plugins/wp/doc/manual/wp.bib b/src/plugins/wp/doc/manual/wp.bib
index bcc4524f29d..cbe190e5609 100644
--- a/src/plugins/wp/doc/manual/wp.bib
+++ b/src/plugins/wp/doc/manual/wp.bib
@@ -98,6 +98,39 @@
url = {http://ergo.lri.fr/papers/ergo.ps}
}
+@inproceedings{CVC4,
+ url = "http://www.cs.stanford.edu/~barrett/pubs/BCD+11.pdf",
+ author = "Clark Barrett and Christopher L. Conway and Morgan Deters and
+ Liana Hadarean and Dejan Jovanovi{'{c}} and Tim King and
+ Andrew Reynolds and Cesare Tinelli",
+ title = "{CVC4}",
+ booktitle = "Proceedings of the 23rd International Conference on Computer Aided Verification (CAV '11)",
+ series = "Lecture Notes in Computer Science",
+ volume = 6806,
+ publisher = "Springer",
+ editor = "Ganesh Gopalakrishnan and Shaz Qadeer",
+ pages = "171--177",
+ month = jul,
+ year = 2011,
+ note = "Snowbird, Utah",
+ category = "Conference Publications"
+}
+
+@InProceedings{Z3,
+author="de Moura, Leonardo
+and Bj{\o}rner, Nikolaj",
+editor="Ramakrishnan, C. R.
+and Rehof, Jakob",
+title="Z3: An Efficient SMT Solver",
+booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
+year="2008",
+publisher="Springer Berlin Heidelberg",
+address="Berlin, Heidelberg",
+pages="337--340",
+abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.",
+isbn="978-3-540-78800-3"
+}
+
@inproceedings{qed,
author = {Lo{\"{\i}}c Correnson},
title = {Qed. Computing What Remains to Be Proved},
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 3e343ef02f7..e565b465840 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -10,51 +10,13 @@ This plug-in computes proof obligations of programs annotated with
\textsf{ACSL} annotations by \emph{weakest precondition calculus},
using a parametrized memory model to represent pointers and heap
values. The proof obligations may then be discharged by external
-decision procedures, which range over automated theorem provers such
-as \textsf{Alt-Ergo}~\cite{AltErgo2006}, interactive proof assistants
-like \textsf{Coq}~\cite{Coq84} and the interactive proof manager
-\textsf{Why3}~\cite{Why3}.
-
-This chapter describes how to use the plug-in, from the
-\textsf{Frama-C} graphical user interface (section~\ref{wp-gui}), from
-the command line (section~\ref{wp-cmdline}), or from another plug-in
-(section~\ref{wp-api}). Additionally, the combination of the \textsf{WP}
-plug-in with the load and save commands of \textsf{Frama-C} and/or the
-\texttt{-then} command-line option is explained in section~\ref{wp-persistent}.
-
-\clearpage
-%-----------------------------------------------------------------------------
-\section{Installing Provers}
-\label{wp-install-provers}
-%-----------------------------------------------------------------------------
-
-The \textsf{WP} plug-in requires external provers to work.
-The recommended versions for external provers are:
-\begin{center}
- \begin{tabular}{crlc}
- Prover & Versions & Download &\\
- \hline
- \textsf{Why3} & \verb|1.3.1| &
- \url{http://why3.lri.fr} & \cite{Why3}\\
- \textsf{Alt-Ergo} & \verb|2.0.0| &
- \url{http://alt-ergo.ocamlpro.com} & \cite{AltErgo2006}\\
- % \textsf{Coq} & \verb|8.9.0| &
- % \url{http://coq.inria.fr} & \cite{Coq84}\\
- \end{tabular}
-\end{center}
-
-Recent \textsf{OPAM}-provided versions should work smoothly.
-Other versions might be supported as well, typically, as far as we know:
-\begin{itemize}
-\item \textsf{Alt-Ergo} \verb+2.2.0+ and \verb+2.3.0+, although distributed under a non-commercial licence.
-% \item \textsf{Coq} \verb+8.7.2+ and \verb+8.8.2+, although proof scripts compatibility can be an issue.
-\item \textsf{Why3} \verb+1.3.1+.
-\end{itemize}
-
-Other provers, like \textsf{Coq}, \textsf{Gappa}, \textsf{Z3}, \textsf{CVC3},
-\textsf{CVC4}, \textsf{PVS}, and many others, are accessible from
-\textsf{WP} through \textsf{Why3}. We refer the user to the manual of
-\textsf{Why3} to handle specific configuration tasks.
+automated theorem provers such as
+\textsf{Alt-Ergo}~\cite{AltErgo2006},
+\textsf{CVC4}~\cite{CVC4} and
+\textsf{Z3}~\cite{Z3}
+or by interactive proof assistants
+like \textsf{Coq}~\cite{Coq84} and more generally, any automated or interactive
+proover supported by \textsf{Why3}~\cite{Why3}.
\clearpage
%-----------------------------------------------------------------------------
@@ -1018,6 +980,10 @@ all unproved proof obligations are sent to external decision procedures.
Support for \textsf{Why-3 IDE} is no longer provided.
+Since \textsf{Frama-C 22.0} (Titanium) support for Coq interactive prover has
+been added and might also work with other interactive provers.
+See \texttt{-wp-interactive <mode>} option for details.
+
\begin{description}
\item[\tt -wp-prover <dp,...>] selects the decision procedures used to
discharge proof obligations. See below for supported provers. By
@@ -1028,6 +994,13 @@ Support for \textsf{Why-3 IDE} is no longer provided.
It is possible to ask for several decision procedures to be tried.
For each goal, the first decision procedure that succeeds cancels the
other attempts.
+\item[\tt -wp-interactive <mode>] selects the interaction mode with
+ interactive provers such as Coq. Three modes are available:
+ \texttt{"batch"} mode only check existing scripts (the default);
+ \texttt{"edit"} mode opens the default prover editor on each generated goal;
+ \texttt{"fix"} mode only opens
+ editor for non-proved goals. New scripts are created in the \texttt{interactive}
+ directory of \textsf{WP} session (see option \texttt{-wp-session <dir>}).
\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}.
@@ -1053,6 +1026,8 @@ Support for \textsf{Why-3 IDE} is no longer provided.
to the decision prover (defaults to 10 seconds).
\item[\tt -wp-smoke-timeout <n>] sets the timeout (in seconds) for smoke tests
(see \verb+-wp-smoke-tests+, defaults to 5 seconds).
+\item[\tt -wp-interactive-timeout <n>] sets the timeout (in seconds) for checking
+ edited scripts with interactive provers (defaults to 30 seconds).
\item[\tt -wp-time-extra <n>] additional time allocated to provers when
replaying a script. This is used to cope with variable machine load.
Default is \verb+5s+.
diff --git a/src/plugins/wp/doc/manual/wp_simplifier.tex b/src/plugins/wp/doc/manual/wp_simplifier.tex
index 4dda147545e..2e3e82551aa 100644
--- a/src/plugins/wp/doc/manual/wp_simplifier.tex
+++ b/src/plugins/wp/doc/manual/wp_simplifier.tex
@@ -344,13 +344,3 @@ following heuristic:
Inside the same level of priority, alternatives are kept in their original
order.
-
-
-
-
-
-
-
-
-
-
--
GitLab