From 06527efadee7f293d7ed23e40cde467b3f451fcb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 18 Sep 2018 18:07:33 +0200
Subject: [PATCH] [userman] the memory analysis is not robust
---
src/plugins/e-acsl/doc/userman/provides.tex | 6 ++++++
1 file changed, 6 insertions(+)
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 222ee31e56c..51d07701428 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -552,6 +552,12 @@ potential memory-related annotations even when it is not required. This
feature can be enabled using the \shortopt{M} switch of \eacslgcc or
\shortopt{e-acsl-full-mmodel} option of the \eacsl plug-in.
+\begin{important}
+The above-mentioned static analysis is probably the less robust part of \eacsl
+for the time being. When handling a large piece of code, it might be necessary
+to deactivate it and systematically instrument the code as explained above.
+\end{important}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% \subsection{Debug Libraries}
%% \label{sec:runtime-debug}
--
GitLab