wp_plugin.tex

\begin{description}
\item[\tt -wp-prover <dp,...>] selects the decision procedures used to
  discharge proof obligations. See below for supported provers.  By
  default, \texttt{alt-ergo} is selected, but you may specify another
  decision procedure or a list of to try with.  Finally, you should
  supply \texttt{none} for this option to skip the proof step.

  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-proof <dp,...>] \textbf{deprecated} alias for \texttt{-wp-prover} for
  backward compatibility with \textsf{WP} version \verb+0.6+.
\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
  decision procedures. Default is 4 processes. With
  \texttt{-wp-par~1}, the order of logged results is fixed. With more
  processes, the order is runtime dependent.
\item[\tt -wp-filename-truncation <n>] truncates the basename of proof
  obligation files to the first \texttt{n} characters.
  Since numbers can be added as suffixes to ensure unique filenames,
  their length can be longer than \texttt{n}.
  No truncation is performed when the value equals zero.
\item[\tt -wp-(no)-proof-trace] asks for provers to output extra information
  on proved goals when available (default is: \texttt{no}).
\item[\tt -wp-(no)-unsat-model] asks for provers to output extra information
  when goals are not proved (default is: \texttt{no}).
\item[\tt -wp-timeout <n>] sets the timeout (in seconds) for the calls
  to the decision prover (defaults to 10 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+.
\item[\tt -wp-time-margin <n>] margin time for considering a proof to be
  replayable without a script. When a proof succeed within \verb+timeout-margin+
  seconds, it is considered fully automatic. Otherwise, a script is created
  by prover \verb+tip+ to register the proof time. This is used to decrease the
  impact of machine load when proof time is closed to the timeout.
  Default is \verb+5s+.
\end{description}

\hrule
\paragraph{Alt-Ergo.}
Direct support for the \textsf{Alt-Ergo} prover is provided. You need at least
version \verb+0.99+ of the prover, but more recent versions \verb+1.01+ or
\verb+1.30+ are preferrable. It is also the default selected prover.
\begin{description}
\item[\tt -wp-prover alt-ergo] selects \textsf{Alt-Ergo}.
\item[\tt -wp-prover altgr-ergo] opens the graphical interface of
  \textsf{Alt-Ergo} when the goal is not proved.
\item[\tt -wp-steps <$n$>] sets the maximal number of \textsf{Alt-Ergo}
  steps. This can be used as a machine-independent alternative to timeout.
\item[\tt -wp-depth <$n$>] sets '\textit{stop}' and
  '\textit{age-limit}' parameters of \textsf{Alt-Ergo} such that $n$ cycles of
  quantifier instantiations are enabled.
\item[\tt -wp-alt-ergo-opt <opt,...>] passes additional options to \textsf{Alt-Ergo}
  (default: none).
\item[\tt -wp-alt-ergo='<cmd>'] override the \verb+alt-ergo+ command.
\item[\tt -wp-altgr-ergo='<cmd>'] override the \verb+altgr-ergo+ command.
\end{description}

\hrule
\paragraph{Coq.}
Direct support for the \textsf{Coq} proof assistant is provided. The
generated proof obligations are accepted by \textsf{Coq} version \verb+8.4+.
When working with \textsf{Coq}, you will enter an interactive session,
then save the proof scripts in order to replay them in batch mode.

\begin{description}
\item[\tt -wp-prover coq] runs \texttt{coqc} with the default tactic or
  with the available proof script (see below).
\item[\tt -wp-prover coqide] first tries to replay some known proof
  script (if any). If it does not succeed, then a new interactive
  session for \texttt{coqide} is opened. As soon as \texttt{coqide}
  exits, the edited proof script is saved back (see below) and finally
  checked by \texttt{coqc}.\par
  The only part of the edited file retained by \textsf{WP} is the proof script
  between ``\texttt{Proof}\ldots\texttt{Qed.}''.
\item[\tt -wp-script <f.script>] specifies the file which proof scripts
  are retrieved from, or saved to. The format of this file is private to
  the \textsf{WP} plug-in. It is, however, a regular text file from which
  you can cut and paste part of previously written script proofs.
  The \textsf{WP} plug-in manages the content of this file for you.
\item[\tt -wp-(no)-update-script] if turned off, the user's script
  file will \emph{not} be modified. A warning is emitted if the script data base
  changed.
\item[\tt -wp-tactic <ltac>] specifies the \textsf{Coq} tactic to try
  with when no user script is found. The default tactic is
  \verb+"auto with zarith"+. See also how to load external libraries
  and user-defined tactics in section~\ref{prooflibs}.
\item[\tt -wp-tryhints] When both the user-provided script and the
  default tactic fail to solve the goal, other scripts for similar goals can
  be tried instead.
\item[\tt -wp-hints <n>] sets the maximal number of suggested proof scripts.
\item[\tt -wp-coq-timeout <n>] sets the maximal time in seconds for running
  the \texttt{coqc} checker. Does not apply to \texttt{coqide} (default: 30s).
\item[\tt -wp-coq-opt <opt,...>] additional options for \texttt{coqc} and \texttt{coqide}
  (default: none).
\item[\tt -wp-coqc='<cmd>'] override the \verb+coqc+ command.
\item[\tt -wp-coqide='<cmd>'] override the \verb+coqide+ command.
  If the command line contains the \verb+emacs+ word (case-insensitive),
  coq-options are not passed to the command, but a coq-project is used instead.
  This conforms to Proof General 4.3 settings.
  The project file can be changed (see below).
\item[\tt -wp-coq-project='<name>'] override the \verb+_CoqProject+ file name
  for Emacs and Proof General.
\end{description}
\hrule

\pagebreak
\paragraph{Why-3.}
Native support for \textsf{Why-3} is provided (for versions 1.0 and newer).
\\
Support for \textsf{Why-3 IDE} is no longer provided.
\begin{description}
\item[\tt -wp-prover "why3:<p>"] runs a \textsf{Why-3} prover named \texttt{<p>}, and
  exactly behaves like invoking \verb+why3 prover -P <p>+. The list of prover
  names \verb+<p>+ must be extracted from the \verb+[alias]+ section of your \textsf{Why-3}
  configuration, which \verb+frama-c -wp-detect+ does for you (see below).
\item[\tt -wp-prover "<p>"] can also be used instead of \verb+-wp-prover "why3:<p>"+
  when \verb+<p>+ is not natively supported by \textsf{WP}, like \texttt{alt-ergo},
  \texttt{altgr-ergo}, \texttt{coq}, \texttt{coqide}, \texttt{script} and \texttt{tip}.
\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}.
  The option reads your \textsf{Why-3} configuration and prints the available
  provers with their \verb+-wp-prover <p>+ code names.
\item[\tt -wp-why3='<cmd>'] overrides the path to the \verb+why3+ command.
\end{description}

\paragraph{Example of using Why-3.}
Suppose you have the following configuration:

\begin{logs}
# frama-c -wp-detect
[wp] Why3 provers detected:
   - Alt-Ergo 2.0.0 [why3:alt-ergo,altergo]
   - CVC4 1.6 [cvc4]
   - CVC4 1.6 (counterexamples) [cvc4-ce]
   - Coq 8.9.0 [why3:coq]
   - Z3 4.6.0 [z3]
   - Z3 4.6.0 (counterexamples) [z3-ce]
   - Z3 4.6.0 (noBV) [z3-nobv]
\end{logs}

Then, to use (for instance) \textsf{CVC4 1.6},
you can use \verb+-wp-prover cvc4+ (since this name is not conflicting
with any native prover). Alternatively, you can also use the less ambiguous
name  \verb+-wp-prover why3:cvc4+ if you prefer.
Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use \verb+-wp-prover z3-nobv+
or \verb+-wp-prover why3:z3-nobv+.

However, to use \textsf{Alt-Ergo 2.0.0} \emph{via} \textsf{Why-3}, you shall use
\verb+-wp-prover why3:alt-ergo+, since \verb+-wp-prover alt-ergo+ would select
the native support of \textsf{Alt-Ergo} prover. Finally, since \textsf{Why-3} also provides the alias
\verb+altergo+ for this prover, \verb+-wp-prover altergo+ will also run it \emph{via} \textsf{Why-3}.

Notice that \textsf{Why-3} provers benefit from a cache management when used in combination with a \textsf{WP}-session, see Section~\ref{wp-cache} for more details.

%% \paragraph{Sessions.}
%% Your \textsf{Why3} session is saved in the \texttt{"project.session"}
%% sub-directory of \texttt{-wp-out}. You may run
%% \texttt{why3ide} by hand by issuing the following command:
%% \begin{shell}
%% # why3ide -I <frama-c-share>/wp <out>/project.session
%% \end{shell}

%% Proof recovering features of \textsf{Why3} are fully available, and
%% you can interleave proving from \textsf{WP} with manual runs of
%% \texttt{why3ide}. Interactive proofs with \textsf{Why3} are completely
%% separated from those managed by the native \textsf{WP} interface with
%% \textsf{Coq}.

\subsection{Generated Proof Obligations}
Your proof obligations are generated and saved to several text
files. With the \texttt{-wp-out} option, you can specify a directory
of your own where all these files are generated. By default, this
output directory is determined as follows: in the GUI, it is
\texttt{<home>/.frama-c-wp} where \texttt{<home>} is the user's home
directory returned by the \texttt{HOME} environment variable. In
command-line, a temporary directory is automatically created and
removed when \textsf{Frama-C} exits.

Other options controlling the output of generated proof
obligations are:
\begin{description}
\item[\tt -wp-(no)-print] pretty-prints the generated proof obligations on
  the standard output. Results obtained by provers are reported as
  well (default is: \texttt{no}).
\item[\tt -wp-out <dir>] sets the user directory where proof
  obligations are saved. The directory is created if it does not exist
  yet. Its content is not cleaned up automatically.
\end{description}

\subsection{Additional Proof Libraries}
\label{prooflibs}

It is possible to add additional bases of knowledge to decision
procedures.  This support is provided for \textsf{Alt-Ergo},
\textsf{Why3} and \textsf{Coq} thanks to the following options:
\begin{description}
\item[\tt -wp-share <dir>] modifies the default directory where
  resources are found.  This option can be useful for running a modified or
  patched distribution of \textsf{WP}.
\item[\tt -wp-include <dir,\ldots,++sharedir>] (\textbf{deprecated} use driver instead) sets the directories where external
  libraries and driver files are looked for.
  The current directory (implicitly added to that list) is always looked up
  first.
  Relative directory names are relative to the current directory except
  for names prefixed by the characters \texttt{++}.
  In such a name, the directory is relative to the main \texttt{FRAMAC\_SHARE}
  directory.
\item[\tt -wp-alt-ergo-lib <f,\ldots>] (\textbf{deprecated} use altergo.file
  in driver instead) looks for \textsf{Alt-Ergo}
  library files \verb+"f.mlw"+ and inlines them into the proof
  obligation files for \textsf{Alt-Ergo}.
\item[\tt -wp-coq-lib <f,\ldots>] (\textbf{deprecated} use coq.file
  in driver instead) looks for \textsf{Coq} files
  \verb+"f.v"+ or \verb+"f.vo"+. If
  \verb+"f.vo"+ is not found, then \textsf{WP} copies \verb+"f.v"+
  into its working directory (see option
  \texttt{-wp-out}) and compiles it locally.
\item[\tt -wp-why-lib <f,\ldots>] (\textbf{deprecated} use why3.file in driver instead) looks for \textsf{Why3} library file
  \verb+"f.why"+ and opens the library \verb+"f.F"+ for the proving the
  goals.
\end{description}

\subsection{Linking \textsf{ACSL} Symbols to External Libraries}
\label{drivers}

Besides additional proof libraries, it is also possible to
\emph{link} declared \textsf{ACSL} symbols to external or predefined
symbols. In such case, the corresponding \textsf{ACSL} definitions,
if any, are not exported by \textsf{WP}s.

External linkage is specified in \emph{driver files}. It is possible
to load one or several drivers with the following \textsf{WP} plug-in option:
\begin{description}
\item[\tt -wp-driver <file,\ldots>] load specified driver files,
  replacing deprecated features from section~\ref{prooflibs}.

\end{description}

\newcommand{\ccc}{\texttt{,}\ldots\texttt{,}}
\newcommand{\user}[1]{\texttt{"}\textit{#1}\texttt{"}}
Each driver file contains a list of bindings with the following syntax:
\begin{center}
  \begin{tabular}{|l}
  \texttt{library} \user{lib}\verb':' \user{lib} \ldots \user{lib} \\
  \quad\begin{tabular}{rll}
  \rule{0em}{1.2em}
  \textit{group}.\textit{field} &\texttt{:=} \textit{string} \\
  \textit{group}.\textit{field} &\texttt{+=} \textit{string} \\
  \texttt{type} & \textit{symbol} & \verb'=' \user{link} \verb';' \\
  \texttt{ctor} & \textit{type} \textit{symbol}
                   \verb'(' \textit{type}\ccc\textit{type} \verb')'
                 & \verb'=' \user{link} \verb';' \\
  \texttt{logic} & \textit{type} \textit{symbol}
                   \verb'(' \textit{type}\ccc\textit{type} \verb')'
                 & \verb'=' \textit{property-tags} \user{link} \verb';' \\
  \texttt{predicate} & \textit{symbol}
                   \verb'(' \textit{type}\ccc\textit{type} \verb')'
                 & \verb'=' \user{link} \verb';'
  \end{tabular}
  \end{tabular}
\end{center}

It is also possible to define \emph{aliases} to other ACSL symbols, rather
than external links. In this case, you may replace \verb+=+ by
\verb+:=+ and use an ACSL identifier in place of the external \user{link}.
No property tag is allowed when defining aliases.

Library specification is optional and applies to subsequent linked
symbols. If provided, the \textsf{WP} plug-in automatically loads the
specified external libraries when linked symbols are used in a
goal. Dependencies among libraries can also be specified, after the
'\verb':''.

Generic \textit{group}.\textit{field} options have a specific
value for each theory. The binding applies to the current theory.
Binding with the \verb':=' operator
resets the option to the singleton of the given string
and binding with the \verb'+=' operator
adds the given string to the current value of the option.
The following options are defined by the plugin:
\texttt{coq.file}, \texttt{altergo.file}, \texttt{why3.file} and \texttt{why3.import}.

\textsf{C}-Comments are allowed in the file. For overloaded
\textsf{ACSL} symbols, it is necessary to provide one \user{link} symbol for
each existing signature. The same \user{link} symbol is used for all provers,
and must be defined in the specified libraries, or in the external
ones (see~\ref{prooflibs}).

It is also possible to specify different names
for each prover, with the following syntax:
\texttt{\{coq=\user{a};altergo=\user{b};why3=\user{c}\}}.
Alternatively, a link-name can be an arbitrary string
with patterns substituted by arguments, \verb="(%1+%2)"= for instance.

When a library \user{lib} is specified, the loaded module depends on the
target solver:
\begin{center}\tt
  \begin{tabular}{llll}
    & \textrm{Option} & \textrm{Format} \\
    \hline
    \textsf{Coq}: & coq.file & \verb+[dir:]path.v+ \\
    \textsf{Alt-Ergo}: & altergo.file & \verb+path.mlw+ \\
    \textsf{Why3}: & why3.file & \verb+path.why[:name][:as]+ \\
                   & why3.import & \verb+theory[:as]+ \\
  \end{tabular}
\end{center}

Precise meaning of formats is given by the following examples (all filenames are relatives to the driver file's directory):
\begin{description}
\item[\tt coq.file="mydir/bar.v"] Imports module \verb+Bar+ from file \verb+mydir/bar.vo+.
\item[\tt coq.file="mydir/foo:Foo.v"] Loads coq library \verb+foo.Foo+ from file \verb+mydir/foo/Foo.vo+.
\item[\tt why3.file="mydir/foo.why"] Imports theory \verb+foo.Foo+ from directory \verb+mydir+.
\item[\tt why3.file="mydir/foo.why:Bar"] Imports theory \verb+foo.Bar+ from directory \verb+mydir+.
\item[\tt why3.file="mydir/foo.why:Bar:T"] Imports theory \verb+foo.Bar as T+ from directory \verb+mydir+.
\item[\tt why3.import="foo.Bar"] Imports theory \verb+foo.Bar+ with no additional includes.
\item[\tt why3.import="foo.Bar:T"] Imports theory \verb+foo.Bar as T+ with no additional includes.
\end{description}

See also the default \textsf{WP} driver file, in \verb+[wp-share]/wp.driver+.

Optional \textit{property-tags} can be given to
\texttt{logic} \user{link} symbols to allow the WP to perform
additional simplifications (See section~\ref{wp-simplifier}).  Tags
consist of an identifier with column (`\verb+:+'), sometimes followed
by a link (`\user{link};'). The available tags are depicted on figure~\ref{wp-driver-tags}.

\begin{figure}[htbp]
\begin{center}
  \begin{tabular}{lp{10cm}}
    \quad Tags & Operator Properties \\
    \hline
\texttt{commutative:} & specify a commutative symbol:
                        $x \odot y = y \odot x$ \\
\texttt{associative:} & specify an associative symbol:
                        $(x \odot y) \odot z = x \odot (y \odot z)$ \\
\texttt{ac:} & shortcut for \texttt{associative:} \texttt{commutative:} \\
\texttt{left:}  & balance the operator on left during export to solvers (requires the associative tag):
                  $x \odot y \odot z = (x \odot y) \odot z$ \\
\texttt{right:} & balance the operator on right during export to solvers (requires the associative tag):
                      $x \odot y \odot z = x \odot (y \odot z)$ \\
\texttt{absorbant:} \user{a-link}\texttt{:} & specify \user{a-link} as being the absorbant element of the symbol: \\
                     & $\user{a-link} \odot x = \user{a-link}$ \\
                     & $x \odot \user{a-link} = \user{a-link}$ \\
\texttt{neutral:} \user{e-link}\texttt{:} & specify \user{e-link} as being the neutral element of the symbol: \\
                     &  $\user{e-link} \odot x = x$ \\
                     &  $x \odot \user{e-link} = x$ \\
\texttt{invertible:} & specify simplification relying on the existence of an inverse: \\
                     &  $x \odot y = x \odot z \Longleftrightarrow y = z$ \\
                     &  $y \odot x = z \odot x \Longleftrightarrow y = z$ \\
\texttt{idempotent:} & specify an idempotent symbol: $x \odot x = x$ \\
\hline
\texttt{injective:} &  specify an injective function:\\
                      & $f(x_1,\ldots,x_n) = f(y_1,\ldots,y_n) \Longrightarrow \forall i \; x_i = y_i$ \\
\texttt{constructor:} & specify an injective function, that constructs different values
                        from any other constructor. Formally, whenever $f$ and $g$ are two
                        distinct constructors, they are both injective and:
                        $f(x_1,\ldots,x_n) \neq g(y_1,\ldots,y_m)$ forall $x_i$ and $y_j$. \\
\hline
\end{tabular}
\end{center}
\caption{Driver Property Tags}
\label{wp-driver-tags}
\end{figure}

\clearpage
\subsection{Proof Session \& Cache}
\label{wp-cache}

The \textsf{WP} plugin can use a session directory to store informations to be used from one execution to another one.
It is used to store proof scripts edited from the TIP (see Section~\ref{wp-proof-editor}) and to replay them from the command line.
And it is also used to speedup the invocation of provers by reusing previous runs.

Actually, running provers can be demanding in terms of memory and CPU resources. When working
interactively or incrementally, it is often the case where most proof obligations remain unchanged
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 -- although proof scripts works with both.
There are different ways of using the cache, depending on your precise needs.

The \textsf{WP} options to control session and cache are \verb+-wp-session+ and \verb+-wp-cache+, as documented below:

\begin{description}
\item[\tt -wp-session <dir>] select the directory where cached results and proof scripts
  are stored. If the local directory \verb+'.frama-c'+ already exists, the default session
  directory \verb+'.frama-c/wp'+ will be used to setup the \textsf{WP} session.
\item[\tt -wp-cache <mode>] selects the cache mode to use with why3 provers. The default mode is \verb'update'
  if a \textsf{WP} session is set, and \verb+none+ otherwise. The cache entries are stored in the session directory,
  which is \verb+./.frama-c/wp/cache+ by default.
\end{description}

The available cache modes are described below:
\begin{description}
\item [\tt -wp-cache update]: use cache entries or run the provers, and store new results in the cache. This mode is useful when you are working interactively : proofs can be partial and volatile, and you want to accumulate and keep as much previous results as you can.
\item [\tt -wp-cache cleanup]: same as \verb+update+ mode but at the end of \textsf{Frama-C} execution, any cache entry that was not used nor updated will be deleted. This mode shall be only used when you want to cleanup your cache with old useless entries, typically at the end of an interactive session.
\item [\tt -wp-cache replay]: same as \verb+update+ mode but new results are \emph{not} stored in the cache. This mode is useful for continuous integration, when you are not sure your cache is complete but don't want to modify it.
\item [\tt -wp-cache offline]: similar to \verb+replay+ mode but cache entries are the unique source of results. Provers are never run and missing cache entries would result in a «~Failed~» verdict. This mode is useful to fasten continuous integration and enforcing cache completeness.
\item [\tt -wp-cache rebuild]: force prover execution and store all results in the cache. Previous results will be replaced with new onces, but entries for non relevant proofs would be kept and you might need a cleanup stage after. This mode is useful when you modify you why3 or prover installation and you don't want to reuse your previous cache entries.
\item [\tt -wp-cache none]: do not use nor modify cache entries; provers are run normally. This option must be used if you have a session set and you don't want to use the cache, since the default is mode \verb+update+ in this case. But you probably always to benefit from a cache when you have an (interactive) session.
\end{description}

When using cache with a non-\verb+offline+ mode, time and steps limits recorded in the cache are compared to the command line settings to produce meaningful and consistent results. Hence, if you provide more time or more steps from the command line than before, the prover would be run again. If you provide less or equal limits, the cache entries are reused, but \textsf{WP} still report the cached time and step limits to inform you of your previous attempts. For instance, if you have in the cache a « Valid » entry with time 12.4s and re-run it with a timeout of 5s, you will have a « Timeout » result with time 12.4s printed on the console.
Cached usage is indicated on the standard output, unless you specify \verb+-wp-msg-key no-cache-info+.

\section{Plug-in Developer Interface}
\label{wp-api}

The \textsf{WP} plug-in has several entry points registered in the
\texttt{Dynamic}\footnote{See the \emph{plug-in development guide}}
module of \textsf{Frama-C}.

Those entry points are however deprecated.
Instead, a full featured \textsf{OCaml} API is now exported with the
\textsf{Wp} plug-in. As documented in the \textsf{Frama-C} user manual, simply add the directive \verb!PLUGIN_DEPENDENCIES+=Wp! to the Makefile of your plug-in.

The high-level API for generating and proving properties is exported
in module \textsf{Wp.API}. The logical interface, compilers, and memory models are also accessible. See the generated \textsf{HTML} documentation of the platform for details.

\section{Proof Obligation Reports}

The \textsf{WP} plug-in can export statistics on generated proof
obligations. These statistics are called \textit{WP reports} and are
distinct from those \textit{property reports} generated by the
\textsf{Report} plug-in. Actually, \textit{WP reports} are statistics
on proof obligations generated by \textsf{WP}, whereas
\textit{property reports} are consolidated status of properties,
generated by the \textsf{Frama-C} kernel from various analyzers.
We only discuss \textit{WP reports} in this section.

Reports are generated with the following command-line options:
\begin{description}
\item[\tt -wp-report <Rspec$_1$,...,Rspec$_n$>] specifies the list of
  reports to export.
  Each value \texttt{Rspec$_i$} is a \textit{WP report} specification file
  (described below).
\item[\tt -wp-report-basename <name>] set the basename for exported
  reports (described below).
\item[\tt -wp-report-json <file>.json] output the reports in JSON format.
  If the file already exists, it is used to stabilize the \verb+range+ of steps
  reports in all other reports (see below).
\end{description}

Reports are created from user defined wp-report specification files.
The general format of a wp-report file is as follows:

\begin{logs}
  <configuration section...>
  @HEAD
  <head contents...>
  @CHAPTER
  <per chapter contents...>
  @SECTION
  <per section contents of a chapter...>
  @TAIL
  <tail contents...>
  @END
\end{logs}

The configuration section consists of optional commands, one per line,
among:
\begin{description}
\item[\tt @CONSOLE] the report is printed on the standard output. \\
  Also prints all numbers right-aligned on 4 ASCII characters.
\item[\tt @FILE "<\textit{file}>"] the report is generated in file \textit{file}.
\item[\tt @SUFFIX "<\textit{ext}>"] the report is generated in file \textit{base.ext},\\
  where \textit{base} can be set with \texttt{-wp-report-basename} option.
\item[\tt @ZERO "<\textit{text}>"] text to be printed for $0$-numbers. Default is \verb+"-"+.

\item[\tt @GLOBAL\_SECTION "<\textit{text}>"] text to be printed for the chapter name about globals
\item[\tt @AXIOMATIC\_SECTION "<\textit{text}>"] text to be printed for the chapter name about axiomatics
\item[\tt @FUNCTION\_SECTION "<\textit{text}>"] text to be printed for the chapter name about functions

\item[\tt @AXIOMATIC\_PREFIX "<\textit{text}>"] text to be printed before axiomatic names.
  Default is \verb+"Axiomatic"+ (with a trailing space).
\item[\tt @FUNCTION\_PREFIX "<\textit{text}>"] text to be printed before function names. Default is empty.
\item[\tt @GLOBAL\_PREFIX "<\textit{text}>"] text to be printed before global property names.
  Default is \verb+"(Global)"+ (with a trailing space).
\item[\tt @LEMMA\_PREFIX "<\textit{text}>"] text to be printed before lemma names.
  Default is \verb+"Lemma"+ (with a trailing space).
\item[\tt @PROPERTY\_PREFIX "<\textit{text}>"] text to be printed before other property names.
\end{description}

The generated report consists of several optional parts, corresponding
to Head, Chapter and Tail sections of the wp-report specification file.
First, the head contents lines are produced.
Then the chapters and their sections are produced.
Finally, the Tail content lines are printed.

The different chapters are about globals, axiomatics and functions.
Outputs for these chapters can be specified using these directives:
\begin{description}
\item[\tt @CHAPTER] <\textit{chapter header...>}
\item[\tt @GLOBAL] <\textit{global section contents...>}
\item[\tt @AXIOMATIC] <\textit{per axiomatic section contents...>}\\
For each axiomatic, a specific section is produced under the chapter about axiomatics.
\item[\tt @FUNCTION] <\textit{per function section contents...>}\\
For each function analyzed by \textsf{WP}, a specific section is produced under the chapter about functions.
\item[\tt @SECTION] <\textit{default section contents...>}
\item[\tt @PROPERTY] <\textit{per property contents...>}\\
For each property of a section, a specific textual content can be specified.
\end{description}

Textual contents use special formatters that will be replaced by
actual statistic values when the report is generated. There are
several categories of formatters (PO stands for \emph{Proof Obligations}):

\begin{center}
  \begin{tabular}{ll}
    \textbf{Formatters} & \textbf{Description} \\
    \hline\hline
    \verb+&<+{\it col}\verb+>:+ & insert spaces up to column \textit{col} \\
    \verb+&&+ & prints a \verb+"&"+ \\
    \verb+%%+ & prints a \verb+"%"+ \\
    \hline
    \verb+%<+{\it stat}\verb+>+ & statistics for section \\
    \verb+%prop+ & percentage of proved properties in section \\
    \verb+%prop:total+ & number of covered properties \\
    \verb+%prop:valid+ & number of proved properties \\
    \verb+%prop:failed+ & number of remaining unproved properties \\
    \verb+%<+{\it prover}\verb+>+ & PO discharged by \textit{prover} \\
    \verb+%<+{\it prover}\verb+>:<+{\it stat}\verb+>+ & statistics for \textit{prover} in section \\
    \hline
  \end{tabular}
\end{center}

\begin{center}
  \begin{tabular}{ll}
    \hline
    \textbf{Provers} \\
    (\verb+<+{\it prover}\verb+>+) & A prover name (see \texttt{-wp-prover}) \\
    \hline
    \hline
    \textbf{Statistics} \\
    (\verb+<+{\it prover}\verb+>+) \\
    \verb+total+ & number of generated PO \\
    \verb+valid+ & number of discharged PO \\
    \verb+failed+ & number of non-discharged PO \\
    \verb+time+ & maximal time used by prover for one PO \\
    \verb+steps+ & maximal steps used by prover for one PO \\
    \verb+range+ & range of maximal steps used by prover (more stable)\\
    \verb+success+ & percentage of discharged PO \\
    \hline
  \end{tabular}
\end{center}

\textbf{Remarks:} \verb+&ergo+ is a shortcut for \verb+&alt-ergo+. Formatters
can be written \verb+"%.."+ or \verb+"%{..}"+. When \verb+range+ is used
instead of \verb+steps+, the maximal number $n$ of steps is printed as a range $a..b$ that
contains $n$.
When option \verb+-report-json+ is used, the previous rank $a$ and $b$ are kept when
available and still fits with the new maximal step number. Otherwise, $a$ and $b$ are re-adjusted
following an heurisitics designed to increase the stability for non-regression testing.

Textual contents can use naming formatters that will be replaced by
current names:
\begin{center}
  \begin{tabular}{ll}
   \textbf{Names} & \textbf{Description} \\
    \hline\hline
    \verb+%chapter+ & current chapter name \\
    \verb+%section+ & current section name \\
    \verb+%global+ & current global name (under the chapter about globals)\\
    \verb+%axiomatic+ & current axiomatic name (under the chapter about axiomatics) \\
    \verb+%function+ & current function name (under the chapter about functions)\\
    \verb+%name+ & current name defined by the context:\\
                 & - property name inside \texttt{@PROPERTY} contents,\\
                 & - function name inside \texttt{@FUNCTION} contents,\\
                 & - axiomatic name inside \texttt{@AXIOMATIC} contents,\\
                 & - global name inside \texttt{@GLOBAL} contents,\\
                 & - section name inside \texttt{@SECTION} contents,\\
                 & - chapter name inside \texttt{@CHAPTER} contents.\\
    \hline
  \end{tabular}
\end{center}
\clearpage

%-----------------------------------------------------------------------------
\section{Plug-in Persistent Data}
\label{wp-persistent}

As a general observation, almost \emph{none} of the internal
\textsf{WP} data is kept in memory after each execution. Most of the
generated proof-obligation data is stored on disk before being sent to
provers, and they are stored in a temporary directory that is removed
upon \textsf{Frama-C} exit (see also \texttt{-wp-out} option).

The only information which is added to the \textsf{Frama-C} kernel
consists in a new status for those properties proved by \textsf{WP} plug-in with
their dependencies.

Thus, when combining \textsf{WP}
options with \texttt{-then}, \texttt{-save} and \texttt{-load}
options, the user should be aware of the following precisions:
\begin{description}
\item[\tt -wp, -wp-prop, -wp-fct, -wp-bhv.] These options make the
  \textsf{WP} plug-in generate proof-obligations for the selected
  properties. The values of theses options are never saved and they are
  cleared by \texttt{-then}. Hence, running \texttt{-wp-prop A}
  \texttt{-then} \texttt{-wp-fct F} does what you expect:
  properties tagged by \texttt{A} are proved only once.
\item[\tt -wp-print, -wp-prover, -wp-gen, -wp-detect.] These options do not
  generate new proof-obligations, but run other actions on all
  previously generated ones. For the same reasons, they are not saved
  and cleared by \texttt{-then}.
\item[\tt -wp-xxx.] All other options are tunings that can be easily
  turned on and off or set to the desired value.
  They are saved and kept across \texttt{-then} commands.
\end{description}

%-----------------------------------------------------------------------------

% vim: spell spelllang=en