wp_plugin.tex

  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
\paragraph{Why3.}
Since \textsf{WP} version \verb+0.7+ (Fluorine), native support for \textsf{Why3}
and \textsf{Why3-Ide} are provided. The older system \textsf{Why}
\verb+2.x+ is \emph{no} longer supported.
\begin{description}
\item[\tt -wp-prover "why3ide"] runs \textsf{Why3-Ide} with all
  generated goals.  On exit, the \textsf{WP} plug-in reads back your
  \textsf{Why3} session and updates the proof obligation status accordingly.
\item[\tt -wp-prover "<p>"] runs a \textsf{Why3} prover named \texttt{<p>}.
\item[\tt -wp-prover "why3:<p>"] useful alias when \texttt{"<p>"} can
  be ambiguous. It is actually different to run \texttt{alt-ergo} or \texttt{coq}
  directly from \textsf{WP} or through \textsf{Why3}.
\item[\tt -wp-detect] lists the provers available with \textsf{Why3}.
  This command calls \texttt{why3 --list-provers} but you have to
  configure \textsf{Why3} on your own before, for instance by using
  \texttt{why3config}. Consult the \textsf{Why3} user manual for details.
  The listed prover names can be directly used with the \texttt{-wp-prover} option.
\item[\tt -wp-why3='<cmd>'] override the \verb+why3+ command.
\end{description}

\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
\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