wp_plugin.tex

\chapter{Using the WP Plug-in}
\label{wp-plugin}

The \textsf{WP} plug-in can be used from the \textsf{Frama-C} command line 
or within its graphical user interface. It is a
dynamically loaded plug-in, distributed with the kernel since the
\textsf{Carbon} release of \textsf{Frama-C}.

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 natively supported provers are:
\begin{center}
  \begin{tabular}{crlc}
    Prover & Version & Download &\\
    \hline
    \textsf{Alt-Ergo} & \verb|0.99.1| to \verb|2.0.0| & 
    \url{http://alt-ergo.ocamlpro.com} & \cite{AltErgo2006}\\
    \textsf{Coq} & \verb|8.5|, \verb|8.6| or \verb|8.7| & 
    \url{http://coq.inria.fr} & \cite{Coq84}\\
    \textsf{Why3} & \verb|0.88+| & 
    \url{http://why3.lri.fr} & \cite{Why3}\\
  \end{tabular}
\end{center}

Recent \textsf{OPAM}-provided versions should work smoothly.

Other provers, like \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.

Provers can be installed at any time, before or after the installation
of \textsf{Frama-C/WP}. However, when using \textsf{Coq} and
\textsf{Why-3}, it is better to install them before, or to
re-configure and re-install \textsf{WP}, as explained below.

\paragraph{Configuration.} When using \textsf{Coq} and \textsf{Why-3}, pre-compiled 
libraries are built during the compilation of \textsf{Frama-C}, which
speed up the proof process in a significant way. This behavior can be
turned on/off at configure time, typically:
\begin{logs}
# configure --disable-wp-coq --disable-wp-why3
\end{logs}

\paragraph{Compilation.} If you want to compile the \textsf{Coq} and \textsf{Why-3} 
libraries manually, you can still run:
\begin{logs}
# make wp-coq wp-why3
# [sudo] make wp-coq-install
\end{logs}

\paragraph{Remark.} The \textsf{Why}~\cite{Filliatre2003} prover is no longer supported 
since \textsf{WP} version \verb+0.7+ (Fluorine).

\clearpage
%-----------------------------------------------------------------------------
\section{Graphical User Interface}
\label{wp-gui}
%-----------------------------------------------------------------------------

\newcommand{\loadicon}[1]{\raisebox{-3pt}{\rule{0pt}{13pt}\includegraphics[height=12pt]{#1}}}

To use the \textsf{WP} plug-in with the GUI, you simply need to run the
\textsf{Frama-C} graphical user interface. No additional option is
required, although you can preselect some of the \textsf{WP} options
described in section~\ref{wp-cmdline}:

\begin{shell}
  \$ frama-c-gui [options...] *.c
\end{shell}

\begin{figure}[p]
\begin{center}
\includegraphics[width=\textwidth]{wp-gui-main.png}
\end{center}
\caption{WP in the Frama-C GUI}
\label{wp-gui-panel}
\end{figure}

\begin{figure}[p]
\begin{center}
\includegraphics[width=\textwidth]{wp-gui-run.png}
\end{center}
\caption{WP run from the GUI}
\label{wp-gui-run}
\end{figure}

As we can see in figure~\ref{wp-gui-panel}, the memory model, the
decision procedure, and some \textsf{WP} options can be tuned from the
\textsf{WP} side panel. Other options of the \textsf{WP} plug-in are still
modifiable from the \texttt{Properties} button in the main GUI toolbar.

To prove a property, just select it in the internal source view and
choose \textsf{WP} from the contextual menu. The \texttt{Console}
window outputs some information about the
computation. Figure~\ref{wp-gui-run} displays an example of such a
session.

If everything succeeds, a green bullet should appear on the left of
the property. The computation can also be run for a bundle of
properties if the contextual menu is open from a function or behavior
selection.

The options from the \textsf{WP} side panel correspond to some options
of the plug-in command-line. Please refer to section~\ref{wp-cmdline}
for more details. In the graphical user interface, there are also
specific panels that display more details related to the \textsf{WP} plug-in,
that we shortly describe below.

\paragraph{Source Panel.} On the center of the \textsf{Frama-C} window, the status 
of each code annotation is reported in the left margin. The meaning of
icons is the same for all plug-ins in \textsf{Frama-C} and more precisely described
in the general user's manual of the platform. The status emitted by the \textsf{WP} plug-in are:
\begin{center}
  \begin{tabular}{cl}
    \multicolumn{2}{l}{\bf Icons for properties:} \\
    \hline
    \loadicon{feedback/never_tried.png} & No proof attempted. \\
    \loadicon{feedback/unknown.png} & The property has not been validated. \\
    \loadicon{feedback/valid_under_hyp.png} & The property is \emph{valid} but has dependencies. \\
    \loadicon{feedback/surely_valid.png} & The property and \emph{all} its dependencies are \emph{valid}. \\
    \hline
  \end{tabular}
\end{center}

\paragraph{WP Goals Panel.}
This panel is dedicated to the \textsf{WP} plug-in. It shows the
generated proof obligations and their status for each prover.
By clicking on a prover
column, you can also submit a proof obligation to a prover by
hand. Right-click provides more options depending on the prover, such
as proof-script editing for \textsf{Coq}.

\paragraph{Interactive Proof Editor.}
From the Goals Panel view, you can double-click on a row and open the \emph{interactive proof editor} panel as described in section~\ref{wp-proof-editor}.

\paragraph{Properties Panel.} This panel summarizes the consolidated 
status of properties, from various plug-ins. This panel is not
automatically refreshed. You should press the \texttt{Refresh} button
to update it. This panel is described in more details in the general
\textsf{Frama-C} platform user's manual.

\clearpage
%-----------------------------------------------------------------------------
\section{Interactive Proof Editor}
\label{wp-proof-editor}
%-----------------------------------------------------------------------------

This panel focus on one goal generated by \textsf{WP}, and allow the user to visualize the logical sequent to be proved, and to interactively decompose a complex proof into smaller pieces by applying \emph{tactics}.

\begin{figure}[htbp]
\begin{center}
\includegraphics[width=\textwidth]{wp-tip-run.png}
\end{center}
\caption{Interactive Proof Editing}
\label{wp-tip-run}
\end{figure}

The general structure of the panel is illustrated figure~\ref{wp-tip-run}. The central text area prints the logical sequent to proved. In consists of a formula to \verb+Prove+ under the hypotheses listed in the \verb+Assume+ section. Each hypothesis can consists of :
\begin{quote}
\begin{tabular}{ll}
\verb+Type:+& formula expressing a typing constraint;\\
\verb+Init:+& formula characterizing global variable initialisation;\\
\verb+Have:+& formula from an assertion or an instruction in the code;\\
\verb+When:+& condition from a simplification performed by \textsf{Qed};\\
\verb+If:+& structured hypothesis from a conditional statement;\\
\verb+Either:+& structured disjunction from a switch statement.\\
\verb+Stmt:+& labels and C-like instructions representing the memory updates during code execution;\\
\end{tabular}
\end{quote}

\subsection{Display Modes}

There are several modes to display the current goal:
\begin{quote}
\begin{tabular}{ll}
\verb+Autofocus:+ & filter out clauses not mentioning \emph{focused} terms (see below);\\
\verb+Full Context:+ & disable autofocus mode --- all clauses are visible; \\
\verb+Unmangled Memory:+ & autofocus mode with low-level details of memory model; \\