wp_plugin.tex

  In this case, a warning is emitted for potential runtime errors.
  Refer to Section~\ref{wp-model-arith} for details.
\item[\tt -wp-(no)-init-const] use initializers for global const variables
  (defaut is: \texttt{yes}).
\item[\tt -wp-(no)-split] conjunctions in generated proof obligations are
  recursively split into sub-goals.  The generated goal names are
  suffixed by ``{\tt part<{\it n}>}'' (defaults to \texttt{no}).
\item[\tt -wp-split-depth <{\it d}>] sets the depth of exploration for the
  \texttt{-wp-split} option. ``-1'' stands for unlimited depth. Default is 0.
\item[\tt -wp-split-max <{\it n}>] When \verb+-wp-split+ is active,
  limit the number of generated sub-goals to \textit{n} parts on each conditional statement.
  (defaults to \verb+1000+).
\item[\tt -wp-(no)-callee-precond] includes preconditions of the callee
  after\footnote{Proof obligations are always generated to check preconditions.}
  a call (default is: \texttt{yes}).
\item[\tt -wp-(no)-precond-weakening] discard pre-conditions of side behaviours (sound but
  incomplete optimisation, default is: \texttt{no}).
\item[\tt -wp-unfold-assigns <{\it n}>] when proving assigns, unfold up to
  \textit{n} levels of \texttt{struct} compounds types or access via ranges.
  \texttt{struct} are unfolded field by field, ranges are unfolded cell by
  cell (via a universal quantification over the index of the cell).
  This allows for proving that assigning a complete structure is still included
  into an assignment field by field, or that assigning a range is still included
  in a union of subranges. This option is set to \texttt{0} by default, because
  it is generally not necessary and it can generates a large number of
  verifications for structures with many (nested) fields. \texttt{-1} enables
  full unfolding.
\item[\tt -wp-(no)-frama-c-stdlib-terminate] Frama-C stdlib functions without
  \texttt{terminates} specification are considered to terminate when called
  (default is: \texttt{no}).
\item[\tt -wp-(no)-declarations-terminate] Undefined external functions without
  \texttt{terminates} specification are considered to terminate when called
  (default is: \texttt{no}).
\item[\tt -wp-(no)-definitions-terminate] Defined functions without
  \texttt{terminates} specification are considered to terminate when called
  (default is: \texttt{no}).
\item[\tt -wp-(no)-variant-with-terminates] prove \texttt{loop variant} under
  the termination hypothesis (thus, under a
  \texttt{terminates \textbackslash{}false}, any loop variant proof is trivial)
  (default is: \texttt{no}).
\end{description}

\subsubsection{ACSL extension \texttt{@calls}}
\label{acsl:calls}

Frama-C provides an ACSL extension \texttt{@calls} that can be written
before an indirect call to indicate which functions can be the target
of the pointer (see \cite{userman} for more information). Upon encountering
such annotation, WP will perform a case analysis with the contract of
each provided function.

For example:

\begin{lstlisting}[language=c, alsolanguage=acsl]
/*@ ensures \result == x ; */
int f1(int x);
/*@ ensures \result == x+1 ; */
int f2(int x);

/*@ requires fp == &f1 || fp == &f2 ;
    ensures POST: \result == 4 || \result == 5; */
int caller(int (*fp)(int)){
  //@ calls f1, f2 ;
  return (*fp)(4);
}
\end{lstlisting}

These annotations split post-conditions to the dynamic call into two sub-goals: one for call to \verb+f1+ and
a second for the call to \verb+f2+. A last goal is generated at the call
site: one must prove that \verb+fp+ is either \verb+f1+ or \verb+f2+.

\subsubsection{Proof of \texttt{@terminates}}
\label{ss-sec:plugin-terminates}

In ACSL, a function can be specified to terminate when some condition \verb+P+ holds
in pre-condition.

\begin{lstlisting}[language=c, alsolanguage=acsl]
/*@ terminates P ; */
void function(void){
  ...
}
\end{lstlisting}

If terminates verification is active (depending on \verb+-wp+ options) WP collects all function calls and loops
and generate verification conditions (VCs) to prove them, as detailed below.

\paragraph{Loop variants.} When a loop has a variant, no particular verification
is generated for termination. However, if \verb+-wp-variant-with-terminates+ is
active, the variant is verified only when \verb+P+ holds in pre-condition.
Intuitively, this option means that variant has to decrease only if the function has to terminate. For example:

\begin{lstlisting}[language=c, alsolanguage=acsl]
//@ terminates i >= 0 ;
void positive(int i){
  /*@ loop invariant \at(i, Pre) >= 0 ==> 0 <= i <= \at(i, Pre) ;
      loop assigns i ;
      loop variant i ; // verified when i >= 0 at pre
  */
  while(i) --i;
}
\end{lstlisting}

Note that when \verb+terminates \false+ is specified, any loop
variant would trivially holds.

When a loop does not have a variant, WP checks that the loop is unreachable
when \verb+P+ holds in precondition, which means that a loop is allowed to not
terminate when the function does not have to terminate. For example:

\begin{lstlisting}[language=c, alsolanguage=acsl]
//@ terminates i >= 0 ;
void function(int i){
  if(i < 0){
    // note i >= 0 && i < 0 ==> \false
    while(1);
  }
}
\end{lstlisting}

\paragraph{Function call.} When a function \verb+f+ is required to terminate on
\verb+P+, and calling function \verb+g+ only terminates when \verb+Q+, WP tries to
prove that \verb+P@pre ==> Q@call-point+. Indeed, for \verb+f+ to terminates while calling
\verb+g+, then \verb+g+ shall terminate. Note that it
means that if the function under verification shall terminate, any call to a
non-terminating function shall be unreachable. For example:

\begin{lstlisting}[language=c, alsolanguage=acsl]
//@ terminates i <= 0 ;
void f(int i) ;

//@ terminates i >  0 ;
void g(int i) ;

/*@ requires i <= 0 ;
    terminates \true ; */
void caller(int i){
  f(i); // succeeds
  g(i); // fails, thus global termination is not proved
}
\end{lstlisting}

When a called function does not have a terminates specification, WP assumes one
as specified by the options:

\begin{itemize}
\item \verb+-wp-frama-c-stdlib-terminate+,
\item \verb+-wp-declarations-terminate+,
\item \verb+-wp-definitions-terminate+.
\end{itemize}

\paragraph{(Mutually) recursive function.} When a function is involved in a
recursive cluster (as defined in the ACSL manual) and shall terminate, WP checks that a
\verb+decreases+ clause is available for the function. Proving that existing
recursive calls might be unreachable is delegated to the proof of the
\verb+decreases+ clause.

\paragraph{Function pointers. } On a call via a function pointer, WP checks that
a \verb+@calls+ is specified for this function pointer. If so, WP just behaves
as explained before for function calls. If such a specification is not available,
WP considers that the pointed function might call the function under
verification and thus that it is part of a recursive cluster and shall provide
a \verb+decreases+ clause.

\subsection{Smoke Tests}

During modular deductive verification, inconsistencies in function requirements
can be difficult to detect until you actually call it.
Although, such inconsistencies make its post-conditions provable, while its pre-conditions
would never be provable.

The \textsf{WP} plug-in can generate smoke-tests to detect such inconsistencies.
Basically, it consists in checking if \verb+\false+ is provable under the requirements
or assumptions of a behaviour, or under the invariants of a loop. Also, a simple reachability
analysis is performed to track dead-code statements and calls that neither terminates nor exits.

This is best-effort verification : if at least one prover succeed in proving \verb+\false+,
an inconsistency is detected. Otherwise, the test is not conclusive, and you can never be sure
that the ACSL annotations are free of inconsistencies.

In case any smoke-test fails, a ``\textit{False if reachable}'' status is put on the
inconsistent requirements, or on the loop with inconsistent invariants, and
\textsf{WP} generates a user warning.

\begin{description}
\item[\tt -wp-(no)-smoke-tests] generates checks to detect inconsistencies
  (default is: \texttt{no}).
\item[\tt -wp-smoke-timeout] timeout to be used for trying to prove \verb+\false+
  on smoke-tests (default is \verb+2+ seconds).
\item[\tt -wp-(no)-smoke-dead-assumes] includes smoke tests for dead assumes
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-smoke-dead-call] includes smoke tests for non-terminating
  calls (default is: \texttt{yes}).
\item[\tt -wp-(no)-smoke-dead-code] includes smoke tests for dead code (default
  is: \texttt{yes}).
\item[\tt -wp-(no)-smoke-dead-local-init] includes smoke tests for dead local
  variables initialization (default is: \texttt{no}).
\item[\tt -wp-(no)-smoke-dead-loop] includes smoke tests for inconsistent loop
  invariants (default is: \texttt{yes}).
\end{description}

When reporting prover results for smoke-tests, the \textsf{WP} displays
``Failed'' when some prover succeeds in discharging the \verb+\false+ proof-obligation
and ``Passed'' when all the provers result are unknown or interrupted.
In the final prover statistics, the interrupted smoke tests are \emph{not} reported, since
they are considered valid tests.

\subsection{Trigger Generation}
\label{triggers}

The \textsf{ACSL} language does not provide the user with a syntax for
declaring \emph{triggers} associated to lemmas and axioms. However,
triggers are generally necessary for \textsf{SMT} solvers to discharge
efficiently the generated proof obligations.

There is a limited support for triggers in \textsf{WP}. The
\emph{sub-terms} and \emph{sub-predicates} marked with label
\verb+"TRIGGER"+ in an axiom or lemma are collected to generate a
multi-trigger for their associated free variables.

\subsection{Qed Simplifier Engine}

These options control the simplifications performed by the \textsf{WP} plug-in before
sending proof obligations to external provers. The default simplifiers can be
controlled by the following options:

\begin{description}
\item[\tt -wp-(no)-simpl] simplifies constant
  expressions and tautologies (default is: \texttt{yes}).
\item[\tt -wp-(no)-let] propagates equalities by substitutions
  and let-bindings (default is: \texttt{yes}).
\item[\tt -wp-(no)-filter] filter non used variables and related hypotheses
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-core] factorize common properties between branches
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-pruning] eliminates trivial branches of conditionals
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-clean] removes unused terms and variables from
  proof obligations (default is: \texttt{yes}).
\item[\tt -wp-(no)-ground] replace ground values in equalities
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-extensional] use extensional equality on compounds
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-reduce] replace functions with precedence to constructors and
  operators (default is: \texttt{yes}).
\item[\tt -wp-(no)-parasite] eliminate parasite variables
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-bits] simplifies bitwise operations
  (default is: \texttt{yes}).
\item[\tt -wp-(no)-init-summarize-array] summarize contiguous initializers
  with quantified formulae (default: \texttt{yes}).
\item[\tt -wp-(no)-simplify-is-cint] eliminates redundant constraints on integers
  (default: \texttt{yes}).
\item[\tt -wp-(no)-simplify-land-mask] tight constants in logical-and with
  unsigned integers (default: \texttt{yes}).
\item[\tt -wp-(no)-prenex] normalize nested quantifiers into prenex-form
  (default: \texttt{no}).
\item[\tt -wp-(no)-simplify-forall] eliminates integer ranges in quantifiers
  (\emph{unsound}, to be used with caution, default is: \texttt{no}).
\item[\tt -wp-(no)-simplify-type] remove type constraints from proof obligation
  (\emph{incomplete}, default is: \texttt{no}).
\item[\tt -wp-bound-forall-unfolding <n>] instantiates statically \texttt{n}
  instances of $k$ for hypothesis $\forall k \in [n_1..n_2], a = b$
  (default is: \texttt{1000}).
\end{description}

\subsection{Prover Selection}
\label{wp-provers}

The generated proof obligations are submitted to external decision
procedures run through the \textsf{Why-3} platform.  If proof obligations have
just been generated, by using \texttt{-wp}, \texttt{-wp-fct}, \texttt{-wp-bhv}
or \texttt{-wp-prop}, then only the new proof obligations are sent. Otherwise,
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
  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-interactive <mode>] selects the interaction mode with
  interactive provers such as Coq (while it could work for other interactive
  provers, it has not been tested so far). Five modes are available:
  \begin{itemize}
  \item \texttt{"batch"} mode only check existing scripts (the default);
  \item \texttt{"update"} mode update the script and then checks it;
  \item \texttt{"edit"} mode opens the default prover editor on each generated goal;
  \item \texttt{"fix"} mode only opens editor for non-proved goals;
  \item \texttt{"fixup"} combines \texttt{"update"} and \texttt{"fix"} (if necessary).
  \end{itemize}
  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}.
  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
  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. (default is: 60)
\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-timeout <n>] sets the timeout (in seconds) for the calls
  to the decision prover (defaults to 10 seconds).
\item[\tt -wp-fct-timeout <f1:t1,f2:t2,...>] customize the timeout for each
  specified function (\texttt{t1} for \texttt{f1}, \texttt{t2} for \texttt{f2},
  etc).
\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-(no)-script-on-stdout] displays generated proof scripts on stdout
  instead of saving them on disk (default is: \texttt{no}).
\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+.
\item[\tt -wp-steps <$n$>] sets the maximal number of prover
  steps. This can be used as a machine-independent alternative to timeout.
\item[\tt -wp-why3-opt='options,...'] provides additional options to the
  \verb+why3+ command.
\item[\tt -wp-prepare-scripts] initialize a script tracking directory in the
  session directory.
\item[\tt -wp-finalize-scripts] remove untracked scripts according to the
  tracking directory if it does exist (does not remove anything otherwise).
\item[]\tt -wp-dry-finalize-scripts] scripts that might be removed by
  \verb+-wp-finalize-scripts+ are kept, a message is printed instead for each
  file. The marks directory is kept.
\end{description}

\paragraph{Example of using provers.}
Suppose you have the following configuration:

\begin{logs}
# ./bin/frama-c -wp-detect
[wp] Prover   Alt-Ergo 2.0.0  [alt-ergo|altergo|Alt-Ergo:2.0.0]
[wp] Prover       CVC4 1.6    [cvc4|CVC4:1.6]
[wp] Prover       CVC4 1.6    [cvc4-ce|CVC4:1.6,counterexamples]
[wp] Prover    Eprover 2.4    [eprover|Eprover:2.4]
[wp] Prover         Z3 4.8.7  [z3-ce|Z3:4.8.7:counterexamples]
\end{logs}

Then, to use (for instance) \textsf{CVC4 1.6},
you can use \verb+-wp-prover cvc4+ or \verb+-wp-prover CVC4:1.6+.
Similarly, if you want to use \textsf{Z3 4.6.0} without bitvectors, you can use \verb+-wp-prover z3-nobv+.
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}.

If you require a specific version of a prover which is not installed,
\textsf{WP} will fallback to the default version available to \textsf{Why-3} for this prover, if any.

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 thanks to the following option:
\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}.
\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.

\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{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}).

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
option:
\begin{center}\tt
  \begin{tabular}{lll}
    \textrm{Option} & \textrm{Format} \\
    \hline
    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 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 \textsf{WP} plugin 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.
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:

\begin{description}
\item[\tt -wp-cache <mode>] selects the cache mode to use with \textsf{Why-3}
  provers. The default mode is \verb'update' if there is \textsf{WP} session
  available, and \verb+none+ otherwise.  You can also use the environment
  variable \texttt{FRAMAC\_WP\_CACHE} instead.
\item[\tt -wp-cache-dir <dir>] select the directory where cached results are
  stored. By default, the cache is store in the \textsf{WP} session
  directory, when available.
  You can also use the environment variable
  \texttt{FRAMAC\_WP\_CACHEDIR} instead.
\item[\tt -wp-cache-env] gives environment variables the precedence over command line options.
  By default, the command line options take precedence, as usual.
\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 your \textsf{Why-3} 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.

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

A full featured \textsf{OCaml} API is 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 proof report in JSON format.
\end{description}

See sections below for details on the generated report formats.

\clearpage
\subsection{JSON Reports}

The generated JSON report format consists of an array of JSON records, one for
each generated toplevel goal. Each record consists of the following fields,
some of them being optional when indicated:

\begin{description}
\raggedright
\itemsep0pt
\newcommand{\jsarray}[1]{[#1,\ldots]}
\item[\tt "goal":<string>] goal identifier (same as in console report);
\item[\tt "property":<string>] property identifier (see \textsf{Frama-C/Report} documentation);
\item[\tt "file":<string>] source file location;
\item[\tt "line":<number>] source line location;
\item[\tt "axiomatic"?:<string>] axiomatic name (optional);
\item[\tt "function"?:<string>] function name (optional);
\item[\tt "behavior"?:<string>] behavior name (optional, non-default);
\item[\tt "smoke":<boolean>] smoke-tests goal
  (\textbf{warning:} Cf. fields \verb+"verdict"+ and \verb+"passed"+ below);
\item[\tt "verdict":<string>] prover returned status. Can be \verb+"none"+,
  \verb+"valid"+, \verb+"failed"+, \verb+"unknown"+, \verb+"stepout"+ or
  \verb+"timeout"+ (\textbf{warning:} Cf. field \verb+"passed"+ below);
\item[\tt "passed":<boolean>] is \verb+"true"+ when the prover verdict is valid for non-smoke tests,
  or when the prover verdict is \textit{not} valid for smoke tests;
\item[\tt "script"?:<string>] script file, when available (optional);
\item[\tt "tactics"?:<number>] number of tactics involved in the script (optional);
\item[\tt "provers":\jsarray{<prover>}] prover detailed output. Each entry of the array is a record
  that consists of the following fields:
  \begin{description}
  \item[\tt "prover":<string>] prover name (with version, see option \texttt{-wp-prover});
  \item[\tt "time":<number>] prover time, in milliseconds. For \texttt{Qed}
    prover, includes also the total simplification time for other provers and
    tactics that contributes to the goal;
  \item[\tt "success":<number>] number of valid sub-goals the prover contributes to.
  \end{description}
\item[\tt "subgoals"?:<number>] number of associated sub-goals (optional, when more than one);
\item[\tt "proved"?:<number>] number of sub-goals proved (optional, when non-zero);
\item[\tt "failed"?:<number>] number of sub-goals ending with prover failure or failed smoke-tests
  (optional, when non-zero);
\item[\tt "timeout"?:<number>] number of sub-goals ending in timeout or step-out
  (except for smoke-tests) (optional, when non-zero);
\item[\tt "unknown"?:<number>] number of sub-goals with unknown verdict
  (except for smoke-tests) (optional, when non-zero);
\item[\tt "cached"?:<number>] number of cached sub-goals verdicts
  (including \texttt{Qed} proved sub-goals) (optional, when non-zero).
\end{description}

Notice that the JSON report file is printed in compact form without extra space nor indentation,
unless verbose level is greater than 2 or debug level is greater than 1.

\subsection{Template-based Reports}

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+-wp-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