diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 04ded99c7eb15b6c63b08ca0a84ecfc4f6711bbb..edbb317dea223f6e93c2f6c604879dcaf9dbe9f6 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -73,12 +73,17 @@ in \lstinline|\\at|}
 \ifthenelse%
     {\boolean{PrintImplementationRq}}%
     {
-\section{Changes in \eacsl implementation}
+\section{Changes in \eacsl Implementation}
 
 \subsection{Version \eacslversion}
 
 \begin{itemize}
-\item Implement bitwise complementation.
+\item \changeinsection{expressions}{support of bitwise complementation}
+\item \changeinsection{memory}{support of \lstinline|\\valid|}
+\item \changeinsection{memory}{support of \lstinline|\\block_length|}
+\item \changeinsection{memory}{support of \lstinline|\\base_addr|}
+\item \changeinsection{memory}{support of \lstinline|\\offset|}
+\item \changeinsection{dangling}{support of \lstinline|\\initialized|}
 \end{itemize}
 
 \subsection{Version 0.1}
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf
index b1d1d32de62af5112dc875c7cf4b8e1530f4ce4d..0e9f3a8e463501bee37c24f5ea1ede1bf5745517 100644
Binary files a/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/refman/e-acsl-implementation.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/e-acsl.pdf b/src/plugins/e-acsl/doc/refman/e-acsl.pdf
index 83c30a2bc54f9289cf8dba18f13388ed8febe33e..52d86031d12315737e55ef3585d80e4686c812dd 100644
Binary files a/src/plugins/e-acsl/doc/refman/e-acsl.pdf and b/src/plugins/e-acsl/doc/refman/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index b418fcf6fb5c11950dcc75366e656f275307c233..0ac2730eab73d0ea62202c64969adfd095818cfb 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -650,12 +650,12 @@ axiomatics.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{Memory blocks and pointer dereferencing}
-\label{subsec:memory}
+\label{subsec:memory}\label{sec:memory}
 \nodiff
 
-\difficultswhy{\notimplemented{\lstinline|\\base\_addr|,
+\difficultswhy{\lstinline|\\base\_addr|,
     \lstinline|\\block\_length|, \lstinline|\\valid| and
-    \lstinline|\\offset|}}{the implementation of a memory model}
+    \lstinline|\\offset|}{the implementation of a memory model}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -762,7 +762,9 @@ same than the one of \acsl.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \section{Undefined values, dangling pointers}
+\label{sec:dangling}
 \nodiff
 
-\difficultswhy{\notimplemented{\lstinline|\\initialized| and
-    \lstinline|\\specified|}}{the implementation of a memory model}
+\difficultswhy{\lstinline|\\initialized| and
+  \notimplemented{\lstinline|\\specified|}}{the implementation of a memory
+  model}
diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex
index aad67173b9b88acafb3efecb3ab67f46b9abde78..f81f170bc692e02fcea39065af30dfef2a1ae761 100644
--- a/src/plugins/e-acsl/doc/refman/term.tex
+++ b/src/plugins/e-acsl/doc/refman/term.tex
@@ -3,7 +3,7 @@
        | "==" | "!=" | "<=" | ">=" | ">" | "<" ;
        | [ "&&" ] | [ "||" ] |   ; boolean operations
        | { "&" } | { "|" } | { "-->" }
-       | { "<-->" } | { "^" } ; bitwise operations
+       | { "<-->" } | "^" ; bitwise operations
        \
   unary-op ::= "+" | "-" ; unary plus and minus
        | "!" ; boolean negation