Skip to content
Snippets Groups Projects
Commit 32c5233e authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp/doc] new behavior for -wp-unfold-assigns

parent e4f74d2c
No related branches found
No related tags found
No related merge requests found
...@@ -24,6 +24,9 @@ ...@@ -24,6 +24,9 @@
Plugin WP <next-release> Plugin WP <next-release>
######################### #########################
- WP [2020-00-00] Option -wp-unfold-assigns is now parameterized by
a max unfold depth and can unfold assigned ranges
(typically arrays)
-* WP [2020-01-20] Fixes opaque structures handling -* WP [2020-01-20] Fixes opaque structures handling
- TIP [2020-11-06] New tactic: Sequence unrolling - TIP [2020-11-06] New tactic: Sequence unrolling
- TIP [2020-11-05] New tactic: Induction - TIP [2020-11-05] New tactic: Induction
......
...@@ -956,12 +956,16 @@ weakest precondition calculus. ...@@ -956,12 +956,16 @@ weakest precondition calculus.
a call (default is: \texttt{yes}). a call (default is: \texttt{yes}).
\item[\tt -wp-(no)-precond-weakening] discard pre-conditions of side behaviours (sound but \item[\tt -wp-(no)-precond-weakening] discard pre-conditions of side behaviours (sound but
incomplete optimisation, default is: \texttt{no}). incomplete optimisation, default is: \texttt{no}).
\item[\tt -wp-(no)-unfold-assigns] prove assigns goal of \texttt{struct} \item[\tt -wp-unfold-assigns <{\it n}>] when proving assigns, unfold up to
compound types field by field. This allows for proving that assigning \textit{n} levels of \texttt{struct} compounds types or access via ranges.
a complete structure is still included into an assignment field by field. \texttt{struct} are unfolded field by field, ranges are unfolded cell by
This option is not set by default, because it is generally not necessary cell (via a universal quantification over the index of the cell).
and it can generates a large number of verifications for structures This allows for proving that assigning a complete structure is still included
with many (nested) fields (defaults to \texttt{no}). 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)-dynamic] handles calls \textit{via} function pointers \item[\tt -wp-(no)-dynamic] handles calls \textit{via} function pointers
thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}). thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}).
\end{description} \end{description}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment