From e1d5e166f1ba48f78ba0941eb3f59dcaea932500 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 9 Feb 2021 17:09:57 +0100
Subject: [PATCH] [wp/doc] -wp-dump and -wp-legacy
---
src/plugins/wp/doc/manual/wp_plugin.tex | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index c44452f15e1..933cd6aa14b 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -808,6 +808,11 @@ interface of the programmatic API.
for which the current status is already 'invalid' (default is: \texttt{no}).
\item [\tt -wp-(no)-status-maybe] includes in the goal selection those properties with
an undetermined status (default is: \texttt{yes}).
+\item [\tt -wp-(no)-legacy] use the legacy WP generator, if set to \texttt{no},
+ WP uses a recently developed generator (default is: \texttt{no}).
+\item [\tt -wp-dump] does not prove selected properties, but dumps the control
+ flow graph computed by WP, including code annotations, both DOT files and PDF
+ files into the directory specified by \texttt{-wp-out}.
\end{description}
\textbf{Remark:} options \texttt{-wp-status-xxx} are not taken into account
--
GitLab