From 32c5233e7e0e59685af82ca74c5558ca5184b763 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 22 Jan 2021 13:40:12 +0100
Subject: [PATCH] [wp/doc] new behavior for -wp-unfold-assigns
---
src/plugins/wp/Changelog | 3 +++
src/plugins/wp/doc/manual/wp_plugin.tex | 16 ++++++++++------
2 files changed, 13 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index d63682d5417..67da155340b 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,6 +24,9 @@
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
- TIP [2020-11-06] New tactic: Sequence unrolling
- TIP [2020-11-05] New tactic: Induction
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 2b8883193da..c44452f15e1 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -956,12 +956,16 @@ weakest precondition calculus.
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-(no)-unfold-assigns] prove assigns goal of \texttt{struct}
- compound types field by field. This allows for proving that assigning
- a complete structure is still included into an assignment field by field.
- This option is not set by default, because it is generally not necessary
- and it can generates a large number of verifications for structures
- with many (nested) fields (defaults to \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)-dynamic] handles calls \textit{via} function pointers
thanks to the dedicated \verb+@calls f1,...,fn+ code annotation (default is: \texttt{yes}).
\end{description}
--
GitLab