diff --git a/src/plugins/e-acsl/doc/userman/limitations.tex b/src/plugins/e-acsl/doc/userman/limitations.tex index 147fc7981a155d1cef980040a141153b15b20d48..5613e684dd505794e82c60c8f5e4a70e521d6616 100644 --- a/src/plugins/e-acsl/doc/userman/limitations.tex +++ b/src/plugins/e-acsl/doc/userman/limitations.tex @@ -125,12 +125,23 @@ function without code. There is also no workaround yet. \section{Recursive Function} \index{Function!Recursive} +Programs containing recursive functions have the same limitations than the ones +containing function without code (Section~\ref{sec:limits:no-code}) and +memory-related annotations. + +Also, even if there is no such annotations, the generated code may call a +function before it is declared. This behavior appears in a non-specified +way. The generated code is however easy to fix by hand. + \section{Variadic Function} \index{Function!Variadic} -\begin{itemize} -\item Not yet duplicated -\end{itemize} +Programs containing variadic functions without code but with a function contract +are not yet supported. There is no workaround. \section{Function Pointer} \index{Function!Pointer} + +Programs containing function pointers have the same limitations as about +memory-related annotations than the ones containing function without code or +recursive functions. diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf index 681398086ae842db2727d513dce9a2c53009a163..f9ade5db66683f6c43756462647067b07d6419e5 100644 Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and b/src/plugins/e-acsl/doc/userman/main.pdf differ