diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog index 405600b3263fe6ba89283519d2f9b81372e9c413..9ccbe3d1182b42ad6f3da8cb6766aa91eb20909f 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 86bdae51f57dfe3abd6becd0515a2ac2005680b5..6d1d1a3a70cec1a9675a2c229b0f72e0ecacce18 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}