diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 16f666bda544747bdcd6d1f4707f94c0cbe76628..d5aa762f7d47059a997a6399ffc2c8a8019fcbd3 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/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. diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf index f91653e290e6453089815156a3ec66c9e1b70970..e2e1ebf632691c9c38fc988f3d57b7466dd61f78 100644 Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-manual.pdf differ diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex index 961d285c2d561139340e0e4fa0491e13653125b5..534bfc4cddfde0e1ae2b3e0dd7331d9472494cc1 100644 --- a/src/plugins/e-acsl/doc/userman/limitations.tex +++ b/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}