diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 416bd00dea1048bcfac220ff16a5c4af8ef4e04c..3f0b0096fb02348a0dd5b19a473e902d3fdef5f4 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -205,7 +205,7 @@ headers::
 	headache -c license/headache_config.txt -h license/CEA_LGPL \
 		*.ml *.mli \
 		Makefile.in configure.ac \
-		share/e-acsl/*.h
+		share/e-acsl/*.[ch] share/e-acsl/*/*.[ch]
 
 ################
 # Generic part #
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 44186c8829cf549a1b1230017a01efaf9a32008a..4c64d0ff83c9dff012e99434a467602710d21650 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -5,27 +5,28 @@
 - [Bernard] avoir une fonction e_acsl_trace_behavior(char *bhv_name) {}
   à appeler dès qu'un behavior est activé
 - [Yannick] Logic functions
+- [Nikolaï] temporal memory properties
+- memory profiling
 
 #####################
 # E-ACSL CONSTRUCTS #
 #####################
 
+- assigns, loop assigns
 - predicates
 - logic functions
 - disjoint and complete behaviors (cf. Bernard's feature wish)
 - loop invariant
 - loop variant
+- grep "not_yet" *.ml
 
 ########
 # CODE #
 ########
 
 - grep TODO *.ml*
-- Gestion du mode -lib-entry et/ou pas de main
-- variable GMP potentiellement initialisée mais non utilisée en présence de \at
-  (voir test result.i, cas -e-acsl-gmp-only)
+- Gestion du mode -lib-entry
 - générer les delete des globals dans une fonction séparée, comme pour les init.
-- variadic functions are not yet duplicated
 - generate guard for \offset, \block_length and \base_addr
   (\offset(p) must ensures that p is valid)
 - don't generate code for properties with status valid_under_hyp when we know
@@ -40,12 +41,16 @@
 - analysis: fixed incorrectness in presence of recursive functions
 - RTE: potential duplication (e.g. with **p)
 - default output of e_acsl_assert in the format of standart error messages
+- some calls to __eacsl_memory_debug are missing in debug mode
 
 ##############
 # KNOWN BUGS #
 ##############
 
 - see BTS
+- see Chapter "Known Limitations" of the User Manual
+- variable GMP potentiellement initialisée mais non utilisée en présence de \at
+  (voir test result.i, cas -e-acsl-gmp-only)
 - comparaisons qui aboutissent à du C incorrect
   ==> comparaison de chaînes litérales
    (voir tests other_constants.i et comparison.i)
@@ -57,21 +62,17 @@
 - incorrect d'utiliser Pre, Post, Here, Old dans stmt contract 
   (même problème que Jessie: cf. BTS #72)
   (voir aussi result.i et ./at_stmt_contract.i)
-- interprétation des tableaux
-- \valid (or other memory-model constructs) in ensures of functions without code
-- function pointers 
-  (in case of the pointing function has a behavior like in test ptr_init.c)
+- interprétation des tableaux logiques
+[Dillon] Windows
 
 #######
 # DOC #
 #######
 
-- write user manual
-- update according to the latest version of ACSL
-
 #########
 # TESTS #
 #########
 
 - inclure exemple du E-ACSL Reference Manual
+- inclure exemple du E-ACSL User Manual
 - test arith.i: mettre les exemples du ACSL manual about div and modulo
diff --git a/src/plugins/e-acsl/demo/TODO b/src/plugins/e-acsl/demo/TODO
new file mode 100644
index 0000000000000000000000000000000000000000..eb262653db9102d2b4581636481d135daebe0783
--- /dev/null
+++ b/src/plugins/e-acsl/demo/TODO
@@ -0,0 +1 @@
+les TODO et assert false dans script.ml
diff --git a/src/plugins/e-acsl/demo/alone.sh b/src/plugins/e-acsl/demo/alone.sh
new file mode 100755
index 0000000000000000000000000000000000000000..bbe34a54cc25f8453c0a90a91570eddde3a061f3
--- /dev/null
+++ b/src/plugins/e-acsl/demo/alone.sh
@@ -0,0 +1,2 @@
+#! /bin/sh
+frama-c demo.c -e-acsl -then-on e-acsl -print -ocode res_demo.c
diff --git a/src/plugins/e-acsl/demo/clean.sh b/src/plugins/e-acsl/demo/clean.sh
new file mode 100755
index 0000000000000000000000000000000000000000..857fa369f070a7b362e317751249bba64adf67a8
--- /dev/null
+++ b/src/plugins/e-acsl/demo/clean.sh
@@ -0,0 +1,5 @@
+#!/bin/bash
+
+clean
+rm -f demo.sav demo script frama_c_journal.ml res_demo.c
+./compile.sh
diff --git a/src/plugins/e-acsl/demo/compile.sh b/src/plugins/e-acsl/demo/compile.sh
new file mode 100755
index 0000000000000000000000000000000000000000..8f56bda68fe3a3c7ebd66a83a06c833d632a6051
--- /dev/null
+++ b/src/plugins/e-acsl/demo/compile.sh
@@ -0,0 +1,2 @@
+#!/bin/sh
+ocamlopt.opt -shared -o ./Script.cmxs -w Ly -warn-error A -I /usr/local/lib/frama-c -I . script.ml
diff --git a/src/plugins/e-acsl/demo/demo.c b/src/plugins/e-acsl/demo/demo.c
new file mode 100644
index 0000000000000000000000000000000000000000..2b5cc8f7e2556ade26706573cf268cad6f2c1da8
--- /dev/null
+++ b/src/plugins/e-acsl/demo/demo.c
@@ -0,0 +1,29 @@
+/*@ assigns \nothing;
+  @ behavior even:
+  @   assumes m % 2 == 0;
+  @   ensures \result >= 1;
+  @ behavior odd:
+  @   assumes m % 2 != 0;
+  @   ensures n >= 0 ==> \result >= 1; 
+  @   ensures n < 0 ==> \result <= -1; */
+int pow(int n, unsigned int m);
+
+int sum(int x) {
+  int n = 0, i;
+  for(i = 1; i <= x; i++) n += i;
+  return n;
+}
+
+int main(void) {
+  int i, n = 0;
+  unsigned int a[100];
+  n = sum(10);
+  /*@ loop invariant 0 <= i <= n ;
+    @ loop invariant \forall integer k; 0 <= k < i ==> a[k] >= 1;
+    @ loop assigns i,a[0..n-1]; */
+  for(i = 0; i < n; i++) {
+    int tmp = pow(i, i);
+    a[i] = tmp;
+  }
+  /*@ assert \forall integer k; 0 <= k < n ==> a[k] >= 1; */
+}
diff --git a/src/plugins/e-acsl/demo/demo.sh b/src/plugins/e-acsl/demo/demo.sh
new file mode 100755
index 0000000000000000000000000000000000000000..a8529b2966a4d8b9378652524ee229f014612467
--- /dev/null
+++ b/src/plugins/e-acsl/demo/demo.sh
@@ -0,0 +1,2 @@
+#! /bin/sh
+frama-c -e-acsl-prepare -save demo.sav demo.c -wp -then -val -slevel 11 -then -e-acsl -then-on e-acsl -print -ocode res_demo.c
diff --git a/src/plugins/e-acsl/demo/load.sh b/src/plugins/e-acsl/demo/load.sh
new file mode 100755
index 0000000000000000000000000000000000000000..ba15ee821379463e93a2359dfacc755e34fb2bc0
--- /dev/null
+++ b/src/plugins/e-acsl/demo/load.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+frama-c-gui -load demo.sav
diff --git a/src/plugins/e-acsl/demo/my_e_acsl.c b/src/plugins/e-acsl/demo/my_e_acsl.c
new file mode 100644
index 0000000000000000000000000000000000000000..c3175d2b822bbd405b0f430f9a0237c864603bf2
--- /dev/null
+++ b/src/plugins/e-acsl/demo/my_e_acsl.c
@@ -0,0 +1,50 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <sys/types.h>
+#include <sys/wait.h>
+#include <unistd.h>
+
+#define LEN 10
+int LAST[LEN] = { -1, -1, -1, -1, -1, -1, -1, -1, -1, -1 };
+int IDX = 0;
+
+int mem(int x) {
+  for(int i = 0; i < LEN; i++)
+    if (LAST[i] == x) return x;
+  return -1;
+}
+
+void e_acsl_assert(int predicate, 
+		   char *kind, 
+		   char *fct, 
+		   char *pred_txt, 
+		   int line) 
+{
+  if (! predicate) {
+    if (mem(line) == -1) {
+      LAST[IDX] = line;
+      IDX++;
+      int cpid = fork ();
+      if (cpid < 0) {
+	printf("%s failed at line %d of function %s.\n	\
+The failing predicate is:\n%s.\n",
+	       kind, line, fct, pred_txt);
+      } else {
+	int status;
+	if (cpid == 0) {
+	  char *line_string = (char*) malloc(sizeof(char)*3);
+	  sprintf(line_string,"%d",line);
+	  char *args[17] = { "frama-c", "-quiet", 
+			     "-load", "demo.sav", "-save", "demo.sav",
+			     "-load-module", "./Script", "-t2p-verbose", "1",
+			     "-ppt-fct", fct,
+			     "-ppt-name", kind,
+			     "-ppt-line", line_string };
+	  status = execvp("frama-c", args);
+	  exit(status);
+	} else
+	  wait(&status);
+      }
+    }
+  }
+}
diff --git a/src/plugins/e-acsl/demo/pow.c b/src/plugins/e-acsl/demo/pow.c
new file mode 100644
index 0000000000000000000000000000000000000000..a7715ec30ec758634c4264dadcd2b9c51f96f6bb
--- /dev/null
+++ b/src/plugins/e-acsl/demo/pow.c
@@ -0,0 +1,11 @@
+#include "stdio.h"
+
+int pow(int x, unsigned int n) {
+  unsigned int res = 1;
+  while (n) {
+    if (n & 1) res *= x;
+    n >>= 1;
+    x *= x;
+  }
+  return res;
+}
diff --git a/src/plugins/e-acsl/demo/run_demo.sh b/src/plugins/e-acsl/demo/run_demo.sh
new file mode 100755
index 0000000000000000000000000000000000000000..f110b94f0012720cf56204a95da92d84b196e5df
--- /dev/null
+++ b/src/plugins/e-acsl/demo/run_demo.sh
@@ -0,0 +1,7 @@
+#! /bin/sh
+
+E_ACSL_LIB=`frama-c -print-share-path`/e-acsl
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o ./demo pow.c $E_ACSL_LIB/e_acsl.c $E_ACSL_LIB/memory_model/e_acsl_bittree.c $E_ACSL_LIB/memory_model/e_acsl_mmodel.c res_demo.c
+
+./demo
diff --git a/src/plugins/e-acsl/demo/run_script.sh b/src/plugins/e-acsl/demo/run_script.sh
new file mode 100755
index 0000000000000000000000000000000000000000..e5d1fd942481bfa0d9b13cfd075db80c03675092
--- /dev/null
+++ b/src/plugins/e-acsl/demo/run_script.sh
@@ -0,0 +1,7 @@
+#! /bin/sh
+
+E_ACSL_LIB=`frama-c -print-share-path`/e-acsl
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o ./script pow.c my_e_acsl.c $E_ACSL_LIB/memory_model/e_acsl_bittree.c $E_ACSL_LIB/memory_model/e_acsl_mmodel.c res_demo.c
+
+./script
diff --git a/src/plugins/e-acsl/demo/script.ml b/src/plugins/e-acsl/demo/script.ml
new file mode 100644
index 0000000000000000000000000000000000000000..37558dbeaaa061d6d93ba068f454fe2cdb8ed58f
--- /dev/null
+++ b/src/plugins/e-acsl/demo/script.ml
@@ -0,0 +1,116 @@
+open Cil_types
+
+(* ************************************************************************** *)
+(* Registering the plug-in *)
+(* ************************************************************************** *)
+
+include Plugin.Register(struct
+  let name = "txt2ppt" 
+  let shortname = "t2p"
+  let help = "Convert E-ACSL textual properties to Frama-C properties"
+end)
+
+(* ************************************************************************** *)
+(* Defining plug-in's options *)
+(* ************************************************************************** *)
+
+module Fct_name = 
+  EmptyString
+    (struct
+      let option_name = "-ppt-fct" 
+      let help = "Name of the function in which the property is defined"
+      let arg_name = ""
+     end)
+
+module Ppt_name = 
+  EmptyString
+    (struct
+      let option_name = "-ppt-name" 
+      let help = "Name of the property (assertion, ...)"
+      let arg_name = ""
+     end)
+
+module Ppt_line = 
+  Zero
+    (struct
+      let option_name = "-ppt-line" 
+      let help = "Line at which the property is defined"
+      let arg_name = ""
+     end)
+
+(* ************************************************************************** *)
+(* Searching the property according to plug-in's options *)
+(* ************************************************************************** *)
+
+exception Found of Property.t * int
+
+let search_assert kf =
+  try
+    Annotations.iter_all_code_annot
+      (fun stmt _ a ->
+	match a.annot_content with
+	| AAssert(_, p) ->
+	  let line = Ppt_line.get () in
+	  if (fst (p.loc)).Lexing.pos_lnum = line then 
+	    raise (Found(Property.ip_of_code_annot_single kf stmt a, line))
+	| _ -> ());
+    assert false
+  with Found(ppt, line) ->
+    ppt, line
+
+let is_predicate p line = (fst (p.ip_loc)).Lexing.pos_lnum = line
+
+let search_funspec_part iter convert kf = 
+  try
+    Annotations.iter_behaviors
+      (fun _ bhv -> iter (fun _ a -> convert bhv a) kf bhv.b_name)
+      kf;
+    assert false
+  with Found(ppt, line) ->
+    ppt, line
+
+let search_ensures kf = 
+  search_funspec_part 
+    Annotations.iter_ensures
+    (fun bhv (_, p as a) ->
+      let line = Ppt_line.get () in
+      if is_predicate p line then
+	raise (Found (Property.ip_of_ensures kf Kglobal bhv a, line)) )
+    kf
+
+let search_requires kf = 
+  search_funspec_part
+    Annotations.iter_requires
+    (fun bhv a ->
+      let line = Ppt_line.get () in
+      if is_predicate a line then
+	raise (Found (Property.ip_of_requires kf Kglobal bhv a, line)) )
+    kf
+
+let search kf = match Ppt_name.get () with
+  | "" | "Assertion" -> search_assert kf
+  | "Precondition" -> search_requires kf
+  | "Postcondition" -> search_ensures kf
+  | _ -> assert false
+
+(* ************************************************************************** *)
+(* Emitting status "invalid" for the property   *)
+(* ************************************************************************** *)
+
+let emitter = 
+  Emitter.create "E-ACSL" [ Emitter.Property_status ] ~correctness:[] ~tuning:[]
+
+let emit ppt line =
+  feedback "@[line %d:@ %a@ is@ invalid.@]" line Property.pretty ppt;
+  Property_status.emit emitter ~hyps:[] ppt Property_status.False_and_reachable
+
+(* ************************************************************************** *)
+(* Plug-in's main *)
+(* ************************************************************************** *)
+
+let main () = 
+  let kf = Globals.Functions.find_by_name (Fct_name.get ()) in
+  let ppt, line = search kf in
+  emit ppt line
+
+let () = Db.Main.extend main
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 0c0a1ce71bec6e0aab44aa926f95b214c1051c69..9c90716ad2c6ab6b7483f6f6e7b737ef81bffe52 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,12 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2013/05/30] Fixed -e-acsl-debug n, with n >= 2.
+
+###################################
+Plugin E-ACSL 0.2 Fluorine_20130401
+###################################
+
 -  E-ACSL       [2013/01/09] New option -e-acsl-valid. By default, valid
 	        annotation are not translated anymore.
 -* E-ACSL       [2013/01/09] Fix bug when translating a postcondition of a
diff --git a/src/plugins/e-acsl/gcc.sh b/src/plugins/e-acsl/gcc.sh
new file mode 100755
index 0000000000000000000000000000000000000000..7e367a3f25256ac3c3b1ab33ac505da3e96ff4c5
--- /dev/null
+++ b/src/plugins/e-acsl/gcc.sh
@@ -0,0 +1,3 @@
+#!/bin/sh
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin -o $1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c $1 -lgmp && $1.out
diff --git a/src/plugins/e-acsl/misc.ml b/src/plugins/e-acsl/misc.ml
index 0e2312bb57b451a0463df297459962938dc0f09a..a152d3128fa839606b52c38ce8fbf158b73e815b 100644
--- a/src/plugins/e-acsl/misc.ml
+++ b/src/plugins/e-acsl/misc.ml
@@ -160,10 +160,11 @@ let result_vi kf = match result_lhost kf with
 (** {2 Handling the E-ACSL's C-libraries, part II} *)
 (* ************************************************************************** *)
 
-(* TODO: convert -debug 2 into a new debugging category *)
 let mk_debug_mmodel_stmt stmt =
-  if Options.debug_atleast 2 then
-    let debug = mk_call "__debug" [] in
+  if Options.debug_atleast 1
+    && Options.is_debug_key_enabled Options.dkey_analysis 
+  then
+    let debug = mk_call "__e_acsl_memory_debug" [] in
     Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
   else 
     stmt
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl.c
index c08633e039db51fa76871d9abb0bbfcb5d1e4a82..5c7a153a4ba3426df200eec15d8fb85f04967adf 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl.c
@@ -2,7 +2,7 @@
 /*                                                                        */
 /*  This file is part of the Frama-C's E-ACSL plug-in.                    */
 /*                                                                        */
-/*  Copyright (C) 2012                                                    */
+/*  Copyright (C) 2012-2013                                               */
 /*    CEA (Commissariat à l'énergie atomique et aux énergies              */
 /*         alternatives)                                                  */
 /*                                                                        */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index 4c70652ea7c00b225c84e90e275ef1c3fcda51cd..31dd8ed5695bd8d91f8e25a4b55d9ec25e3f4911 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of the Frama-C's E-ACSL plug-in.                    */
+/*                                                                        */
+/*  Copyright (C) 2012-2013                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It is distributed in the hope that it will be useful,                 */
+/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
+/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
+
 #include <assert.h>
 #include <errno.h>
 #include <unistd.h>
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
index 81c724e589a2dc5771660138e7ce0ec91e6df8b4..3738659e58962a4dd0cfa57b07befdb70a369f72 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.h
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of the Frama-C's E-ACSL plug-in.                    */
+/*                                                                        */
+/*  Copyright (C) 2012-2013                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It is distributed in the hope that it will be useful,                 */
+/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
+/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
+
 #ifndef E_ACSL_BITTREE
 #define E_ACSL_BITTREE
 
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index e2ec24d10794909863f1eec82cb8af8f54f5a02d..50f5681edcf129e48e49318654b3f3fcc8984816 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -1,3 +1,24 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of the Frama-C's E-ACSL plug-in.                    */
+/*                                                                        */
+/*  Copyright (C) 2012-2013                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It is distributed in the hope that it will be useful,                 */
+/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
+/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
 
 #include <stdio.h>
 #include <stdlib.h>
@@ -10,13 +31,12 @@
 size_t __memory_size = 0;
 /*unsigned cpt_store_block = 0;*/
 
-
 const int nbr_bits_to_1[256] = {
   0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
 };
 
 /*@ assigns \nothing;
-  @ ensures \resul == __memory_size;
+  @ ensures \result == __memory_size;
   @*/
 size_t __get_memory_size(void) {
   return __memory_size;
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 39eb7c215a27552ba7b3b405430052f206ac719f..ff4de942d7c414d6abddf7de30205fac616fb087 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -1,3 +1,24 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of the Frama-C's E-ACSL plug-in.                    */
+/*                                                                        */
+/*  Copyright (C) 2012-2013                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It is distributed in the hope that it will be useful,                 */
+/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
+/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
 
 #ifndef E_ACSL_MMODEL
 #define E_ACSL_MMODEL
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index 517ae2feba4c98a23f396406e8fd9e545500e0b2..0dfb43597562d94fde53df8f9ee7229234a27fda 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -1,3 +1,25 @@
+/**************************************************************************/
+/*                                                                        */
+/*  This file is part of the Frama-C's E-ACSL plug-in.                    */
+/*                                                                        */
+/*  Copyright (C) 2012-2013                                               */
+/*    CEA (Commissariat à l'énergie atomique et aux énergies              */
+/*         alternatives)                                                  */
+/*                                                                        */
+/*  you can redistribute it and/or modify it under the terms of the GNU   */
+/*  Lesser General Public License as published by the Free Software       */
+/*  Foundation, version 2.1.                                              */
+/*                                                                        */
+/*  It is distributed in the hope that it will be useful,                 */
+/*  but WITHOUT ANY WARRANTY; without even the implied warranty of        */
+/*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         */
+/*  GNU Lesser General Public License for more details.                   */
+/*                                                                        */
+/*  See the GNU Lesser General Public License version 2.1                 */
+/*  for more details (enclosed in the file licenses/LGPLv2.1).            */
+/*                                                                        */
+/**************************************************************************/
+
 #ifndef E_ACSL_MMODEL_API
 #define E_ACSL_MMODEL_API
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index dfd6be32f6e0826c6591810b94c540639e89368d..dda39b4964cfaa221c8c01f948736988af24b4af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
@@ -18,8 +18,8 @@
 [value] using specification for function __full_init
 tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __delete_block
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index dfd6be32f6e0826c6591810b94c540639e89368d..dda39b4964cfaa221c8c01f948736988af24b4af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -18,8 +18,8 @@
 [value] using specification for function __full_init
 tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __delete_block
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
index 07fcdaf5d06cfade5ff4e9e9c7c1336d4be73ab9..5411fb367046acf0e7099cd055a62eac54588898 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
@@ -20,8 +20,8 @@ tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
 [value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
index 07fcdaf5d06cfade5ff4e9e9c7c1336d4be73ab9..5411fb367046acf0e7099cd055a62eac54588898 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
@@ -20,8 +20,8 @@ tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
 [value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index 4e05beb5b82748e552cdb62d63f93d9215c2ab8e..26fdbdf56a1cfd6d37c1e948e1aa681304125764 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
@@ -37,8 +37,8 @@ tests/e-acsl-runtime/bts1399.c:24:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
 FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 6b1be31fcb0f2dfe471743c9f7ff96c982d1ddd8..aa490e4d81067549b58c9be9ef298b02995081ad 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -58,8 +58,8 @@ share/e-acsl/e_acsl_gmp.h:163:[value] Function __gmpz_tdiv_q: precondition got s
 [value] using specification for function __gmpz_get_ui
 share/e-acsl/e_acsl_gmp.h:194:[value] Function __gmpz_get_ui: precondition got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 [value] using specification for function __gmpz_clear
 share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
 FRAMAC_SHARE/libc/stdlib.h:142:[value] Function __e_acsl_free, behavior deallocation: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
index 367980e27e71ab1ba3695b530bf9690db2a05a36..564a7b4632f674c4ae7173d3ba5686ae0533e0da 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
@@ -25,8 +25,8 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 [value] using specification for function __valid
 tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 [value] using specification for function __delete_block
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index 92d0252727de5d3a845d4c9577aec48e724c437e..93d783ae1482426b5035ecca198df0b466afd316 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -38,8 +38,8 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 share/e-acsl/e_acsl_gmp.h:114:[value] Function __gmpz_clear: precondition got status valid.
 tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
 [value] using specification for function __valid_read
 tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index 40f94b88cb3f9f5ea622debd3f704bf8adbc5502..5b920f33e5ac50f8c46cedf349ddbfda8cc7cc27 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -31,8 +31,8 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid.
 tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid.
 [value] using specification for function __valid
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 40a81d2213effc8fde7d820da941eb9c2cd7e620..6928f226ea0c260ac3974e8f7d7bb58197c3a23f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -29,8 +29,8 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index 40a81d2213effc8fde7d820da941eb9c2cd7e620..6928f226ea0c260ac3974e8f7d7bb58197c3a23f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -29,8 +29,8 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function __valid
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index f859ef03dcb37ee5be9a64f210e8be005ba79368..f60e8f83e3ef2664ba5a0e5cddca073ea64d8778 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -19,8 +19,8 @@
 [value] using specification for function __initialize
 tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function __valid_read
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 42d20c631881211445b7ee7612e5a98c2c4012af..65357e1cff85b1cd4747a6b868beab06892fa5eb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -37,8 +37,8 @@ tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 42d20c631881211445b7ee7612e5a98c2c4012af..65357e1cff85b1cd4747a6b868beab06892fa5eb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -37,8 +37,8 @@ tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
 tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
 [kernel] warning: Neither code nor specification for function __e_acsl_memory_clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index c31f4f17a23d6b62a5ba03fc02bb6073bfb42cc1..a611a50644342ff77774003c701ad9020f4c6a08 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -32,8 +32,8 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' i
 [value] using specification for function __full_init
 tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
 tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
@@ -49,7 +49,7 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
 tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in b.
 tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index c31f4f17a23d6b62a5ba03fc02bb6073bfb42cc1..a611a50644342ff77774003c701ad9020f4c6a08 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -32,8 +32,8 @@ tests/e-acsl-runtime/valid.c:33:[e-acsl] warning: E-ACSL construct `\allocate' i
 [value] using specification for function __full_init
 tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 tests/e-acsl-runtime/valid.c:35:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
 tests/e-acsl-runtime/valid.c:35:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid.c:35:[value] all evaluations are invalid for function call argument
@@ -49,7 +49,7 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 tests/e-acsl-runtime/valid.c:37:[kernel] warning: accessing uninitialized left-value: assert \initialized(&b);
 tests/e-acsl-runtime/valid.c:37:[kernel] warning: completely indeterminate value in b.
 tests/e-acsl-runtime/valid.c:37:[value] all evaluations are invalid for function call argument
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index ad833159dd46309b9278b4ae3679ffa78afc8266..56f011916a1cee7646cfba9a69895e8eff2ab957 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -29,8 +29,8 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
 [value] using specification for function __store_block
 tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for function call argument
@@ -47,7 +47,7 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __initialize
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function __valid
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 132daabd9ccc7b214c21f428c35470790d5d0638..6bbb1e532ed881130eb726d8db9c225f1e5a5727 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -29,8 +29,8 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
 [value] using specification for function __store_block
 tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
 tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for function call argument
@@ -47,7 +47,7 @@ FRAMAC_SHARE/libc/stdlib.h:127:[value] Function __e_acsl_malloc, behavior alloca
 FRAMAC_SHARE/libc/stdlib.h:132:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function __initialize
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function __valid
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 92e4abd42c4022e621b3c46a023c3c6532c92641..0ed09a242860052b788108dbaa1a8c32122f0b69 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -18,8 +18,8 @@
 [value] using specification for function __store_block
 [value] using specification for function __valid
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 [value] using specification for function __valid_read
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 92e4abd42c4022e621b3c46a023c3c6532c92641..0ed09a242860052b788108dbaa1a8c32122f0b69 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -18,8 +18,8 @@
 [value] using specification for function __store_block
 [value] using specification for function __valid
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status unknown.
 [value] using specification for function __valid_read
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index d5e6abb42d5f65ea8679d3bdcd9ece533d07630b..3a62b0c363a2d01227d31e2af8591aa097d87785 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -31,8 +31,8 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
 [value] using specification for function __initialize
 tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __full_init
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index ab6aa7e7c58ca7c98462b95c655e63ccc7ccca24..d1cf5ba1df8769be7a6f17cef5e15b3f928d900f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -31,8 +31,8 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
 [value] using specification for function __initialize
 tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid.
 [value] using specification for function __initialized
-share/e-acsl/memory_model/e_acsl_mmodel.h:86:[value] Function __initialized: postcondition got status unknown.
-share/e-acsl/memory_model/e_acsl_mmodel.h:87:[value] Function __initialized: postcondition got status valid.
+share/e-acsl/memory_model/e_acsl_mmodel.h:107:[value] Function __initialized: postcondition got status unknown.
+share/e-acsl/memory_model/e_acsl_mmodel.h:108:[value] Function __initialized: postcondition got status valid.
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 [value] using specification for function __full_init