diff --git a/src/plugins/e-acsl/INSTALL b/src/plugins/e-acsl/INSTALL
index e608425d39ad4b2ba96fad4b8ed239e1685ad152..01c6cd8d0fa4f93703982df2eb74c8aba051c8f6 100644
--- a/src/plugins/e-acsl/INSTALL
+++ b/src/plugins/e-acsl/INSTALL
@@ -41,14 +41,14 @@ See below for more detailed and specific instructions.
 
 - GNU make version >= 3.81
 - Objective Caml >= 3.12.1;
-- Frama-C = Fluorine-20130601
+- Frama-C = Sodium-20150201
   (no warranty that this plug-in works with a more recent version of Frama-C)
 
 - The native version of the plug-in is only available if native dynamic linking
   feature of OCaml is available on your system (see Frama-C User Manual, 
   Section 3.1). 
 - Optionally, the GMP library >= 4.3
-  It is required to run the tests and to run the generated programs, 
+  It is required to run the tests and to run some generated programs, 
   but not to run the plug-in through Frama-C.
 
 ===============================================================================
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index d91e513b4f06f40f467ce81ef573ffbea45ea6fa..137e7566d6a7509d8cb6f50c5282b3a651b0e7bd 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -160,7 +160,9 @@ EACSL_DISTRIB_FILES=\
 	configure.ac Makefile.in \
 	doc/Changelog \
 	$(DOC_FILES) \
-	share/e-acsl/*.[ch] share/e-acsl/memory_model/*.[ch] \
+	share/e-acsl/*.[ch] \
+	share/e-acsl/memory_model/e_acsl_bittree.[ch] \
+	share/e-acsl/memory_model/e_acsl_mmodel*.[ch] \
 	tests/test_config.in \
 	tests/e-acsl-reject/test_config tests/e-acsl-reject/*.i \
 	tests/e-acsl-runtime/test_config tests/e-acsl-runtime/*.[ci] \
@@ -176,7 +178,8 @@ e-acsl-distrib: .depend
 	$(PRINT_UNTAR) tmp-distrib
 	cd $(EXPORT); \
 	  $(TAR) xf ../tmp.tar; autoconf; \
-	  $(SED) -i -e 's/IS_DISTRIBUTED:=no/IS_DISTRIBUTED:=yes/' Makefile.in; \
+	  $(SED) -i \
+	    -e 's/IS_DISTRIBUTED:=no/IS_DISTRIBUTED:=yes/' Makefile.in; \
 	  $(RM) -rf autom4te.cache
 	$(PRINT_RM) tmp-distrib
 	$(RM) tmp.tar
diff --git a/src/plugins/e-acsl/README b/src/plugins/e-acsl/README
index f74b18167cc5e1f53156f503af5ff797a3ca452a..7af25b11de2dd145bb52ffaa886349e31b531c7b 100644
--- a/src/plugins/e-acsl/README
+++ b/src/plugins/e-acsl/README
@@ -43,12 +43,12 @@ The user manual is available at:
 
 The standard use is the following:
 
-$ frama-c -e-acsl <files> -then-on e-acsl -print -ocode generated_code.c
+$ frama-c -e-acsl <files> -then-last -print -ocode generated_code.c
 
 Option -e-acsl runs the Frama-C's E-ACSL plug-in on the given <files>: it
-computes a new Frama-C project called `e-acsl'. Option -then-on switches to 
-this project while options -print and -ocode pretty prints the corresponding C 
-code into file `generated_code'.
+generates a new Frama-C project. Option -then-last switches to this project
+while options -print and -ocode pretty prints the corresponding C code into file
+`generated_code'.
 
 Here the only E-ACSL specific option is -e-acsl. The others (-then-on, -print
 and -ocode) are standard Frama-C options, described in the Frama-C User Manual
@@ -79,7 +79,7 @@ int main(void) {
 
 Since the assertion is always true, the generated code behaves in the same way 
 that just returning 0:
-$ frama-c -e-acsl true.i -then-on e-acsl -print -ocode gen_true.i
+$ frama-c -e-acsl true.i -then-last -print -ocode gen_true.i
 $ gcc `frama-c -print-share-path`/e-acsl/e_acsl.c gen_true.i -o gen_true
 $ ./gen_true
 $ echo $?
@@ -94,7 +94,7 @@ int main(void) {
 }
 
 Since the assertion is always false, the generated code fails at runtime:
-$ frama-c -e-acsl false.i -then-on e-acsl -print -ocode gen_false.i
+$ frama-c -e-acsl false.i -then-last -print -ocode gen_false.i
 $ gcc `frama-c -print-share-path`/e-acsl/e_acsl.c gen_false.i -o gen_false
 $ ./gen_false
 Assertion failed at line 3.
diff --git a/src/plugins/e-acsl/VERSION b/src/plugins/e-acsl/VERSION
index 0fac06906078bff672ef05555f9cafaa0820c22a..2eb3c4fe4eebcdea3da0790cc0ba74cb286ec4f4 100644
--- a/src/plugins/e-acsl/VERSION
+++ b/src/plugins/e-acsl/VERSION
@@ -1 +1 @@
-0.4.1+dev
+0.5
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index efcec9a7cb634beaeb716bde95886cba2410f68d..346766a77c44b042df62a11eeeaa8cc666596a98 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -51,17 +51,21 @@ AC_MSG_RESULT($FRAMAC_VERSION)
 
 DEV_VERSION_NUMBER=`echo $FRAMAC_VERSION | sed -e 's/.*-\(.*\)/\1/' `
 VERSION_NUMBER=`echo $DEV_VERSION_NUMBER | sed -e 's/\(.*\)+dev/\1/' `
-REQUIRED_NUMBER=20140301
+REQUIRED_NUMBER=20150201
+REQUIRED_NAME=Sodium
 
 case $FRAMAC_VERSION in
-  Neon-$REQUIRED_NUMBER+dev*)
-    # at the time being, must use the Frama-C development version
-    ;;
+  # $REQUIRED_NAME-$REQUIRED_NUMBER+dev*)
+  #   # at the time being, must use the Frama-C development version
+  #   ;;
+  $REQUIRED_NAME-$REQUIRED_NUMBER*)
+      ;;
   *)
     if test $VERSION_NUMBER -lt $REQUIRED_NUMBER; then
-      AC_MSG_ERROR(Frama-C version must be at least Neon-$REQUIRED_NUMBER.)
+      AC_MSG_ERROR(Frama-C version must be at least \
+$REQUIRED_NAME-$REQUIRED_NUMBER.)
     else
-      AC_MSG_WARN(Frama-C version is more recent than Neon: \
+      AC_MSG_WARN(Frama-C version is more recent than $REQUIRED_NAME: \
 use it at your own risk)
     fi;;
 esac
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 86ac96a1e814dc3f02c0f061ae59820a0bd83450..30272295f402784cfca682a2b0c3b1fd186c7df2 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,10 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+########################
+Plugin E-ACSL 0.5 Sodium
+########################
+
 -  E-ACSL       [2015/06/01] Support of \freeable. Thus illegal calls to
 	        free (e.g. double free) are detected.
 -* E-ACSL       [2015/05/28] Fix types of \block_length and \offset.
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 0b7390d6e4c436f83432facf335352818224222e..fe1ac7d29861b3f1992219b2ad2efedc2e944667 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 60374aa4a458eef18d85348491b499810d4fd453..008cf267af995537f7ece3fc7f26bfdcea23d019 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 a82672b65e1250faa2d12b1ce359bef5d35159aa..b4a9bfb6dbed2161525df474b1055de4a06c9c42 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 437e3b6491becdc70d4648882b772f822dcda591..c6f936ac8ce3bbb75e66cc6619397b0def464058 100644
--- a/src/plugins/e-acsl/doc/refman/Makefile
+++ b/src/plugins/e-acsl/doc/refman/Makefile
@@ -20,7 +20,7 @@ e-acsl: e-acsl-implementation.pdf e-acsl.pdf main.pdf
 
 all: e-acsl
 
-LANGUAGE_VERSION=1.8
+LANGUAGE_VERSION=1.9
 EACSL_VERSION=$(shell cat $(VERSION_FILE))
 
 EACSL_DIR=../..
diff --git a/src/plugins/e-acsl/doc/refman/assertions.tex b/src/plugins/e-acsl/doc/refman/assertions.tex
index bc5d0d0334b30304235f5b0800ddc29a08358e43..0671104df075c2dd60049795472441e5e0776620 100644
--- a/src/plugins/e-acsl/doc/refman/assertions.tex
+++ b/src/plugins/e-acsl/doc/refman/assertions.tex
@@ -1,7 +1,7 @@
 \begin{syntax}
-  compound-statement ::= "{" declaration* statement* assertion+ "}"
+  C-compound-statement ::= "{" declaration* statement* assertion+ "}"
         \
-  statement ::= assertion statement \
+  C-statement ::= assertion statement \
   assertion ::= "/*@" "assert" pred ";" "*/" ;
   | { "/*@" "for" id ("," id)* ":" "assert" pred ";" "*/" } ;
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/binders.tex b/src/plugins/e-acsl/doc/refman/binders.tex
index 677b920c4d8143a082c898684792c333608ae2a9..53a46c97cc32b0eda572c5d911617e9fb082d93b 100644
--- a/src/plugins/e-acsl/doc/refman/binders.tex
+++ b/src/plugins/e-acsl/doc/refman/binders.tex
@@ -4,7 +4,7 @@
   binder ::= type-expr variable-ident;
              (,variable-ident)*
   \
-  type-expr ::= logic-type-expr | C-type-expr
+  type-expr ::= logic-type-expr | C-type-name
   \
   logic-type-expr ::= built-in-logic-type ;
   | id ; type identifier
diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex
index 416480e6e48783746bbdd1fe81599cd103311d92..015978d8b81bdd6ae641c50736d3b74b7c8ce369 100644
--- a/src/plugins/e-acsl/doc/refman/changes_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex
@@ -4,6 +4,7 @@
 
 \begin{itemize}
 \item \changeinsection{alloc-dealloc}{include this section}
+\item Update according to \acsl 1.9.
 \end{itemize}
 
 \subsection{Version 1.8}
diff --git a/src/plugins/e-acsl/doc/refman/data_invariants.tex b/src/plugins/e-acsl/doc/refman/data_invariants.tex
index fba204a690117900c7e57da09945e751c0a52c84..6f9186f8c441db2ab04add58868491d60660b32b 100644
--- a/src/plugins/e-acsl/doc/refman/data_invariants.tex
+++ b/src/plugins/e-acsl/doc/refman/data_invariants.tex
@@ -7,7 +7,7 @@
                       { id ":" pred ";" } 
   \
   { type-invariant } ::= { { inv-strength? } "type" "invariant" };
-                      { id "(" C-type-expr id ")" "=" pred ";" }
+                      { id "(" C-type-name id ")" "=" pred ";" }
   \
   { inv-strength } ::= { "weak" } | { "strong" }
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/eacslversion.tex b/src/plugins/e-acsl/doc/refman/eacslversion.tex
index ecdb5293dfa4d061fb3db7989dae0215b186daa8..8aae7b9eff6f2de6fe20ee0bd3a55415809a6389 100644
--- a/src/plugins/e-acsl/doc/refman/eacslversion.tex
+++ b/src/plugins/e-acsl/doc/refman/eacslversion.tex
@@ -1 +1 @@
-\newcommand{\eacslversion}{0.4.1}
+\newcommand{\eacslversion}{0.5}
diff --git a/src/plugins/e-acsl/doc/refman/fn_behavior.tex b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
index 7412b9ff146bf63b972ebd1041f43568e1398c21..4cd97341aa542521fb64da755d74617ab20726a5 100644
--- a/src/plugins/e-acsl/doc/refman/fn_behavior.tex
+++ b/src/plugins/e-acsl/doc/refman/fn_behavior.tex
@@ -3,9 +3,9 @@
                             { decreases-clause? } simple-clause*;
                             named-behavior* { completeness-clause* }
   \
-  requires-clause ::= "requires" predicate ";"
+  requires-clause ::= "requires" pred ";"
   \
-  { decreases-clause } ::= { "decreases" term ("for" ident)? ";" }
+  { decreases-clause } ::= { "decreases" term ("for" id)? ";" }
   \
   [ simple-clause ] ::= { assigns-clause } | ensures-clause
   \
@@ -15,13 +15,13 @@
   \
   { location } ::= { tset }
   \
-  ensures-clause ::= "ensures" predicate ";"
+  ensures-clause ::= "ensures" pred ";"
   \
   named-behavior ::= "behavior" id ":" behavior-body
   \
   behavior-body ::= assumes-clause* requires-clause* simple-clause*
   \
-  assumes-clause ::= "assumes" predicate ";"
+  assumes-clause ::= "assumes" pred ";"
   \
   { completeness-clause } ::= { "complete" "behaviors" (id (","id)*)? ";" } ;
      | { "disjoint" "behaviors" (id (","id)*)? ";" }
diff --git a/src/plugins/e-acsl/doc/refman/ghost.tex b/src/plugins/e-acsl/doc/refman/ghost.tex
index b3c24434126f2bcb1b3faa712e5de9ed57e21200..1d6d0e9c9e6bd8ff337f7f0f3e4ba13c4085eda5 100644
--- a/src/plugins/e-acsl/doc/refman/ghost.tex
+++ b/src/plugins/e-acsl/doc/refman/ghost.tex
@@ -1,21 +1,21 @@
 \begin{syntax}
 
   ghost-type-specifier ::= C-type-specifier ;
-  | { logic-type-name } \
+  | { logic-type } \
   declaration ::= C-declaration ;
   | "/*@" "ghost" ghost-declaration "*/" \
   direct-declarator ::= C-direct-declarator ;
     | direct-declarator ;
-    "(" parameter-type-list? ")";
+    "(" C-parameter-type-list? ")";
         {"/*@" "ghost"};
-          {"("parameter-list")"};
+          {"("ghost-parameter-list")"};
           {"*/"}; ghost args
         \
   postfix-expression ::= C-postfix-expression ;
     | postfix-expression ;
-     "(" argument-expression-list? ")";
+     "(" C-argument-expression-list? ")";
      {"/*@" "ghost"} ;
-     {  "(" argument-expression-list ")"};
+     {  "(" ghost-argument-expression-list ")"};
      {  "*/"} ; call with ghosts
     \
   statement ::= C-statement ;
@@ -23,14 +23,14 @@
   statements-ghost ::= "/*@" "ghost" ;
                        ghost-statement+ "*/" \
   ghost-selection-statement ::= C-selection-statement ;
-    | "if" "(" expression ")";
+    | "if" "(" C-expression ")";
        statement;
       {"/*@" "ghost" "else"};
-      {  C-statement+ };
+      {  ghost-statement+ };
       {  "*/"} \
 
   struct-declaration ::= C-struct-declaration ;
   | {"/*@" "ghost" };
-    {C-struct-declaration "*/"} ; ghost field
+    {struct-declaration "*/"} ; ghost field
 
 \end{syntax}
diff --git a/src/plugins/e-acsl/doc/refman/logic.tex b/src/plugins/e-acsl/doc/refman/logic.tex
index 283d438702d4e1cf0ca96627fa14e09c27728fbf..6dd160eada7218be33c171109ae76dea571e45ea 100644
--- a/src/plugins/e-acsl/doc/refman/logic.tex
+++ b/src/plugins/e-acsl/doc/refman/logic.tex
@@ -3,7 +3,7 @@
   \
   [ { logic-def } ] ::= { logic-const-def } ;
           | { logic-function-def } ;
-          | { predicate-def } ;
+          | { logic-predicate-def } ;
   \
   [ { type-expr } ] ::= { id };
   \
@@ -11,7 +11,7 @@
   \
   [ { logic-function-def } ] ::= { "logic" type-expr id parameters "=" term ";" }
   \
-  [ { predicate-def } ] ::= { "predicate" id parameters? "=" pred ";" }
+  [ { logic-predicate-def } ] ::= { "predicate" id parameters? "=" pred ";" }
   \
   { parameters } ::= { "(" parameter (, parameter)* ")" }
   \
diff --git a/src/plugins/e-acsl/doc/refman/loops.tex b/src/plugins/e-acsl/doc/refman/loops.tex
index 35435e801af541c58d678ff9b1022bf5df07bd78..3294e626298e73ab219550810f0fd87c6963ee72 100644
--- a/src/plugins/e-acsl/doc/refman/loops.tex
+++ b/src/plugins/e-acsl/doc/refman/loops.tex
@@ -1,13 +1,13 @@
 \begin{syntax}
   statement ::= "/*@" loop-annot "*/" ;
-  "while" "(" expr ")" statement ;
+  "while" "(" C-expression ")" C-statement ;
   | "/*@" loop-annot "*/" ;
     "for";
-  "(" expr ";" expr ";" expr ")";
+  "(" C-expression ";" C-expression ";" C-expression ")";
   statement ;
   | "/*@" loop-annot "*/" ;
-  "do" statement ;
-  "while" "(" expr ")" ";"
+  "do" C-statement ;
+  "while" "(" C-expression ")" ";"
   \
   loop-annot ::= loop-clause* ;
   { loop-behavior* } ;
diff --git a/src/plugins/e-acsl/doc/refman/main.tex b/src/plugins/e-acsl/doc/refman/main.tex
index 6b41fe4bddb49c73557c5dbaaaff2ff6fb77ca8d..0a3803d504811c87c38ecceb411af61a4f3ba270 100644
--- a/src/plugins/e-acsl/doc/refman/main.tex
+++ b/src/plugins/e-acsl/doc/refman/main.tex
@@ -24,7 +24,7 @@
 \usepackage{alltt}
 \makeindex
 
-\newcommand{\acslversion}{1.8\xspace}
+\newcommand{\acslversion}{1.9\xspace}
 \newcommand{\version}{\acslversion\xspace}
 
 \renewcommand{\textfraction}{0.01}
diff --git a/src/plugins/e-acsl/doc/refman/model.tex b/src/plugins/e-acsl/doc/refman/model.tex
index 05423f750d1fca7983dc02bb123c7380bb1474b5..d46d192e91e764114ccadccc7a39308c6c24f33a 100644
--- a/src/plugins/e-acsl/doc/refman/model.tex
+++ b/src/plugins/e-acsl/doc/refman/model.tex
@@ -1,5 +1,5 @@
 \begin{syntax}
   declaration ::= C-declaration ;
   | {"/*@" "model" parameter ";" "*/"} ; model variable
-  | { "/*@" "model" C-type "{" parameter ";"? "}" ";" "*/" } ; model field
+  | { "/*@" "model" C-type-name "{" parameter ";"? "}" ";" "*/" } ; 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 d86f2ae0aa473b0806f1de3844930a588b7aec08..a9d2e139285eac9ea8f1c23579f40209c8a97c2e 100644
--- a/src/plugins/e-acsl/doc/refman/speclang_modern.tex
+++ b/src/plugins/e-acsl/doc/refman/speclang_modern.tex
@@ -790,5 +790,5 @@ same than the one of \acsl.
 \nodiff
 
 \difficultswhy{\lstinline|\\initialized| and
-  \notimplemented{\lstinline|\\specified|}}{the implementation of a memory
+  \notimplemented{\lstinline|\\dangling|}}{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 7982a735c032ddd28c7753f514fa1e4868659cc1..33576d7718faf8d054233b5fab1295bf6d704c15 100644
--- a/src/plugins/e-acsl/doc/refman/term.tex
+++ b/src/plugins/e-acsl/doc/refman/term.tex
@@ -31,7 +31,7 @@
        | [ term "?" term ":" term ] ; ternary condition
        | { "\let" id "=" term ";" term } ; local binding
        | "sizeof" "(" term ")" ;
-       | "sizeof" "(" C-type-expr ")" ;
+       | "sizeof" "(" C-type-name ")" ;
        | 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 1c7943103ab157f63da6431ac06c9cc2dfe03a19..25aafc00b0e30815481e645605c075a3e4ac397a 100644
--- a/src/plugins/e-acsl/doc/userman/Makefile
+++ b/src/plugins/e-acsl/doc/userman/Makefile
@@ -16,7 +16,7 @@ default: main.pdf
 main.pdf: $(DEPS_MODERN)
 
 EACSL_VERSION= $(shell cat $(VERSION_FILE))
-FC_VERSION= Neon
+FC_VERSION= Sodium
 
 EACSL_DIR=../..
 DISTRIB_DIR=$(HOME)/frama-c/doc/www/distrib
diff --git a/src/plugins/e-acsl/doc/userman/biblio.bib b/src/plugins/e-acsl/doc/userman/biblio.bib
index 7d0c29f24a18dd3b96fc830318e200d04692fbf9..6bc3d9e3068d7c377c74f4c443ffbb5a3df626d0 100644
--- a/src/plugins/e-acsl/doc/userman/biblio.bib
+++ b/src/plugins/e-acsl/doc/userman/biblio.bib
@@ -38,26 +38,26 @@
   author = {Baudin, Patrick and Pascal Cuoq and Filli\^{a}tre, Jean-Christophe 
             and March\'{e}, Claude and Monate, Benjamin and Moy, Yannick and
             Prevosto, Virgile},
-  month = apr,
-  title = {ACSL: ANSI/ISO C Specification Language. Version 1.8 --- 
+  month = mar,
+  title = {ACSL: ANSI/ISO C Specification Language. Version 1.9 --- 
            Frama-C Neon implementation.},
-  year = {2014}
+  year = {2015}
 }
 
 @manual{eacsl,
   author = {Julien Signoles},
-  title  = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.8},
-  year   = 2014,
-  month  = apr,
+  title  = {E-ACSL: Executable ANSI/ISO C Specification Language. Version 1.9},
+  year   = 2015,
+  month  = jun,
   note   = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl.pdf}}}
 }
 
 @manual{eacsl-implem,
   author = {Julien Signoles},
-  title  = {E-ACSL Version 1.7. 
-            Implementation in Frama-C Plug-in E-ACSL version 0.4},
-  year   = 2014,
-  month  = apr,
+  title  = {E-ACSL Version 1.9. 
+            Implementation in Frama-C Plug-in E-ACSL version 0.5},
+  year   = 2015,
+  month  = jun,
   note   = {\mbox{\url{http://frama-c.com/download/e-acsl/e-acsl-implementation.pdf}}}
 }
 
@@ -124,6 +124,19 @@
   month  = oct,
 }
 
+@article{fac15,
+year={2015},
+month={jan},
+journal={Formal Aspects of Computing},
+title={{Frama-C: A Software Analysis Perspective}},
+publisher={Springer London},
+keywords={Formal verification; Static analysis; Dynamic analysis; C},
+author={Kirchner, Florent and Kosmatov, Nikolai and Prevosto, Virgile and 
+Signoles, Julien and Yakobowski, Boris},
+pages={1-37},
+note={Extended version of \cite{sefm12}},
+}
+
 @article{runtime-assertion-checking,
   author    = {Lori A. Clarke and
                David S. Rosenblum},
@@ -155,3 +168,13 @@
   year =	 2009,
   publisher =	 {{IEEE} Computer Society},
 }
+
+@inproceedings{jfla15,
+  title = {{Rester statique pour devenir plus rapide, plus pr{\'e}cis et plus mince}},
+  author = {Arvid Jakobsson and Nikolai Kosmatov and Julien Signoles},
+  booktitle = {Journées Francophones des Langages Applicatifs (JFLA'15)},
+  editor = {David Baelde and Jade Alglave},
+  year = {2015},
+  month = jan,
+  note = {In French},
+}
diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex
index 2d98c60ec54379a10804a8e4c8c465aef8780f8b..5fd7532a3866c6863d2a64359cfa4c360cd43cad 100644
--- a/src/plugins/e-acsl/doc/userman/changes.tex
+++ b/src/plugins/e-acsl/doc/userman/changes.tex
@@ -6,13 +6,18 @@ release. First we list changes of the last release.
 \section*{E-ACSL \eacslversion}
 
 \begin{itemize}
+\item \textbf{Libc}: new section.
+\item \textbf{Architecture Dependent Annotations}: add a remark about \gcc's
+  machdep.
+\item Use \texttt{-then-last} whenever possible.
+\item Update output wrt \framac Sodium changes.
 \item \textbf{Bibliography:} fix incorrect links.
 \end{itemize}
 
 \section*{E-ACSL 0.4}
 
 \begin{itemize}
-\item No change
+\item No change.
 \end{itemize}
 
 \section*{E-ACSL 0.3}
diff --git a/src/plugins/e-acsl/doc/userman/eacslversion.tex b/src/plugins/e-acsl/doc/userman/eacslversion.tex
index e8d776727c61611ca4b294e6aead5c4277bd7ddb..b962244f9d57fc8b5f4b8cba06716cfe6bb23a5d 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.4.1\xspace}
-\newcommand{\fcversion}{Neon\xspace}
+\newcommand{\eacslversion}{0.5\xspace}
+\newcommand{\fcversion}{Sodium\xspace}
diff --git a/src/plugins/e-acsl/doc/userman/examples/pointer.c b/src/plugins/e-acsl/doc/userman/examples/pointer.c
index 4bab6d41faf74ecb1daff715fb4085a5cb1045e0..43d0fb4b088b7d84e19180568fa876c1327ffda6 100644
--- a/src/plugins/e-acsl/doc/userman/examples/pointer.c
+++ b/src/plugins/e-acsl/doc/userman/examples/pointer.c
@@ -1,4 +1,4 @@
-#include "stdlib.h"
+#include <stdlib.h>
 
 extern void *malloc(size_t);
 extern void free(void*);
diff --git a/src/plugins/e-acsl/doc/userman/introduction.tex b/src/plugins/e-acsl/doc/userman/introduction.tex
index d2e536b9453307788c6edde3059feaf2d601ab83..3fd972fe589a41b976e2cd6433b8fcd5a8449193 100644
--- a/src/plugins/e-acsl/doc/userman/introduction.tex
+++ b/src/plugins/e-acsl/doc/userman/introduction.tex
@@ -1,7 +1,7 @@
 \chapter{Introduction}
 
-\framac~\cite{userman,sefm12} is a modular analysis framework for the C language
-which supports the ACSL specification language~\cite{acsl}. This manual
+\framac~\cite{userman,sefm12,fac15} is a modular analysis framework for the C
+language which supports the ACSL specification language~\cite{acsl}. This manual
 documents the \eacsl plug-in of \framac, version \eacslversion. The \eacsl
 version you are using is indicated by the command \texttt{frama-c
   -e-acsl-version}\optionidx{-}{e-acsl-version}. This plug-in automatically
diff --git a/src/plugins/e-acsl/doc/userman/macros.tex b/src/plugins/e-acsl/doc/userman/macros.tex
index d666389d9db0282fd7c754b4728cf651de9ab7d5..c5c52f75339852fb785f00a2d0f75318e5913e1d 100644
--- a/src/plugins/e-acsl/doc/userman/macros.tex
+++ b/src/plugins/e-acsl/doc/userman/macros.tex
@@ -275,3 +275,11 @@
 
 \newcommand{\optionuse}[2]{\texttt{#1#2}\optionidx{#1}{#2}}
 \newcommand{\textttuse}[1]{\texttt{#1}\codeidx{#1}}
+
+\definecolor{gris}{gray}{0.85}
+\makeatletter
+\newenvironment{important}%
+{\hspace{5pt plus \linewidth minus \marginparsep}%
+ \begin{lrbox}{\@tempboxa}%
+   \begin{minipage}{\linewidth - 2\fboxsep}}
+{\end{minipage}\end{lrbox}\colorbox{gris}{\usebox{\@tempboxa}}}
diff --git a/src/plugins/e-acsl/doc/userman/main.tex b/src/plugins/e-acsl/doc/userman/main.tex
index f896579ded4a96452459fd4347dc3f0947669db8..3de64a5d6dbea2b68aedd97bd46cad8ec39ebdc8 100644
--- a/src/plugins/e-acsl/doc/userman/main.tex
+++ b/src/plugins/e-acsl/doc/userman/main.tex
@@ -42,14 +42,15 @@ CEA LIST, Software Safety Laboratory, Saclay, F-91191 \\
 This is the user manual of the \framac plug-in
 \eacsl\footnote{\url{http://frama-c.com/eacsl}}. The contents of this document
 correspond to its version \eacslversion (\today) compatible with the version
-\fcversion of \framac~\cite{userman,sefm12}. However the development of the
-\eacsl plug-in is still ongoing: features described here may still evolve in the
-future.
+\fcversion of \framac~\cite{userman,sefm12,fac15}. However the development of
+the \eacsl plug-in is still ongoing: features described here may still evolve in
+the future.
 
 \section*{Acknowledgements}
 
-We gratefully thank all the people who contributed to this document: Florent
-Kirchner, Nikolaï Kosmatov and Guillaume Petiot.
+We gratefully thank all the people who contributed to this document: Jens
+Gerlach, Pierre-Lo\"ic Garoche, Florent Kirchner, Nikolaï Kosmatov and Guillaume
+Petiot.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
diff --git a/src/plugins/e-acsl/doc/userman/provides.tex b/src/plugins/e-acsl/doc/userman/provides.tex
index 830a76bf2b5c133c57bd56c701436499a5376ecc..47981cbfc6d7bcc3f5aa4ee7bddc33308bf70f7e 100644
--- a/src/plugins/e-acsl/doc/userman/provides.tex
+++ b/src/plugins/e-acsl/doc/userman/provides.tex
@@ -39,38 +39,40 @@ Running \eacsl on this file just consists in adding the option
 \optiondef{-}{e-acsl} to the \framac command line:
 \begin{shell}
 \$ frama-c -e-acsl first.i
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
+[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
+[kernel] Parsing first.i (no preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 \end{shell}
 
 Even if \texttt{first.i} is already preprocessed, \eacsl first asks the \framac
 kernel to preprocess and to link against \texttt{first.i} several files which
-form the \eacsl library. Their usage will be explain later, mainly in
+form the \eacsl library. Their usage will be explained later, mainly in
 Section~\ref{sec:exec-env}.
 
-Then \eacsl takes the annotated \C code as input and
-translates it into a new \framac project named \texttt{e-acsl}\footnote{The
-  notion of \emph{project} is explained in Section 8.1 of the \framac user
-  manual~\cite{userman}.}. By default, the option \optionuse{-}{e-acsl} does
-nothing more. It is however possible to have a look at the generated code in the
-\framac GUI. This is also possible through the command line thanks to the kernel
-options \optionuse{-}{then-on} and \optionuse{-}{print} which respectively
-switch to another project and pretty prints the \C code~\cite{userman}:
+Then \eacsl takes the annotated \C code as input and translates it into a new
+\framac project named \texttt{e-acsl}\footnote{The notion of \emph{project} is
+  explained in Section 8.1 of the \framac user manual~\cite{userman}.}. By
+default, the option \optionuse{-}{e-acsl} does nothing more. It is however
+possible to have a look at the generated code in the \framac GUI. This is also
+possible through the command line thanks to the kernel options
+\optionuse{-}{then-last} and \optionuse{-}{print} which respectively switch to
+the last generated project and pretty prints the \C code~\cite{userman}:
 
 \begin{shell}
-\$ frama-c -e-acsl first.i -then-on e-acsl -print
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp_types.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/e_acsl_gmp.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel_api.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_bittree.h
-[kernel] preprocessing with <...> share/frama-c/e-acsl/memory_model/e_acsl_mmodel.h
+\$ frama-c -e-acsl first.i -then-last -print
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
+[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 /* Generated by Frama-C */
@@ -82,9 +84,6 @@ struct __anonstruct___mpz_struct_1 {
 typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
 typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
 typedef unsigned int size_t;
-/*@
-model __mpz_struct { integer n };
-*/
 /*@ requires predicate != 0;
     assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
@@ -93,18 +92,24 @@ extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
                                                            char *pred_txt,
                                                            int line);
 
-int __fc_random_counter __attribute__((__unused__));
+/*@
+model __mpz_struct { integer n };
+*/
+int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__));
 unsigned long const __fc_rand_max = (unsigned long)32767;
-/*@ ghost extern int __fc_heap_status; */
+/*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__); */
 
 /*@
-axiomatic
-  dynamic_allocation {
+axiomatic dynamic_allocation {
   predicate is_allocable{L}(size_t n) 
     reads __fc_heap_status;
   
   }
  */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
 extern size_t __memory_size;
 
 /*@
@@ -152,20 +157,22 @@ precise error reports as shown in Section~\ref{sec:exec}.
 \label{sec:exec}
 
 By using the option \optionuse{-}{ocode} of \framac~\cite{userman}, we can
-redirect the generated code into a \C file as follows.
+redirect the generated code into a \C file as follow.
 
 \begin{shell}
-\$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
+\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.i
 \end{shell}
 
 Then it may be executed by a standard \C compiler like \gcc in the following
 way.
-\lstset{escapechar=£}
+\lstset{escapechar=£}
 \begin{shell}
 \$ gcc -o monitored_first `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_first.i
+In file included from <file_path>/e_acsl.c:23:0:
 <file_path>/e_acsl.h:41:3: warning: `FC_BUILTIN' attribute directive ignored [-Wattributes]
 monitored_first.i:8:1: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
-monitored_first.i:19:60: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
+monitored_first.i:16:60: warning: `__FC_BUILTIN__' attribute directive ignored [-Wattributes]
+monitored_first.i:21:1: warning: `__FRAMA_C_MODEL__' attribute directive ignored [-Wattributes]
 \end{shell}
 You may notice that the generated file \texttt{monitored\_first.i} is linked
 against the file \texttt{`frama-c -print-share-path`/e-acsl/e\_acsl.c}. This
@@ -223,8 +230,8 @@ undefined as soon as $e$ has to be evaluated in order to evaluate $t$
   undefined term is never evaluated''}~\cite{eacsl}.
 
 Accordingly, the \eacsl plug-in prevents an undefined term from being
-evaluated. Should it be because an annotation contains such a term, it will
-report a proper error at runtime instead.
+evaluated. If an annotation contains such a term, \eacsl will report a proper
+error at runtime instead of evaluating it.
 
 Consider for instance the following annotated program.
 
@@ -239,7 +246,7 @@ However we can generate an instrumented code and compile it through the
 following command lines:
 
 \begin{shell}
-\$ frama-c -e-acsl rte.i -then-on e-acsl -print -ocode monitored_rte.i
+\$ frama-c -e-acsl rte.i -then-last -print -ocode monitored_rte.i
 \$ gcc -o rte `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_rte.i
 \end{shell}
 
@@ -255,7 +262,7 @@ division_by_zero: y != 0.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection{Architecture Dependent Annotations}
+\subsection{Architecture Dependent Annotations}\label{sec:architecture}
 
 In many cases, the execution of a \C program depends on the underlying machine
 architecture it is executed on. The program must be compiled on the very same
@@ -279,7 +286,7 @@ following command lines (the option \optionuse{-}{pp-annot} must be used to
 preprocess the annotations~\cite{userman}):
 
 \begin{shell}
-\$ frama-c -pp-annot -e-acsl archi.c -then-on e-acsl -print -ocode monitored_archi.i
+\$ frama-c -pp-annot -e-acsl archi.c -then-last -print -ocode monitored_archi.i
 \$ gcc -o archi `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_archi.i
 \end{shell}
 
@@ -298,9 +305,32 @@ when running the \eacsl plug-in.
 
 \begin{shell}
 \$ frama-c -machdep x86_64 -pp-annot -e-acsl archi.c \
-          -then-on e-acsl -print -ocode monitored_archi.i
+          -then-last -print -ocode monitored_archi.i
 \end{shell}
 
+\begin{important}\index{Gcc}
+If you plan to compile the generated code with \gcc, it is even better to set
+\texttt{-machdep} to \texttt{gcc\_x86\_64} (or \texttt{gcc\_x86\_32}), even if
+it does not matter on this simple example.
+\end{important}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\subsection{Libc}\index{Libc}
+
+By default, \framac uses its own standard library (\emph{aka} libc) instead of
+the one of your system. If you do not want to use it, you have to add the option
+\texttt{-no-framac-stdlib}\optionidx{-}{framac-stdlib} to the \framac command
+line following options on the command line:
+
+It might be particularly useful in one of the following contexts:
+\begin{itemize}
+\item several libc functions are still not defined in the \framac libc; or
+\item your system libc and the \framac libc mismatch about several function
+  types (for instance, your system libc is not 100\% posix compliant); or
+\item several \framac lib functions get a contract and you are not interested in
+  verifying them (for instance, only runtime errors matter).
+\end{itemize}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -312,9 +342,9 @@ when running the \eacsl plug-in.
 corresponds to mathematical integers. Such a type does not fit in any integral
 \C type. To circumvent this issue, \eacsl uses the \gmp
 library\footnote{\url{http://gmplib.org}}. Thus, even if \eacsl does its best to
-use standard integral types instead of \gmp~\cite{sac13}, it may generate such
-integers from time to time. In such cases, the generated code must be linked
-against \gmp to be executed.
+use standard integral types instead of \gmp~\cite{sac13,jfla15}, it may generate
+such integers from time to time. In such cases, the generated code must be
+linked against \gmp to be executed.
 
 Consider for instance the following program.
 
@@ -328,11 +358,11 @@ We can generate an instrumented code as usual through the following command
 line:
 
 \begin{shell}
-\$ frama-c -e-acsl gmp.i -then-on e-acsl -print -ocode monitored_gmp.i
+\$ frama-c -e-acsl gmp.i -then-last -print -ocode monitored_gmp.i
 \end{shell}
 
 To compile it however, you need to have \gmp installed and to add the option
-\optionuse{-}{lgmp} to \gcc as follows:
+\optionuse{-}{lgmp} to \gcc as follow:
 
 \begin{shell}
 \$ gcc -o pow_gmp `frama-c -print-share-path`/e-acsl/e_acsl.c monitored_gmp.i -lgmp
@@ -370,17 +400,17 @@ Consider for instance the following program.
 \listingname{valid.c}
 \cinput{examples/valid.c}
 
-Assuming that we want to execute the generated code on an X86 64-bit machine,
-the generation of the instrumented code requires the use of the option
-\optionuse{-}{machdep} since the code uses \texttt{sizeof}. However, nothing
-is required here.
+Assuming that we want to execute the generated code on an X86 64-bit machine and
+to compile it with \gcc, the generation of the instrumented code requires the
+use of the option \optionuse{-}{machdep} since the code uses
+\texttt{sizeof}. However, nothing is required here.
 
 \begin{shell}
-\$ frama-c -machdep x86_64 -e-acsl valid.c -then-on e-acsl -print -ocode monitored_valid.i
+\$ frama-c -machdep gcc_x86_64 -e-acsl valid.c -then-last -print -ocode monitored_valid.i
 \end{shell}
 
 Since the original code uses \lstinline|\valid|, the executable binary
-must be generated from \texttt{monitored\_valid.i} as follows:
+must be generated from \texttt{monitored\_valid.i} as follow:
 
 \begin{shell}
 \$ DIR=`frama-c -print-share-path`/e-acsl
@@ -403,9 +433,9 @@ freed: \valid(x).
 \end{shell}
 
 Like for integers, the \eacsl plug-in does its best to use the dedicated memory
-library only when required~\cite{rv13}. So, if your program does not contain
-memory-related annotations, the generated one does not require to be linked
-against the dedicated memory library, like the examples of the previous
+library only when required~\cite{rv13,jfla15}. So, if your program does not
+contain memory-related annotations, the generated one does not require to be
+linked against the dedicated memory library, like the examples of the previous
 sections.
 
 However, if your program contains some annotations with pointer dereferencing
@@ -419,7 +449,7 @@ example.
 \cinput{examples/pointer.c}
 
 \begin{shell}
-\$ frama-c -machdep x86_64 -e-acsl pointer.c -then-on e-acsl -print -ocode
+\$ frama-c -machdep gcc_x86_64 -e-acsl pointer.c -then-last -print -ocode
   monitored_pointer.i
 \$ DIR=`frama-c -print-share-path`/e-acsl
 \$ MDIR=\$DIR/memory_model
@@ -459,7 +489,7 @@ instead of \texttt{e\_acsl.c}, as shown below (we reuse the initial example
 \texttt{first.i} of this manual).
 
 \begin{shell}
-\$ frama-c -e-acsl first.i -then-on e-acsl -print -ocode monitored_first.i
+\$ frama-c -e-acsl first.i -then-last -print -ocode monitored_first.i
 \$ gcc -o customized_first my_assert.c monitored_first.i
 \$ ./customized_first
 Assertion at line 3 in function main is valid.
@@ -497,7 +527,7 @@ Consider for instance the following annotated program without such a
 The instrumented code is generated as usual, even though you get an additional
 warning.
 \begin{shell}
-\$ frama-c -e-acsl no_main.i -then-on e-acsl -print -ocode monitored_no_main.i
+\$ frama-c -e-acsl no_main.i -then-last -print -ocode monitored_no_main.i
 <skip preprocessing command line>
 [e-acsl] beginning translation.
 [e-acsl] warning: cannot find entry point `main'.
@@ -603,7 +633,7 @@ Consider the following program.
 To check at runtime that this program does not perform any runtime error (which
 are potential overflows in this case), just do:
 \begin{shell}
-\$ frama-c -rte combine.i -then -e-acsl -then-on e-acsl -print \
+\$ frama-c -rte combine.i -then -e-acsl -then-last -print \
           -ocode monitored_combine.i
 \$ gcc -o combine `frama-c -print-share-path`/e-acsl monitored_combine.i
 \$ ./combine.
@@ -626,14 +656,14 @@ plug-in does not generate additional code for checking them if you run the
 following command.
 \begin{shell}
 \$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
-          -then-on e-acsl -print -ocode monitored_combine.i
+          -then-last -print -ocode monitored_combine.i
 \end{shell}
 The additional code will be generated with one of the two following commands.
 \begin{shell}
 \$ frama-c -e-acsl-prepare -rte combine.i -then -val -then -e-acsl \
-          -e-acsl-valid -then-on e-acsl -print -ocode monitored_combine.i
+          -e-acsl-valid -then-last -print -ocode monitored_combine.i
 \$ frama-c -rte combine.i -then -val -then -e-acsl \
-          -then-on e-acsl -print -ocode monitored_combine.i
+          -then-last -print -ocode monitored_combine.i
 \end{shell}
 In the first case, that is because it is explicitly required by the option
 \texttt{-e-acsl-valid} while, in the second case, that is because the option
@@ -712,7 +742,7 @@ also displays the information of all the lower levels.
 \hline
 \texttt{-e-acsl-verbose 3}& predicates- and statements-related information\\
 \hline
-\texttt{-e-acsl-verbose 4 and above}& terms- and expressions-related information
+\texttt{-e-acsl-verbose 4}& terms- and expressions-related information
 \\
 \hline
 \end{tabular}
diff --git a/src/plugins/e-acsl/literal_strings.ml b/src/plugins/e-acsl/literal_strings.ml
index ba294e4d1d03dfdfb7ca787035c5a9b0fd62da8a..cb8ab4f499998e2bb3b2056584252a610e46665e 100644
--- a/src/plugins/e-acsl/literal_strings.ml
+++ b/src/plugins/e-acsl/literal_strings.ml
@@ -32,7 +32,7 @@ let is_empty () = Datatype.String.Hashtbl.length strings = 0
 
 let add = Datatype.String.Hashtbl.add strings
 let find = Datatype.String.Hashtbl.find strings
-let fold f = Datatype.String.Hashtbl.fold f strings
+let fold f = Datatype.String.Hashtbl.fold_sorted f strings
 
 (*
 Local Variables:
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
index 50aadc2155f974c60815459dc48a0d768cc0d0b0..95439a4657d03a382f8b8dfff5999a0c41f6e6e2 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
-char *__e_acsl_literal_string_2;
 char *__e_acsl_literal_string;
+char *__e_acsl_literal_string_2;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -241,14 +241,14 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
 
 void __e_acsl_memory_init(void)
 {
-  __e_acsl_literal_string_2 = "tata";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("tata"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __e_acsl_literal_string = "toto";
   __store_block((void *)__e_acsl_literal_string,sizeof("toto"));
   __full_init((void *)__e_acsl_literal_string);
   __literal_string((void *)__e_acsl_literal_string);
+  __e_acsl_literal_string_2 = "tata";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("tata"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
index c3965f7f49c722615223bac581591594d8c74977..4405fd55d8d2b5712208daeb6c6de7bf1dcd5f1c 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
@@ -1,6 +1,6 @@
 /* Generated by Frama-C */
-char *__e_acsl_literal_string_2;
 char *__e_acsl_literal_string;
+char *__e_acsl_literal_string_2;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -386,14 +386,14 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
 
 void __e_acsl_memory_init(void)
 {
-  __e_acsl_literal_string_2 = "tata";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("tata"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __e_acsl_literal_string = "toto";
   __store_block((void *)__e_acsl_literal_string,sizeof("toto"));
   __full_init((void *)__e_acsl_literal_string);
   __literal_string((void *)__e_acsl_literal_string);
+  __e_acsl_literal_string_2 = "tata";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("tata"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
index 6a0ea2b012a1d4a08a71e107dad3576f61b140d2..686c78bb30d91e3f28b125198ec09253b77c7e7e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
+++ b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
@@ -1,7 +1,7 @@
 /* Generated by Frama-C */
-char *__e_acsl_literal_string_2;
-char *__e_acsl_literal_string;
 char *__e_acsl_literal_string_3;
+char *__e_acsl_literal_string;
+char *__e_acsl_literal_string_2;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -141,18 +141,18 @@ int f(void)
 
 void __e_acsl_memory_init(void)
 {
-  __e_acsl_literal_string_2 = "bar";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
-  __e_acsl_literal_string = "foo";
-  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
-  __full_init((void *)__e_acsl_literal_string);
-  __literal_string((void *)__e_acsl_literal_string);
   __e_acsl_literal_string_3 = "toto";
   __store_block((void *)__e_acsl_literal_string_3,sizeof("toto"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __e_acsl_literal_string = "foo";
+  __store_block((void *)__e_acsl_literal_string,sizeof("foo"));
+  __full_init((void *)__e_acsl_literal_string);
+  __literal_string((void *)__e_acsl_literal_string);
+  __e_acsl_literal_string_2 = "bar";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
   __store_block((void *)(& S),4U);
   __full_init((void *)(& S));
   S = (char *)__e_acsl_literal_string;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index a21ae762bc8ca9c231e558050f01d95572b7ccd1..5cbdd9a0e2b10458db2c4729b715aa3bd26d603d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
@@ -1,8 +1,8 @@
 /* Generated by Frama-C */
-char *__e_acsl_literal_string_4;
-char *__e_acsl_literal_string_2;
 char *__e_acsl_literal_string;
+char *__e_acsl_literal_string_4;
 char *__e_acsl_literal_string_3;
+char *__e_acsl_literal_string_2;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -113,22 +113,22 @@ int G2 = 2;
 char *U = (char *)"baz";
 void __e_acsl_memory_init(void)
 {
-  __e_acsl_literal_string_4 = "foo2";
-  __store_block((void *)__e_acsl_literal_string_4,sizeof("foo2"));
-  __full_init((void *)__e_acsl_literal_string_4);
-  __literal_string((void *)__e_acsl_literal_string_4);
-  __e_acsl_literal_string_2 = "bar";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __e_acsl_literal_string = "ss";
   __store_block((void *)__e_acsl_literal_string,sizeof("ss"));
   __full_init((void *)__e_acsl_literal_string);
   __literal_string((void *)__e_acsl_literal_string);
+  __e_acsl_literal_string_4 = "foo2";
+  __store_block((void *)__e_acsl_literal_string_4,sizeof("foo2"));
+  __full_init((void *)__e_acsl_literal_string_4);
+  __literal_string((void *)__e_acsl_literal_string_4);
   __e_acsl_literal_string_3 = "foo";
   __store_block((void *)__e_acsl_literal_string_3,sizeof("foo"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __e_acsl_literal_string_2 = "bar";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
   __store_block((void *)(& S2),4U);
   __full_init((void *)(& S2));
   S2 = (char *)__e_acsl_literal_string_4;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index c64b325f8fa69df1108fa87f4752ddc5e50dc66a..d5bb4999c2dc6591705bfcf661b341809840aa94 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
@@ -1,8 +1,8 @@
 /* Generated by Frama-C */
-char *__e_acsl_literal_string_4;
-char *__e_acsl_literal_string_2;
 char *__e_acsl_literal_string;
+char *__e_acsl_literal_string_4;
 char *__e_acsl_literal_string_3;
+char *__e_acsl_literal_string_2;
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
    int _mp_size ;
@@ -141,22 +141,22 @@ int G2 = 2;
 char *U = (char *)"baz";
 void __e_acsl_memory_init(void)
 {
-  __e_acsl_literal_string_4 = "foo2";
-  __store_block((void *)__e_acsl_literal_string_4,sizeof("foo2"));
-  __full_init((void *)__e_acsl_literal_string_4);
-  __literal_string((void *)__e_acsl_literal_string_4);
-  __e_acsl_literal_string_2 = "bar";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
-  __full_init((void *)__e_acsl_literal_string_2);
-  __literal_string((void *)__e_acsl_literal_string_2);
   __e_acsl_literal_string = "ss";
   __store_block((void *)__e_acsl_literal_string,sizeof("ss"));
   __full_init((void *)__e_acsl_literal_string);
   __literal_string((void *)__e_acsl_literal_string);
+  __e_acsl_literal_string_4 = "foo2";
+  __store_block((void *)__e_acsl_literal_string_4,sizeof("foo2"));
+  __full_init((void *)__e_acsl_literal_string_4);
+  __literal_string((void *)__e_acsl_literal_string_4);
   __e_acsl_literal_string_3 = "foo";
   __store_block((void *)__e_acsl_literal_string_3,sizeof("foo"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __e_acsl_literal_string_2 = "bar";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
+  __full_init((void *)__e_acsl_literal_string_2);
+  __literal_string((void *)__e_acsl_literal_string_2);
   __store_block((void *)(& S2),4U);
   __full_init((void *)(& S2));
   S2 = (char *)__e_acsl_literal_string_4;