diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 104a9cf5aa797877bf9a3e63a5149f616eb559d8..416bd00dea1048bcfac220ff16a5c4af8ef4e04c 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -96,7 +96,7 @@ PLUGIN_GENERATED:= $(PLUGIN_DIR)/local_config.ml
 
 EACSL_VERSION=$(shell $(SED) -e 's/\\(.*\\)/\\1/' VERSION)
 
-$(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in
+$(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION
 	$(PRINT_MAKING) $@
 	$(RM) $@
 	$(ECHO) "(* This file was automatically generated from $<. Don't edit it. *)" >> $@
@@ -146,12 +146,14 @@ uninstall::
 
 EXPORT	=e-acsl-$(EACSL_VERSION)
 
+DOC_FILES= doc/manuals/e-acsl-manual.pdf  \
+	doc/manuals/e-acsl.pdf doc/manuals/e-acsl-implementation.pdf
+
 DISTRIB_FILES= $(filter-out $(wildcard *local_config.ml), $(wildcard *.ml)) \
 	$(wildcard *.mli) \
 	configure.ac Makefile.in \
 	doc/Changelog \
-	doc/manuals/e-acsl-manual.pdf  \
-	doc/manuals/e-acsl.pdf doc/manuals/e-acsl-implementation.pdf \
+	$(DOC_FILES) \
 	share/e-acsl/*.[ch] share/e-acsl/memory_model/*.[ch] \
 	tests/test_config.in \
 	tests/e-acsl-reject/test_config tests/e-acsl-reject/*.i \
@@ -186,6 +188,13 @@ WWW	= /localhome/julien/frama-c/doc/www
 e-acsl-install-distrib: e-acsl-distrib
 	$(PRINT) Copying to website
 	$(CP) $(EXPORT).tar.gz $(WWW)/distrib/download/e-acsl
+	$(CP) $(DOC_FILES) $(WWW)/distrib/download/e-acsl
+	$(CP) doc/manuals/e-acsl-manual.pdf \
+	      $(WWW)/distrib/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
+	$(CP) doc/manuals/e-acsl.pdf \
+	      $(WWW)/distrib/download/e-acsl/e-acsl-1.7.pdf
+	$(CP) doc/manuals/e-acsl-implementation.pdf \
+	      $(WWW)/distrib/download/e-acsl/e-acsl-implementation-$(EACSL_VERSION).pdf
 
 ##########
 # Header #
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 209580245f320fc09d5668727cbb70247f63852c..3b04cfb60da13a716867848ebeb2191a164887d9 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-0.1+dev
+0.2
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 9d46b003f577c23d42a87e4944125cf8b62d28dc..0c0a1ce71bec6e0aab44aa926f95b214c1051c69 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -20,12 +20,12 @@
 -* E-ACSL       [2013/01/09] Fix bug when translating a postcondition of a
 	        function where the init state is the same than the final
 	        state (bts #!1300).
--  E-ACSL       [2013/01/09] Support of specified function without code.
+-  E-ACSL       [2013/01/09] Support of undefined function with a contract.
 -  E-ACSL       [2012/12/20] Support of ghost variables and statements.
 -* E-ACSL       [2012/12/13] Fix bug with complex term left-values.
 -  E-ACSL       [2012/11/27] Support of \valid_read.
 -  E-ACSL       [2012/11/27] Prevent runtime errors in annotations, except
-	        unitialized variables.
+	        uninitialized variables.
 -  E-ACSL       [2012/11/19] Support of floats in annotations. Approximate
 	        reals by floats.
 -  E-ACSL       [2012/10/25] Support of \valid.
diff --git a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf
index b6002a0014dd41ad909416fd00bce9453bdda6e7..a4a9967aee14c59ba7ad1a4e27a94e8fbe2180a9 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl-implementation.pdf differ
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 59a41d0f3486fefe9b0201c14241e5b46c9452fc..4d38f3557331e4efe8e83dafe8dd304b6339db18 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/manuals/e-acsl.pdf b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf
index b7ed786018125b9cd5296675eac11e155f37c75e..b854d3b4d29c97ce40db9c8136f70550e497965f 100644
Binary files a/src/plugins/e-acsl/doc/manuals/e-acsl.pdf and b/src/plugins/e-acsl/doc/manuals/e-acsl.pdf differ
diff --git a/src/plugins/e-acsl/doc/refman/Makefile b/src/plugins/e-acsl/doc/refman/Makefile
index 15a0d50d2b998cd5b013d2e06f1badb027db8efa..f948b4964651546c2bf67ecff8f03286652383ac 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -18,8 +18,8 @@ e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
 
 all: e-acsl
 
-LANGUAGE_VERSION=1.6+dev
-EACSL_VERSION= 0.1+dev
+LANGUAGE_VERSION=1.7
+EACSL_VERSION= 0.2
 
 EACSL_DIR=$(HOME)/plugins/e-acsl
 DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
diff --git a/src/plugins/e-acsl/doc/refman/binders.tex b/src/plugins/e-acsl/doc/refman/binders.tex
index 8b62fd8f3903d9968695a825e5b51f68c2510a0d..677b920c4d8143a082c898684792c333608ae2a9 100644
--- a/src/plugins/e-acsl/doc/refman/binders.tex
+++ b/src/plugins/e-acsl/doc/refman/binders.tex
@@ -7,7 +7,7 @@
   type-expr ::= logic-type-expr | C-type-expr
   \
   logic-type-expr ::= built-in-logic-type ;
-  | id ; type id
+  | id ; type identifier
   \
   built-in-logic-type ::= "boolean" | "integer" | { "real" }
   \
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 16bc5a14a32ee9ed31120c08e70190b887694a8a..e43f30f93ccbbb2c7faba0712e4b5c8244bccd75 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -3,7 +3,7 @@
 \subsection{Version \version}
 
 \begin{itemize}
-\item Update according to \acsl 1.6.
+\item Update according to \acsl 1.7.
 \item \changeinsection{separation}{no more absent}
 \end{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 b6002a0014dd41ad909416fd00bce9453bdda6e7..a4a9967aee14c59ba7ad1a4e27a94e8fbe2180a9 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 6e477abc5f1a5e33305da7c9ad9fccaa1719f6fb..b854d3b4d29c97ce40db9c8136f70550e497965f 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/eacslversion.tex b/src/plugins/e-acsl/doc/refman/eacslversion.tex
index 6ad21205e535e4c491538d22375635051875df3d..3cbdcf18373fdbeb7ea83719442837bf0ecd4891 100644
--- a/src/plugins/e-acsl/doc/refman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/refman/eacslversion.tex
@@ -1 +1 @@
-\newcommand{\eacslversion}{0.1+dev}
+\newcommand{\eacslversion}{0.2}
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 7a06076bd560dedaca17476adcf1c47af53b70e0..9a0c56d7eabea0da2b7f83d72e62b8107e60c082 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.6\xspace}
-\newcommand{\version}{\acslversion+dev\xspace}
+\newcommand{\acslversion}{1.7\xspace}
+\newcommand{\version}{\acslversion\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 6b017dd9c89a53e3a7b68d4fff10b1f98fb6e6b3..05423f750d1fca7983dc02bb123c7380bb1474b5 100644
--- a/src/plugins/e-acsl/doc/refman/model.tex
+++ b/src/plugins/e-acsl/doc/refman/model.tex
@@ -1,6 +1,5 @@
 \begin{syntax}
   declaration ::= C-declaration ;
   | {"/*@" "model" parameter ";" "*/"} ; model variable
-  | "/*@" "model" C-type "{" parameter ";"? "}" ";" "*/" ; model field
-  | { "/*@" "model" C-declaration "*/" } ; model variable
+  | { "/*@" "model" C-type "{" parameter ";"? "}" ";" "*/" } ; model field
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/predicate.tex b/src/plugins/e-acsl/doc/refman/predicate.tex
index ecddda6bc58b811f2eb86ca9d941d1da3c7d4498..a72f293e044dec7a75066461523e44dc2fc9f07b 100644
--- a/src/plugins/e-acsl/doc/refman/predicate.tex
+++ b/src/plugins/e-acsl/doc/refman/predicate.tex
@@ -26,6 +26,7 @@
        | [ { "\forall" binders ";" pred } ]; univ. quantification
        | [ { "\exists" binders ";" pred } ]; exist. quantification
        | id ":" pred ; syntactic naming
+       | string ":" pred ; syntactic naming
        \
   [ integer-guards ] ::= [ interv  ("&&" interv)* ]
        \
diff --git a/src/plugins/e-acsl/doc/refman/speclang_modern.tex b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
index 78dd60f322a6792828df0e5915a3500d9d6062f5..a320a825768d322faf88341b206a4e18d0146aaf 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -45,6 +45,12 @@ only difference between \eacsl and \acsl predicates are quantifications.
 \label{fig:gram:binders}
 \end{figure}
 
+\begin{notimplementedenv}
+  Reals are not correctly supported by the \eacsl plug-in right now. Only
+  floating point numbers are supported: real constants and operations are seen as
+  \C floating point constants and operations.
+\end{notimplementedenv}
+
 \subsection*{Quantification}
 \eacsl quantification must be computable. They are limited to two limited forms.
 
diff --git a/src/plugins/e-acsl/doc/refman/term.tex b/src/plugins/e-acsl/doc/refman/term.tex
index f81f170bc692e02fcea39065af30dfef2a1ae761..7982a735c032ddd28c7753f514fa1e4868659cc1 100644
--- a/src/plugins/e-acsl/doc/refman/term.tex
+++ b/src/plugins/e-acsl/doc/refman/term.tex
@@ -1,9 +1,14 @@
 \begin{syntax}
-  bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ];
+  literal ::= { "\true" } | { "\false" } ; boolean constants
+       | integer ; integer constants
+       | real ; real constants
+       | string ; string constants
+       | character ; character constants
+       \ 
+  bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] | { "<<" } | { ">>" };
        | "==" | "!=" | "<=" | ">=" | ">" | "<" ;
-       | [ "&&" ] | [ "||" ] |   ; boolean operations
-       | { "&" } | { "|" } | { "-->" }
-       | { "<-->" } | "^" ; bitwise operations
+       | [ "&&" ] | [ "||" ] | [ "^^" ] ; boolean operations
+       | { "&" } | { "|" } | { "-->" } | { "<-->" } | "^" ; bitwise operations
        \
   unary-op ::= "+" | "-" ; unary plus and minus
        | "!" ; boolean negation
@@ -11,9 +16,7 @@
        | [ "*" ]; pointer dereferencing
        | "&" ; address-of operator
        \
-  term ::= { "\true" } | { "\false" };
-       | integer ; integer constants
-       | { real } ; real constants
+  term ::= literal ; literal constants
        | id ; variables
        | unary-op term ;
        | term bin-op term ;
@@ -30,4 +33,5 @@
        | "sizeof" "(" term ")" ;
        | "sizeof" "(" C-type-expr ")" ;
        | id ":" term ; syntactic naming
+       | string ":" term ; syntactic naming
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/userman/Makefile b/src/plugins/e-acsl/doc/userman/Makefile
index 5f320df835c686e184304ea1496788e56adc475a..01c27391dc7bc07c25b2c62a2d04c8aaf431978e 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -13,7 +13,7 @@ default: main.pdf
 
 main.pdf: $(DEPS_MODERN)
 
-EACSL_VERSION= 0.1+dev
+EACSL_VERSION= 0.2
 FC_VERSION= Fluorine-20130501
 
 EACSL_DIR=$(HOME)/plugins/e-acsl
@@ -21,7 +21,7 @@ DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
 install: 
 	cp -f main.pdf $(EACSL_DIR)/doc/manuals/e-acsl-manual.pdf
 	cp -f main.pdf \
-	  $(DISTRIB_DIR)/download/e-acsl/e-acsl-$(EACSL_VERSION).pdf
+	  $(DISTRIB_DIR)/download/e-acsl/e-acsl-manual-$(EACSL_VERSION).pdf
 
 include $(EACSL_DIR)/doc/support/MakeLaTeXModern
 
diff --git a/src/plugins/e-acsl/doc/userman/eacslversion.tex b/src/plugins/e-acsl/doc/userman/eacslversion.tex
index c5b0dd941b6d7806f51e4aeba1d928fcf593e0c3..a881bbe9533f436a23cd002ed5f8ccc0db31ae73 100644
--- a/src/plugins/e-acsl/doc/userman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/userman/eacslversion.tex
@@ -1,2 +1,2 @@
-\newcommand{\eacslversion}{0.1+dev\xspace}
+\newcommand{\eacslversion}{0.2\xspace}
 \newcommand{\fcversion}{Fluorine-20130501\xspace}
diff --git a/src/plugins/e-acsl/doc/userman/main.pdf b/src/plugins/e-acsl/doc/userman/main.pdf
index c028842663b7e8f58089b5ea536337877cd0f910..4d38f3557331e4efe8e83dafe8dd304b6339db18 100644
Binary files a/src/plugins/e-acsl/doc/userman/main.pdf and b/src/plugins/e-acsl/doc/userman/main.pdf differ