From 1c204eb75bdd4356c5c3dfcc352a7d3948198a76 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 28 Jan 2019 15:23:27 +0100
Subject: [PATCH] [wp] update the doc & changelog
---
src/plugins/wp/Changelog | 2 ++
src/plugins/wp/doc/manual/wp_plugin.tex | 7 ++++++-
2 files changed, 8 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 405600b3263..9ccbe3d1182 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,8 @@
# <Prover>: prover
###############################################################################
+- Wp [2019/28/01] Now -wp-dynamic is set by default (annotation @calls)
+
######################
Plugin WP 18.0 (Argon)
######################
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index 86bdae51f57..6d1d1a3a70c 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -916,7 +916,12 @@ weakest precondition calculus.
and it can generates a large number of verifications for structures
with many (nested) fields (defaults to \texttt{no}).
\item[\tt -wp-(no)-dynamic] handles calls \textit{via} function pointers
- (experimental, default is: \texttt{no}).
+ thanks to the dedicated \verb+@calls f1,...,fn+ code annotation.
+ For each call to a function pointer \texttt{fp}
+ in the instruction or block under the annotaion,
+ \texttt{fp} is required to belongs to the set \texttt{f1,\ldots,fn} and
+ a case analysis is performed with the contract of each provided function
+ (default is: \texttt{yes}).
\end{description}
\subsection{Trigger Generation}
--
GitLab