[wp] update the doc & changelog

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)
 ######################

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}