From 3e034a88bae65a8b0d6e71ed0a973d60c0239a73 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 18 Sep 2018 18:23:56 +0200
Subject: [PATCH] [userman] highlight the importance of -e-acsl-prepare as
 suggested in issue #58

---
 src/plugins/e-acsl/doc/userman/provides.tex | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 51d07701428..08d1e9aaea3 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -894,8 +894,14 @@ library in order to generate the \framac internal representation of the \C
 program (\emph{aka} AST), as explained in Section~\ref{sec:run}. Consequently,
 even if the \eacsl plug-in keeps the maximum amount of information, the results
 of already executed analyzers (such as validity status of annotations) are not
-known in this new project. If you want to keep them, you have to set the option
-\shortopt{e-acsl-prepare} when the first analysis is asked for.
+known in this new project.
+
+\begin{important}
+If you want to keep results of former analysis, you have to set the option
+\shortopt{e-acsl-prepare} when the first analysis is asked for. The standard
+example is running \eacsl after \Eva: in such a case, \shortopt{e-acsl-prepare}
+must be provided together with the \Eva's \shortopt{-val} option.
+\end{important}
 
 In this context, the \eacsl plug-in does not generate code for annotations
 proven valid by another plug-in, except if you explicitly set the option
-- 
GitLab