[manual] fixed bug #1696 by clarifying the manual

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,7 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2014/08/04] Fix bug #1696 by clarifying the manual.
 -* E-ACSL       [2014/08/04] Fix bug #1831 about argc and argv.
 -* E-ACSL       [2014/07/08] Fix bug about using some part of the
 	        (Frama-C) libc which prevents linking of the generated C code.

src/plugins/e-acsl/doc/userman/limitations.tex

@@ -107,6 +107,11 @@ The failing predicate is:
 freed: \valid(x).
 \end{shell}
 
+Also, if the unprovided main initializes some variables, running the
+instrumented code (linked against this main) could print some warnings from the
+\eacsl memory library\footnote{see
+  \url{https://bts.frama-c.com/view.php?id=1696} for an example}.
+
 \subsection{Undefined Functions}
 \label{sec:limits:no-code}
 \index{Function!Undefined}