wp_plugin.tex

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

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

This plug-in computes proof obligations of programs annotated with
\textsf{ACSL} annotations by \emph{weakest precondition calculus},
using a parametrized memory model to represent pointers and heap
values. The proof obligations may then be discharged by external
automated theorem provers such as
\textsf{Alt-Ergo}~\cite{AltErgo2006},
\textsf{CVC4}~\cite{CVC4} and
\textsf{Z3}~\cite{Z3}
or by interactive proof assistants
like \textsf{Coq}~\cite{Coq84} and more generally, any automated or interactive
prover supported by \textsf{Why3}~\cite{Why3}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\subsection{Display Modes}

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

\paragraph{Remark:} the fold/unfold operations only affect the goal display. It does not \emph{transform} the goal to be proven.

The autofocus mode is based on a ring of \emph{focused terms}. Clicking a term of a clause automatically focus this term. Shift-clicking a term adds the term to the focus ring. When autofocus mode is active, only the clauses that contains a \emph{focused} term are displayed. Hidden clauses are mentioned by an ellipsis \texttt{[...]}.

Low-level details of the memory model are normally hidden, and represented by C-like instructions such as:

\begin{ccode}
   Stmt { Label A: a.f[0] = y@Pre; }
\end{ccode}

This reads as follows: a program point is defined by the label \texttt{A}. At this point, the left-value \texttt{a.f[0]} receives the value that variable \texttt{y} holds at label \texttt{Pre}. More generally, \texttt{lv@L} means the value of l-value \texttt{lv} at label \texttt{L:}, and for more complex expression, \texttt{« e »@L} means the expression \texttt{e} evaluated at label \texttt{L}. Redundant labels are removed when possible. This is a short-hand for \textsf{ACSL} notation \lstinline{\at(e,L)} but is generally more readable.

Sometimes, some memory operations can not be rendered as C instructions, typically after transforming a goal so far. In such situations, the memory model encoding might appear with terms like \texttt{µ:Mint@L}.

With memory model unmangled, the encoding in logic formulae is revealed and no label are displayed.

\subsection{Tactics}

The right panel display a palette of tactics to be applied on the current goal. Tooltips are provided to help the user understanding how to configure and run tactics.

Only applicable tactics are displayed, with respect to current term or clause selected. Many tactics can be configured by the user to tune their effect. Click on the tactic button to toggle its control panel. Once a tactic is correctly configured, it can be applied by clicking its « Play » button.

\subsection{Term Composer}

Some tactic require one or several terms to be selected.
In such case, the normal view display the selected term.
It can be edited by buttons in the view, like a \texttt{RPN} calculator. More buttons appear with respect to already selected terms. Numerical constants can be composed, and combined with selected terms.

Typically, the composer displays a stack of values, like for instance:
\begin{ccode}
  A: 45
  B: a[0]@Pre (int)
\end{ccode}

In such a case, the user can select the value \texttt{45} with the \texttt{Select A} button, or add the two numbers with the \texttt{Add A+B} button.

Sometimes, like for the Instance tactic, a \emph{range} of numerical values can be selected. In such a case, when two numbers are selected, a special button \texttt{Select A..B} appears.

The list of all available composer buttons is displayed by the \texttt{Help} button.

A composer worth to be mentioned is \texttt{Destruct}, typically available on complex expressions. It allows to decompose a value into its sub-components. For instance, destructuring the value \texttt{B} above will reveal the address \texttt{« a+0 »@Pre} and memory \texttt{µ:Mint@Pre}.

\subsection{Proof Script}

The top toolbar upon the goal display show the current status of the goal and the number of pending goals. The media buttons allow to navigate in the proof tree.
\begin{quote}
\begin{tabular}{ll}
\verb+Next/Prev:+ & navigate among the list of pending (non proved) sub-goals; \\
\verb+Forward:+ & goes to the next pending sub-goal; \\
\verb+Backward:+ & cancel the current tactic and prover results; \\
\verb+Clear:+ & restart all the interactive proof from the initial goal.
\end{tabular}
\end{quote}

A sketch of current proof is displayed on top of the goal ; each step is clickable to navigate into the proof. Only the path leading to the current node is unfolded.

When all pending sub-goals have been proved, the initial goal is marked proved by \textsf{Tactical} in the goal list panel. It is time to save the script. A button is also available to replay the saved script, if any. Saving and replay are also accessible from the list of goals, in the popup menu of the \texttt{Script} prover column.

\subsection{Replaying Scripts}

Editing scripts interactively allows the user to finish the proofs. Once proofs are saved, he must be able to replay them from the command line. To ease the process, the following options are available to the user:
\begin{quote}
\begin{tabular}{ll}
\verb+-wp-session <dir>+ & to setup a directory where scripts are saved in; \\
\verb+-wp-prover tip+ & for incrementally building and updating the session scripts;\\
\verb+-wp-prover script+ & for replaying saved scripts only, as they are;\\
\end{tabular}
\end{quote}

The \verb+script+ prover only runs the proof scripts edited by the user from the TIP, including the scripts being complete or known to being stuck at some sub-goal. The other proof obligations are transmitted to other provers, if some are provided.

This mode is well suited for replaying a proof bench, by using a combination of provers such as \verb+-wp-prover script,alt-ergo+. Moreover, the \verb+script+ prover never modifies the proof session and the proof scripts.

The \verb+tip+ prover is similar, except that it never runs sub-goals that are known to be stuck but updates the proof scripts on success or when an automated proof fails. Using the \verb+tip+ prover is less time consuming and eventually prepares new scripts for failed proofs to be edited later under the TIP.

Notice that, as soon as you have setup a wp-session directory, you benefit from cache facilities to speedup your proofs. Consult Section~\ref{wp-cache} for details.

\clearpage
A typical proof session consists then in the following stages:

a. Collecting the automated proofs and preparing for the TIP.
\begin{logs}
  frama-c [...] -wp-prover tip,alt-ergo
\end{logs}

This runs all existing scripts (none at the very beginning) in success-mode only, and try Alt-Ergo on the others. Failed proofs lead to new empty scripts created.

b. Running the TIP.
\begin{logs}
  frama-c-gui [...] -wp-prover tip
\end{logs}

This mode only runs existing scripts (typically prepared in the previous phase) in success-mode only, which is quite fast. Finally, the GUI is opened and the user can enter the TIP and edit the proofs.

Most goals are reported not to be proved, because automated proof is deactivated since no other prover than \verb+tip+ is specified. However, by filtering only those proof scripts that requires completion, only the relevant goals appear. The user has to save its edited proof scripts to re-run them later.

Any number of phase a. and b. can be executed and interleaved. This incrementally builds the set of proof scripts that are required to complement the automated proofs.

c. Consolidating the Bench.
\begin{logs}
  frama-c [...] -wp-prover script,alt-ergo
\end{logs}

This mode replays the automated proofs and the interactive ones, re-running Alt-Ergo on every \textsf{WP} goals and every proof tactic sub-goals. The user scripts are never modified — this is a replay mode only.

\subsection{Tracking Scripts}

When working on large verification use-cases, it is common that some proof scripts
become useless because the associated proof obligation does not exist anymore.

WP can track the scripts that are used during verification. For this, one has to
initialize a tracking directory. This is done using the option
\verb+-wp-prepare-scripts+. This command creates a \verb+.marks+ directory in the
proof session scripts directory (that can be configured using \verb+-wp-session+),
if such a directory already exists it is removed and created again.

Then, each time WP uses a proof script, it is marked as used in the \verb+.marks+
directory. In particular, it is then possible to run WP
several times to verify different parts of the code, yet marking the scripts for
all those different parts.

Once one is certain that the entire verification of the use case has been replayed
for marking, the option \verb+-wp-finalize-scripts+ can be used to remove all
orphan scripts and the marking directory. The option \verb+-wp-dry-finalize-scripts+
can be used to log the remove actions instead of actually doing them.

\subsection{Strategies}

Strategies are heuristics that generate a prioritized bunch of tactics to be tried on the current goal.
Few built-in strategies are provided by the \textsf{WP} plug-in ; however, the user can extends the proof editor with
custom ones, as explained in section~\ref{wp-custom-tactics} below.

To run strategies, the interactive proof editor provide a single button \texttt{Strategies} in the tactic panel.
Configure the heuristics you want to include in your try, then click the button. The generated with highest priority is immediately applied. The proof summary now display \texttt{backtrack} buttons revealing proof nodes where alternative tactics are available. You can use those backtracking button to cycle over the generated tactics.

Of course, strategies are meant to be used multiple times, in sequence. Recall that strategies apply highest priority tactic first, on the current goal. When using strategies several times, you shall see several \texttt{backtrack}ing buttons in your proof script. You backtrack from any point at any time.

You shall also alternate strategies \emph{and} manually triggered tactics. Though, strategies are only used to
\emph{infer} or \emph{suggest} interesting tactics to the user. Once your are finished with your proved, only the tactics are saved in the script, not the strategies used to find them. Hence, replaying a script generated with strategies would not involve backtracking any more. The script will directly replay your chosen alternatives.

It is also possible to call strategies from the command line, with option \texttt{-wp-auto}. The strategies are tried up to some depth, and while a limited number of pending goals
remains unproved by \textsf{Qed} or the selected provers. More precisely:
\begin{description}
\item[\tt -wp-auto s,...] applies strategies \texttt{s,...} recursively to unproved goals.
\item[\tt -wp-auto-depth <$n$>] limit recursive application of strategies to depth $n$ (default is 5).
\item[\tt -wp-auto-width <$n$>] limit application of strategies when there is less than $n$ pending goals (default is 10).
\item[\tt -wp-auto-backtrack <$n$>] when the first tried strategies do not close a branch, allows for backtracking
  on $n$ alternative strategies. Backtracking is performed on goals which are closed to the root proof obligation, hence
  performing a kind of width-first search strategy, which tends to be more efficient in practice.
  Backtracking is deactivated by default ($n=0$) and only used when \verb+-wp-auto+ is set.
\end{description}

The name of registered strategies is printed on console by using \texttt{-wp-auto '?'}. Custom strategies can be loaded by plug-ins, see below.

\newcommand{\TACTIC}[2]{#1\quad\quad\triangleright\quad\quad#2}

\subsection{General Tactics}

\paragraph{Absurd} Contradict a Hypothesis\\
The user can select a hypothesis $H$, and change the goal to $\neg H$:

$$ \TACTIC{\Delta,H\models\,G}{\Delta\models\,\neg H} $$

\paragraph{Clear} Remove Hypothesis\\
The user can select a hypothesis $H$, and remove it from the context:

$$ \TACTIC{\Delta,H\models\,G}{\Delta\models\,G} $$

\paragraph{Choice} Select a Goal Alternative\\
When the goal is a disjunction, the user select one alternative and discard the others:
$$ \TACTIC{\Delta\models\,\Gamma,G}{\Delta\models\,G} $$

\paragraph{Compound} Decompose compound equalities\\
When the user select an equality between two records, it is decomposed field by field.

$$ \TACTIC{ a = b }{ \bigwedge a.f_i = b.f_i } $$

\paragraph{Contrapose} Swap and Negate Hypothesis with Conclusion\\
The user select a hypothesis (typically, a negation) and swap it with the goal.
$$ \TACTIC{\Delta,H\models\,G}{\Delta,\neg G\models\,\neg H} $$

\paragraph{Cut} Use Intermediate Hypothesis
The user introduce a new clause $C$ with the composer to prove the goal. There two variants of the tactic, made available by a menu in the tactic panel.

The \textsf{Modus-Ponens} variant where the clause $C$ is used as an intermediate proof step:

$$\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta &\models C \\
\Delta,C &\models G
\end{array}} $$

And the \textsf{Case Analysis} variant where the clause $C$ is used with a split:
$$\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,\phantom{\neg}C \models G \\
\Delta,\neg C \models G
\end{array}} $$

\paragraph{Definition} Unfold predicate and logic function definition\\
The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available.

\paragraph{Filter} Dependent Erasure of Hypotheses \\
The tactic is always applicable. It removes hypotheses from the goal on a
variable used basis. When variables are compounds (record and arrays) a finer
heuristic is used to detect which parts of the variable is relevant. A
transitive closure of dependencies is also used. However, it is always
possible that too many hypotheses are removed.

The tactic also have a variant where only hypotheses \emph{not relevant} to the
goal are retained. This is useful to find absurd hypotheses that are completely
disjoint from the goal.

\paragraph{Instance} Instantiate properties\\
The user selects a hypothesis with one or several $\forall$ quantifiers, or an $\exists$ quantified goal. Then, with the composer, the use choose to instantiate one or several of the quantified parameters. In case of $\forall$ quantifier over integer, a range of values can be instantiated instead.

When instantiating hypothesis with an expression $e$:
$$\TACTIC{\Delta,\,\forall x\, P(x)\models G}{\Delta,P(e)\models G}$$

When instantiating with a range of values $n\ldots m$:
$$\TACTIC{\Delta,\,\forall x\, P(x)\models G}{\Delta,P(n)\ldots P(m)\models G}$$

When instantiating a goal with an expression $e$:
$$\TACTIC{\Delta\models \exists x\,G(x)}{\Delta\models G(e)}$$

\paragraph{Intuition} Decompose with Conjunctive/Disjunctive Normal Form\\
The user can select a hypothesis or a goal with nested conjunctions and disjunctions. The tactics then computes the conjunctive or disjunctive normal form of the selection and split the goal accordingly.

\paragraph{Lemma} Search \& Instantiate Lemma\\
The user start by selecting a term in the goal. Then, the search button in the tactic panel will display a list of lemma related to the term. Then, he can instantiate the parameters of the lemma, like with the Instance tactic.

\paragraph{Rewrite} Replace Terms\\
This tactic uses an equality in a hypothesis to replace each occurrence of term by another one.
The tactic exists with two variants: the left-variant which rewrites $a$ into $b$ from equality $a=b$,
and the right-variant which rewrites $b$ into $a$ from equality $a=b$.
The original equality hypothesis is removed from the goal.

$$\TACTIC{\Delta,a=b\models\,G}{\Delta[a\leftarrow b]\models\,G[a\leftarrow b]}$$

\paragraph{Split} Decompose Logical Connectives and Conditionals\\
This is the most versatile available tactic. It decompose merely any logical operator following the sequent calculus rules. Typically:

\[
\begin{array}{c@{\quad\quad}c@{\quad\quad}c}
  \Delta,(H_1\vee H_2)\models G & \triangleright &
     \Delta,H_1 \models G \\
  && \Delta,H_2 \models G \\
  \Delta\models(G_1\wedge G_2) & \triangleright &
     \Delta\models G_1 \\
  && \Delta\models G_2 \\
  \Delta,H?P:Q\models G & \triangleright &
     \Delta,\phantom{\neg}H,P\models G \\
  && \Delta,\neg H,Q\models G \\
  \ldots
\end{array}
\]

When the user selects a arbitrary boolean expression $e$, the tactic is similar to the Cut one:
\[\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{l}
\Delta,\phantom{\neg}e\models G \\
\Delta,\neg e\models G
\end{array}} \]

Finally, when the user select a arithmetic comparison over $a$ and $b$,
the tactics makes a split over $a=b$, $a<b$ and $a>b$:
\[\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,a<b&\models G \\
\Delta,a=b&\models G \\
\Delta,a>b&\models G
\end{array}} \]

\subsection{Integers \& Bit-wised Tactics}

\paragraph{BitRange} Range of logical bitwise operators \\
This tactical applies the two following lemmas to the current goal.
The first lemma is on logical-or, and only applies to positive integers:
\[
\begin{array}{c}
  \bigwedge_i 0 \leq x_i < 2^p
  \\\hline
  0 \leq \mathtt{lor}(x_1,\ldots,x_n) \leq 2^p
\end{array}
\]

The second lemma is on logical-and, and applies to at-least one positive integer:
\[
\begin{array}{c}
  \bigvee_i 0 \leq x_i \quad\wedge\quad \bigwedge_i x_i \leq 2^p
  \\\hline
  0 \leq \mathtt{land}(x_1,\ldots,x_n) \leq 2^p
\end{array}
\]

The tactical rewrites range goals on logical and/or into the corresponding range over its parameters, by finding a suitable $2^p$
to apply the theorems. Such a strategy is \emph{not} complete in general.
Typically, $\mathtt{land}(x,y) < 38$ is true whenever both $x$ and $y$ are in range $0\ldots 31$, but this is also true
in other cases.

\paragraph{Bit-Test Range} Tighten bounds with respect to bits \\
The \lstinline{bit_test(a,b)} function is predefined in \textsf{WP} and is equivalent
to the \textsf{ACSL} expression \lstinline{(a & (1 << k)) != 0}. The
\textsf{Qed} engine has many simplification rules that applies to
such patterns.

The user selects an expression $\mathtt{bit\_test}(n,k)$ with $k$
a \emph{constant} integer value greater or equal to 0 and lower than
128. The tactic uses this test to thighten the bounds of $n$.

$$\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,T &\models G \\
\Delta,F &\models G
\end{array}} $$

with
$$\begin{array}[t]{rlcll}
  T \equiv & \mathtt{bit\_test}(n,k) & \wedge & (0 \leq n & \Rightarrow 2^{k} \leq n) \\
  F \equiv & \neg \mathtt{bit\_test}(n,k) & \wedge & (0 \leq n < 2^{k+1} & \Rightarrow n < 2^{k})
  \end{array}
$$

\paragraph{Bitwise} Decompose equalities over $N$-bits\\
The use selects an integer equality and a number of bits.
Providing the two members of the equality are in range $0..2^N-1$,
the equality is decomposed into $N$ bit-tests equalities:
\[\TACTIC{\Delta\models G}{%
\begin{array}[t]{rcl}
\Delta\phantom{)} &\models & 0 \leq a,b < 2^N \\
\sigma(\Delta) & \models & \sigma(G)
\end{array}
}\]
where $\sigma$ is the following subsitution:
\[ \sigma \equiv
\left[ a=b \quad \leftarrow
\bigwedge_{k\in 0..N-1} \mathtt{bit\_test}(a,k) = \mathtt{bit\_test}(b,k)
\right]
\]

\paragraph{Congruence} Simplify Divisions and Products \\
This tactic rewrites integer comparisons involving products and divisions.
The tactic applies one of the following theorems to the current goal.
In the following lemmas, $k$, $k'$, and $n$ are integer constants, $a$ and $b$ any integer terms.
The notation $k|n$ stands for $k$ divides $n$.
The lemmas are extended to non-strict inequalities and non-positive constants in a natural way.
\[
\begin{array}{crcl}
0<k, & a < n/k &\Longrightarrow& k.a < n \\
k|n, & a = n/k &\Longleftrightarrow& k.a = n \\
\neg(k|n), & k.a = n & \Longrightarrow & \mathtt{false} \\
0<k, & a < k.(b+1) &\Longrightarrow& a/k < b \\
0<k, 0<k', & k'.a < k.b &\Longrightarrow& a/k < b/k' \\
n|k, n|k', & (k/n).a = (k'/n).b &\Longleftrightarrow& k.a = k'.b
\end{array}
\]

\paragraph{Induction} Start a proof by integer induction \\
The user select any integer expression $e$ in the proof and a base value $b$ (which defaults to
0). The tactic generates a proof by induction on $e$, that is, the base case
$e = b$ and then the cases $e < b$ and $b < e$. Formally, the initial goal
$\Delta_0\models\,G_0$ is first generalized into $\Delta,P(e)\models\,Q(e)$. The tactic
then proceed by (strong) induction over $n$ for
$G(n) \equiv P(n)\Longrightarrow\,Q(n)$:

\[\TACTIC{\Delta\models\,G(n)}{%
\begin{array}[t]{lll}
\Delta,\; \quad n = b & \models G(n) \\
\Delta,\; \forall i,\, b \leq i < n \Longrightarrow G(i) \; & \models G(n) \\
\Delta,\; \forall i,\, n < i \leq b \Longrightarrow G(i) \; & \models G(n)
\end{array}} \]

\paragraph{Mod-Mask} Rewrite bitmask into/from modulo \\
This tactic is used to rewrite a bitmask into a modulo (or a modulo into a
bitmask) when possible. The user selects an expression $e$ of the form
$b \% m$ (resp. $b \& m$ - $\texttt{land b m}$) than can be rewritten into
$b \& (m+1)$ (resp. $b \% (m - 1)$), if $0 \leq b$ and $m$ is a positive power
of 2 (resp. $m + 1$ is a positive power of 2). When selecting an expression
$x \& y$, both directions $x \% (y - 1)$ and $y \% (x - 1)$ can be considered.

Since establishing that $m$ is a positive power of 2 can be hard, the tactic has
several behaviors. If \textsf{Qed} can prove immediately that an operand $m$ (or
$m+1$ for bitmaks) is a positive power of 2, the tactic only generates the guard
$0 \leq b$ and the rewritten goal. If it is not the case, the tactic appears
with the name ``Mod-Mask (hard)'' in the GUI. In this situation, the guard
consists of two conditions: $0 \leq b$ and $m$ (or $m+1$) is a positive power of
2. This guard involves an existential quantification, so it can be hard to
prove. When the selected term is a bitmask, the tactic cannot decide itself the
direction of the modulo, thus a checkbox is added in the configuration of the
tactic to select the direction of rewriting.

\paragraph{Overflow} Integer Conversions \\
This tactic split machine integer conversions into three cases: value in integer
range, lower than range and upper than range. The tactic applies on expression
with pattern $\mathtt{to\_iota(e)}$ where \texttt{iota} is a machine-integer type
name, \emph{eg.} \texttt{to\_uint32}.

\[\TACTIC{\Delta\models G}{%
\begin{array}[t]{rcl}
\sigma_{id}(\Delta) & \models & low \leq e \leq up \Rightarrow \sigma_{id}(G) \\
\sigma_{+}(\Delta) & \models & low < e \Rightarrow \sigma_{+}(G) \\
\sigma_{-}(\Delta) & \models & e < up \Rightarrow \sigma_{-}(G)
\end{array}
}\]
where
\begin{itemize}
  \item $[low..up]$ is the range of the \texttt{iota} integer domain,
  \item $\sigma_{id} = [ \mathtt{to\_iota}(e) \mapsto e ]$,
  \item $\sigma_{+}  = [ \mathtt{to\_iota}(e) \mapsto \mathtt{overflow}(e) ]$,
  \item $\sigma_{-}  = [ \mathtt{to\_iota}(e) \mapsto \mathtt{overflow}(e) ]$.
\end{itemize}

\paragraph{Range} Enumerate a range of values for an integer term\\
The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $e<a$ and $e>b$:
$$\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,e<a &\models G \\
\Delta,e=a &\models G \\
&\vdots \\
\Delta,e=b &\models G \\
\Delta,e>b &\models G
\end{array}} $$

\paragraph{Shift} Transform logical shifts into arithmetics\\
For positive integers, logical shifts such as \lstinline{a << k}
and \lstinline{a >> k} where \lstinline$k$ is a constant can be interpreted into a multiplication or a division by $2^k$.

When selecting a logical-shift, the tactic performs:
\[\TACTIC{\Delta\models G}{%
\begin{array}[t]{rcl}
\Delta\phantom{)} &\models& 0 \leq a \\
\sigma(\Delta) &\models& \sigma(G)
\end{array}
}\]
where:
\begin{tabular}[t]{ll}
$\sigma = [ \mathtt{lsl}(a,k) \leftarrow a * 2^k ]$ &
for left-shift, \\
$\sigma = [ \mathtt{lsr}(a,k) \leftarrow a / 2^k ]$ &
for right-shifts.
\end{tabular}

\subsection{Domain Specific Tactics}

\paragraph{Array} Decompose array access-update patterns\\
The use select an expression $e\equiv a[k_1\mapsto v][k_2]$. Then:

\[
\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,\,k_1=k_2,\,e = v &\models G \\
\Delta,\,k_1\neq k_2,\,e = a[k_2] &\models G
\end{array}
}\]

\paragraph{Havoc} Go Through Assigns \\
This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predicate generate by complex assigns clause. The user select an address, and if the address is not assigned by the \texttt{Havoc} clause, the memory at this address is unchanged.

\paragraph{Separated} Expand Separation Cases\\
This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.


\paragraph{Sequence} Unroll repeat-sequence operator\\
In this section, let us use $A^n$ for the ACSL notation \lstinline{A *^ n},
the repeat list operation, and $A \oplus l$ for the list concatenation.

This tactics is used to transform $A^n$ sequences. Threes behaviors
can be selected:
unroll left that rewrites the list  $A^n$ into $A \oplus A^{n-1}$,
unroll right that rewrites the list $A^n$ into $A^{n-1} \oplus A$
and unroll sum that rewrites the list $A ^{n_1 + ... + n_k}$
into $A^{n_1} \oplus ... \oplus A^{n_k}$. For unroll left and right,
a negative value leads to an empty list. For unroll sum, one must prove that all
$nI$ are positive.

Rule for unroll left:

\[
\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{lll}
  \Delta[A^n\leftarrow A \oplus A^{n-1}],& n > 0 & \models G[A^n\leftarrow A \oplus A^{n-1}]\\
  \Delta[A^n\leftarrow []],& n \leq 0 & \models G[A^n\leftarrow []]
\end{array}
}\]

Rule for unroll right:

\[
\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{lll}
  \Delta[A^n\leftarrow A^{n-1} \oplus A],& n > 0 & \models G[A^n\leftarrow A^{n-1} \oplus A]\\
  \Delta[A^n\leftarrow []],& n \leq 0 & \models G[A^n\leftarrow []]
\end{array}
}\]

Rule for unroll sum:

\[
\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
  \Delta & \models\bigwedge_{i=1}^{k} 0 \leq n_i\\
  &\\
  \Delta[A^{\sum_{i=1}^{k}n_i}\leftarrow \bigoplus_{i=1}^{k} A^{n_i}] &
  \models G[A^{\sum_{i=1}^{k}n_i}\leftarrow \bigoplus_{i=1}^{k} A^{n_i}]
\end{array}
}\]

\paragraph{Validity} Unfold validity and range definitions\\
The user selects a validity expression (\lstinline{valid_rd},
\lstinline{valid_rw}, \lstinline{invalid} or \lstinline{included}).
The expression is unfolded to a \textsf{Qed} term.


\subsection{Custom Tactics and Strategies}
\label{wp-custom-tactics}

The proof editor and script runner can be extended by loading additional plug-ins. These plug-ins are regular OCaml files to be loaded with the kernel \texttt{-load-module} option. They will be compiled by \textsf{Frama-C} against its API. The \textsf{WP} plug-in exports a rich API to extend the proof editor with new tactics, strategies, and even term-composer tools.

It is not possible to reproduce here the complete API ; it is better to use the automatically generated HTML documentation from \textsf{WP}'s sources. We only provide here a quick tour of this API, as a tutorial on how to implement a basic custom strategy.

The main extension points of the \textsf{WP} plug-in's API are the following ones:
\begin{center}
    \begin{tabular}{ll}
    \hline
    \texttt{Wp.Tactical.tactical} & Base-class definition of custom Tactic. \\
    \texttt{Wp.Strategy.heuristic} & Base-class definition of custom Strategy. \\
    \hline
    \texttt{Wp.Auto.$\star$} & Pre-defined tactics and strategies. \\
    \texttt{Wp.Tactical.register} & Registration point for custom Tactics. \\
    \texttt{Wp.Strategy.register} & Registration point for custom Strategies. \\
    \texttt{Wp.Tactical.add\_composer} & Registration point for custom term composer. \\
    \hline
    \end{tabular}
\end{center}

\paragraph{Warning:} It is technically possible to break the logical soundness of \textsf{WP} when using custom tactics crafted by hand. Fortunately, using only pre-defined tactics in custom strategies will be always safe, even if your heuristic generates crazily stupid alternatives to solve a goal. The point with custom \emph{tactics} is that you might transform a sequent \emph{without preserving} the equivalence with the original goal if you make some mistakes into your custom code. This is the same problem as using \textsf{ACSL} axioms instead of lemmas. So, use custom tactics carefully, and prefer custom strategies when possible.

To build a custom strategy, the typical boilerplate code is as follows:
\begin{lstlisting}[language=ocaml]
 (* file: dummy.ml *)
open Wp

class dummy : Strategy.heuristic =
object
    method id = "MyStrategy.dummy" (* required, must be unique *)
    method title = "Split Goal"    (* visible in Strategy panel *)
    method descr = "Simply split conjunctions in goal" (* idem *)
    method search push sequent = (* heuristic code *)
      let goal = snd sequent in
      match Repr.pred goal with
      | And _ ->
          let selection = Tactical.(Clause(Goal goal)) in
          push (Auto.split ~priority:2.0 selection)
      | _ -> ()
end

(* Register the strategy *)
let () = Strategy.register (new dummy)
\end{lstlisting}

Then, simply extend your command line with the following options to make your strategy available from the interactive proof editor:
\begin{logs}
> frama-c-gui -load-module dummy.ml [...]
\end{logs}

\paragraph{Note:} Loading custom strategies is only required when running the graphical user interface (\texttt{frama-c-gui}). When replaying scripts from the command line (\texttt{frama-c}), only custom tactics and custom composers actually involved in proofs are required to be loaded.

The example custom strategy above is structured as follows. First we open the module \lstinline$Wp$ to simplify
access to the API. A custom strategy must be an instance of class-type \lstinline$Strategy.heuristic$, and we use a coercion here to explicit types. Methods \lstinline$#id$, \lstinline$#title$ and \lstinline$#descr$ are required and describes the strategy, making it available from the tactic panel in the graphical user interface.

The actual heuristic code takes place in method \lstinline$#search$ which has the following type (consult the html API for details):
\begin{lstlisting}[language=ocaml]
    method search : (Strategy.strategy -> unit) -> Conditions.sequent -> unit
\end{lstlisting}

This method takes two parameters: a strategy registration callback and the sequent to prove. Each heuristic
is supposed to register any number of strategies to be tried on the provided sequent. In turn, each strategy
is a record consisting of a priority, a tactic, a target selection for the tactic and its arguments.
It is possible to build such a record by hand, using custom or predefined tactics. However, it is much more convenient
to use the helper functions from module \lstinline$Auto$ that directly build strategies.

In the example above, we inspect the structure of the goal, and when a conjunction is detected (\lstinline$And _$),
we decide to register a split tactic, thanks to the helper function \lstinline$Auto.split$. Default priority is \lstinline$1.0$ by convention. Pre-installed strategies would only use range $[0.5\ldots2.0]$ of priorities. You can use any value you want inside or outside this range. In the example below, we assign a high priority to the split of goal conjunctions, meaning that such a split should be tried first.

\paragraph{Using Selections.} Tactics always need a \lstinline$selection$ target. Moreover, some tactics require additional parameters, also to be provided as \lstinline$selection$ values. Typically, consider the \lstinline$Auto.range$ tactic:

\begin{lstlisting}{language=ocaml}
   val Auto.range : ?priority:float -> selection -> vmin:int -> vmax:int -> strategy
\end{lstlisting}

Here the selection argument shall targets the expression to be enumerated in range \lstinline$vmin..vmax$.
Selections must refer to a term that pre-exists in the sequent. You must indicate to the \textsf{WP} proof engine
how to rebuild this term from the sequent. Hence, if the \textsf{C}-code or the \textsf{ACSL} specification change,
\textsf{WP} still has a chance to rebuild the same selection from the updated sequent.

Selections are easy to build. There are five basic forms, as described below:
\begin{lstlisting}[language=ocaml]
   type Tactical.selection =
     | Empty (** no selection *)
     | Clause of clause (** selects a full hypothesis or the full goal *)
     | Inside of clause * Lang.F.term (** selects a sub-term of a hypothesis or goal *)
     | Compose of compose (** a calculus from several sub-selections *)
   and Tactical.clause =
     | Goal of Lang.F.pred
     | Step of Conditions.step
\end{lstlisting}

It is also possible to build selections from sequent by explicit lookup:
\begin{lstlisting}[language=ocaml]
   val Strategy.select_e : Conditions.sequent -> Lang.F.term -> Tactical.selection
   val Strategy.select_p : Conditions.sequent -> Lang.F.pred -> Tactical.selection
\end{lstlisting}

Composition allows you to build new terms from existing ones, like when using the term composer from the graphical user interface. You access composers by their name, like in the term composer. The API for building new terms is as follows:
\begin{lstlisting}[language=ocaml]
   val Tactical.int : int -> Tactical.selection
   val Tactical.cint : Integer.t -> Tactical.selection
   val Tactical.range : int -> int -> Tactical.selection
   val Tactical.compose : string -> Tactical.selection list -> Tactical.selection
\end{lstlisting}

For instance, provided you have two selected terms \lstinline$a$ and \lstinline$b$, you can build their sum using
\lstinline$compose "wp:add" [a;b]$. The name of composers can be obtained from the graphical user interface.

\paragraph{Exploring Sequents.}
The clauses refer to parts of the provided sequent. Typically, a sequent consists of a
sequence of hypothesis, and a goal to prove. Each hypothesis is represented by a \lstinline$step$, consisting either of single hypothesis or a more structured condition
(branch, cases, \textit{etc}.):

\begin{lstlisting}[language=ocaml]
   type Conditions.sequent = sequence * Lang.F.pred
   and  sequence = .... step list ... (* private type *)
   and  step = { condition : condition ; ... }
   and  condition =
           | Have of Lang.F.pred (** hypothesis *)
           | Init of Lang.F.pred (** C-initializer initialization clause *)
           | Type of Lang.F.pred (** C/ACSL type constraints *)
           | Core of Lang.F.pred (** Common hypothesis factorization from WP *)
           | When of Lang.F.pred (** hypothesis from tactical or simplification *)
           | Branch of Lang.F.pred * sequence * sequence (** If-Then-Else *)
           | Either of sequence list (** Disjunction of Cases *)
   val iter : (step -> unit) -> sequence -> unit
\end{lstlisting}

When you walk through a sequence of hypothesis, you shall reuse the provided steps to build clauses and selections.

\paragraph{Exploring Formulae}.
The constituent of hypothesis and goals are logical terms and predicates. You shall use
module \lstinline$Repr.term$ and \lstinline$Repr.pred$ to access the internal representation
of formulae. There are many constructors for terms and predicates, simply browse the html documentation to have an overview. Many properties about terms and predicates are directly obtained from the \lstinline$Lang.F$ module. The API is quite rich, so use the html documentation to get details.

\clearpage
%-----------------------------------------------------------------------------
\section{Command Line Options}
\label{wp-cmdline}
%-----------------------------------------------------------------------------

The best way to know which options are available is to use:
\begin{shell}
# frama-c -wp-help
\end{shell}

The \textsf{WP} plug-in generally operates in three steps:
\begin{enumerate}
\item Annotations are selected to produce a control-flow graph of
  elementary statements annotated with hypotheses and goals.
\item Weakest preconditions are computed for all selected goals in the
  control-flow graph. Proof obligations are emitted and saved on disk.
\item Decision procedures (provers) are run to discharge proof obligations.
\end{enumerate}

The \textsf{WP} options allow to refine each step of this process. It
is very convenient to use them together with the standard \texttt{-then}
option of \textsf{Frama-C}, in order to operate successive passes on the project.
See section~\ref{wp-persistent} for details.

\subsection{Goal Selection}

This group of options refines the selection of annotations for which
proof obligations are generated. By default, all annotations are
selected. A property which is already proved -- by \textsf{WP} or by
any other plug-in -- does not lead to any proof-obligation generation,
unless the property is individually selected from the graphical user
interface of the programmatic API.

\begin{description}
\item [\tt -wp] generates proof obligations for all (selected) properties.
\item [\tt -wp-fct <f$_1$,...,f$_n$>] selects annotations of functions
  \texttt{f$_1$},...,\texttt{f$_n$} (defaults to all functions).
\item [\tt -wp-skip-fct <f$_1$,...,f$_n$>] ignores
  functions \texttt{f$_1$},...,\texttt{f$_n$} (defaults to none).
\item [\tt -wp-bhv <b$_1$,...,b$_n$>] selects annotations for behaviors
  \texttt{b$_1$},...\texttt{b$_n$} (defaults to all behaviors) of the
  selected functions (the name \texttt{default!} can be used to select
  the default anonymous behavior).
\item [\tt -wp-prop <p$_1$,...,p$_n$>] selects properties having
  \texttt{p$_1$} or ...\texttt{p$_n$} as tagname (defaults to all
  properties). You may also replace a tagname by a
    \texttt{@<category>} of properties.
    \\
    Recognized categories are: \texttt{@lemma}, \texttt{@requires}, \texttt{@assigns},
    \texttt{@ensures}, \texttt{@exits}, \texttt{@assert}, \texttt{@check},
    \texttt{@invariant}, \texttt{@variant}, \texttt{@breaks},
    \texttt{@continues}, \texttt{@returns}, \texttt{@terminates},\\
    \texttt{@decreases},
    \texttt{\mbox{@complete\_behaviors}}, \texttt{\mbox{@disjoint\_behaviors}}.
    \\
    Properties can be prefixed with a minus sign to \emph{skip} the associated annotations.
    For example \texttt{-wp-prop="-@assigns"} removes all \texttt{assigns}
    and \texttt{loop assigns} properties from the selection.
    \\
    \textbf{Remark:} properties with name \verb+no_wp:+ are always and automatically
    filtered and never proved by \textsf{WP}.
\item [\tt -wp-(no)-status-all] includes in the goal selection all properties
  regardless of their current status (default is: \texttt{no}).
\item [\tt -wp-(no)-status-valid] includes in the goal selection those properties
  for which the current status is already 'valid' (default is: \texttt{no}).
\item [\tt -wp-(no)-status-invalid] includes in the goal selection those properties
  for which the current status is already 'invalid' (default is: \texttt{no}).
\item [\tt -wp-(no)-status-maybe] includes in the goal selection those properties with
  an undetermined status (default is: \texttt{yes}).
\item [\tt -wp-(no)-legacy] use the legacy WP generator, if set to \texttt{no},
  WP uses a recently developed generator (default is: \texttt{no}).
\item [\tt -wp-dump] does not prove selected properties, but dumps the control
  flow graph computed by WP, including code annotations, both DOT files and PDF
  files into the directory specified by \texttt{-wp-out}.
\end{description}

\textbf{Remark:} options \texttt{-wp-status-xxx} are not taken into account
when selecting a property by its name or from the GUI.

\subsection{Program Entry Point}

The generic \textsf{Frama-C} options dealing with program entry point
are taken into account by \textsf{WP} plug-in as follows:

\begin{description}
\item [\tt -main <f>] designates \texttt{f} to be the main entry point (defaults to \texttt{main}).
\item [\tt -lib-entry] the main entry point (as defined by option
\texttt{-main}) is analyzed regardless of its initial context (default is no).
\end{description}

These options impact the generation of proof-obligations for the
``\texttt{requires}'' contract of the main entry point. More precisely, if there
is a main entry point, \emph{and} \texttt{-lib-entry} is not set:
\begin{itemize}
\item the global variables are set to their initial values at the
  beginning of the main entry point for all its properties to be established;
\item special proof obligations are generated for the preconditions of the
  main entry point, hence to be proved with globals properly initialized.
\end{itemize}

Otherwise, initial values for globals are not taken into account and
no proof obligation is generated for preconditions of the main entry
point.

\subsection{Model Selection}
These options modify the underlying memory model that is used for
computing weakest preconditions. See chapter~\ref{wp-models} for
details. Models are identified by a combination of \emph{selectors}
which are defined below:
\begin{center}
  \begin{tabular}{cl}
    Selector & Description \\
    \hline
    \texttt{\bf Hoare} & Select Hoare memory model. \\
    \texttt{\bf Typed} & Select Typed memory model with limited casts.\\
    \texttt{cast}  & Select Typed memory model with unlimited casts (unsound). \\
    \texttt{nocast} & Select Typed memory model with \emph{no} casts. \\
    \hline
    \texttt{raw} & Disable the combination of memory models. \\
    \texttt{var} & Combination of memory models based on variable analysis. \\
    \texttt{ref} & Activate the detection of pointer variables used for reference passing style. \\
    \texttt{caveat} & Caveat memory model (see~\ref{CAVEAT}). \\
    \hline
    \texttt{int} & Use machine integers when overflows and downcasts might occurs. \\
    \texttt{nat} & Integer model without bounds (no overflow assumed). \\
    \hline
    \texttt{float} & Use floating-point operations. \\
    \texttt{real} & Use mathematical reals instead of floating point. \\
    \hline
  \end{tabular}
\end{center}

Refer to Section~\ref{wp-model-arith} for details on arithmetic models and
Chapter~\ref{wp-models} for a description of memory models.

The available \textsf{WP} command-line options related to model selection are:
\begin{description}
\item[\tt -wp-model <spec...>] specifies the models to use. The
  specification is a list of \emph{selectors}. Selectors are usually
  separated by `\verb|,|' although other separators are accepted as well:
  `\verb|+|', `\verb|_|', spaces, newlines, tabs and parentheses `\verb|(|',
  `\verb|)|'.\\ Selectors are \emph{case insensitive}. The option
  \texttt{-wp-model} can be used several times. All provided selectors
  are processed from left to right, possibly canceling previous ones.\\
  Default setting corresponds to \texttt{-wp-model "Typed+var+int+float"}.

\item[\tt -warn-(un)signed-(overflow|downcast)] those kernel options are
  used by the (default) arithmetic model \texttt{-wp-model +int} to interpret integer
  arithmetic. See section~\ref{wp-model-arith} for details.

\item[\tt -wp-literals] exports the contents of string literals
  to provers (default: \texttt{no}).
\item[\tt -wp-extern-arrays] gives an arbitrary large size to arrays
  with no dimensions. This is a model of infinite size arrays
  (default is: \texttt{no}).
\item[\tt -wp-(alias|unalias|ref|context)-vars <var,...>] these options can be used
  to finely tweak the memory model inferred by \textsf{WP}. Each variable with a given name
  can be forced to be modeled as follows:\\[1ex]
  \begin{tabular}{rl}
      \texttt{alias}: & the variable is known to have aliases and modeled by \texttt{Typed}.\\
      \texttt{noalias}: & the variable is known to have \emph{no} alias and modeled with \texttt{Hoare}.\\
      \texttt{ref}: & the variable is a constant pointer and is modeled by the \texttt{Ref}.\\
      \texttt{context}: & the variable is initially non-aliased and uses a fresh global in \texttt{Typed}.\\
  \end{tabular}
\item[\tt -wp-(no)-alias-init] Use initializers for aliasing propagation (default is: yes).
\item[\tt -wp-(no)-volatile] this option (de)activate the correct handling of
  volatile access. By default, accessing a volatile l-value returns an undefined
  value, and writing to a volatile l-value is modeled like an \textsf{ACSL} assigns clause.
  Hence, only the accessed \emph{values} are ignored.\\
  Setting \texttt{-wp-no-volatile} turns this behavior off: it is potentially \emph{unsound} and
  makes the \textsf{WP} emitting a warning on each volatile access.
\item[\tt -wp-(no)-warn-memory-model] this option (de)activate the
  warnings about memory model hypotheses
  for the generated proof obligations, as described in Section~\ref{wp-model-hypotheses}.
  For each model supporting this feature, and each concerned function,
  an \textsf{ACSL} specification is printed on output.
  Currently, only the \texttt{Caveat}, \texttt{Typed} and \texttt{Ref} memory models support
  this feature. See also experimental option below.
\item[\tt -wp-(no)-check-memory-model] this \emph{experimental} option generates
  ACSL contracts for the selected memory model hypotheses, as described
  in Section~\ref{wp-model-hypotheses} and listed by option
  \texttt{-wp-warn-memory-model}.
  Hence, the memory model hypothes are exposed to \textsf{WP} and other plugins.
  Disabled by default.
\end{description}

\subsection{Computation Strategy}

These options modify the way proof obligations are generated during
weakest precondition calculus.

\begin{description}
\item[\tt -wp-(no)-rte] generates RTE guards before computing weakest
  preconditions. This option calls the \emph{rte generation} plug-in
  before generating proof obligations.
  The generated guards, when proved\footnote{It is still correct to prove these RTE
    annotations with the \textsf{WP} plug-in.}, fulfill the requirements for
  using the \textsf{WP} plug-in with the default machine-integer domain (default is: \texttt{no}).
  Using this option with \texttt{-wp-model nat} is tricky, because \texttt{rte} uses the kernel options
  to generate guards, and they might be not strong enough to meet the natural model requirements.