diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index b3779bcf96169d001aee02a8889c9b4e5536ae96..653d3355f8f7c7e4eb04db420473d3d46be6a970 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -31,10 +31,9 @@
 -* E-ACSL       [2012/01/24] Fix bug with boolean.
 -* E-ACSL       [2012/01/24] Fix bug with negation and GMP integers.
 -* E-ACSL       [2012/01/24] Fix bug with conditional and GMP integers.
--  E-ACSL       [2012/01/24] function e_acsl_assert now consistent with
+-  E-ACSL       [2012/01/24] Function e_acsl_assert now consistent with
 	        standard assert.
--* E-ACSL	[2012/01/23] Function __gmp_com was wrongly named in
-	        E_ACSL C header.
+-  E-ACSL	[2012/01/23] Support of bitwise complementation.
 -  E-ACSL	[2012/01/20] Use GMP arithmetics only when required
 	        (i.e. mostly never in practice).
 
@@ -42,6 +41,6 @@
 Plugin E-ACSL 0.1 Nitrogen_20111001
 ###################################
 
--  E-ACSL	[2012/01/06] First release for the Hi-Lite FUI9 project.
+-  E-ACSL	[2012/01/06] First public release.
 
 ###################################
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 445b8df769694e9290747315b8942193a6528b7e..b96e6ebf47ffe00f08d8114a388bddf9a8c9f1d7 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -18,7 +18,7 @@ e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
 
 all: e-acsl
 
-LANGUAGE_VERSION=1.5-4+dev
+LANGUAGE_VERSION=1.6+dev
 EACSL_VERSION= 0.1+dev
 
 EACSL_DIR=$(HOME)/plugins/e-acsl
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index edbb317dea223f6e93c2f6c604879dcaf9dbe9f6..16bc5a14a32ee9ed31120c08e70190b887694a8a 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -2,6 +2,11 @@
 
 \subsection{Version \version}
 
+\begin{itemize}
+\item Update according to \acsl 1.6.
+\item \changeinsection{separation}{no more absent}
+\end{itemize}
+
 \subsection{Version 1.5-4}
 
 \begin{itemize}
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 0e9f3a8e463501bee37c24f5ea1ede1bf5745517..35109ca7c4bf70f13b12506c11e440a4dd567fc1 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 52d86031d12315737e55ef3585d80e4686c812dd..ca3054d1616e70bb26f01e513453f978158d1570 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/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
index a9a3b5b40a92cf37ea8840cdda72832a57a9d4dc..7412b9ff146bf63b972ebd1041f43568e1398c21 100644
--- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -13,6 +13,8 @@
   \
   { locations } ::= { location ("," location) * | "\nothing" }
   \
+  { location } ::= { tset }
+  \
   ensures-clause ::= "ensures" predicate ";"
   \
   named-behavior ::= "behavior" id ":" behavior-body
diff --git a/src/plugins/e-acsl/doc/refman/intro_modern.tex b/src/plugins/e-acsl/doc/refman/intro_modern.tex
index bcf74f8361e7faa8fe8b366869c15deb00a2fcf4..bd83ffa548821603b9b6a47b1cc47a655e8c3826 100644
--- a/src/plugins/e-acsl/doc/refman/intro_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/intro_modern.tex
@@ -50,18 +50,15 @@ currently implemented into the \framac's \eacsl plug-in.
       & \lstinline|\\true| and \lstinline|\\false| \\
       & bitwise operators \\
       & let binding \\
-      & typeof \\
       & t-sets \\
-      & \lstinline|base\_addr|, \lstinline|offset| and
-      \lstinline|block\_length|
-      \\
       \hline
       predicates 
       & exclusive or operator \\  %     \lstinline|^^|
       & let bindings \\
       & quantifications over non-integer types \\
-      & \lstinline|valid| and \lstinline|valid\_range| \\
-      & \lstinline|initialized| and \lstinline|specified|
+      & \lstinline|\\valid\_read| \\
+      & \lstinline|\\separated| \\
+      & \lstinline|\\specified|
       \\
       \hline
       annotations 
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 5f968cf265420bd1e073549506154d0bf05c748a..4eaaf13e2e817a6789593f247481411ea2a0457e 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -25,8 +25,8 @@
 \usepackage{alltt}
 \makeindex
 
-\newcommand{\acslversion}{1.5\xspace}
-\newcommand{\version}{\acslversion-4+dev\xspace}
+\newcommand{\acslversion}{1.6\xspace}
+\newcommand{\version}{\acslversion+dev\xspace}
 
 \renewcommand{\textfraction}{0.01}
 \renewcommand{\topfraction}{0.99}
diff --git a/src/plugins/e-acsl/doc/refman/model.tex b/src/plugins/e-acsl/doc/refman/model.tex
index 6e2a728555951a84b122230fb772badab6b01621..6b017dd9c89a53e3a7b68d4fff10b1f98fb6e6b3 100644
--- a/src/plugins/e-acsl/doc/refman/model.tex
+++ b/src/plugins/e-acsl/doc/refman/model.tex
@@ -1,7 +1,6 @@
 \begin{syntax}
   declaration ::= C-declaration ;
+  | {"/*@" "model" parameter ";" "*/"} ; model variable
+  | "/*@" "model" C-type "{" parameter ";"? "}" ";" "*/" ; model field
   | { "/*@" "model" C-declaration "*/" } ; model variable
-  \
-  struct-declaration ::= C-struct-declaration ;
-  | { "/*@" "model" C-struct-declaration "*/" } ; model field
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 0ac2730eab73d0ea62202c64969adfd095818cfb..b5e7667f378427fe2a639b65e0f9deb3af895fb7 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -654,13 +654,17 @@ axiomatics.
 \nodiff
 
 \difficultswhy{\lstinline|\\base\_addr|,
-    \lstinline|\\block\_length|, \lstinline|\\valid| and
+    \lstinline|\\block\_length|, \lstinline|\\valid|, 
+    \notimplemented{\lstinline|\\valid_read|} and
     \lstinline|\\offset|}{the implementation of a memory model}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{Separation}
-\absentexperimental
+\subsection{Separation}\label{sec:separation}
+\nodiff
+
+\difficultswhy{\notimplemented{\lstinline|\\separated|}}{the implementation of a
+  memory model}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -718,6 +722,7 @@ invariants.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 \subsection{\notimplemented{Model variables and model fields}}
+\label{sec:model}
 \index{model}
 
 \nodiff