diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 611e2eb01bd2b3589906243bbec18c4784a561b3..a0cc7fef9f4fe68dc42641c984c7738272eefd99 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2014/08/05] Fix bug #1818 about initialization of globals.
 -* E-ACSL       [2014/08/04] Fix bug #1696 by clarifying the manual.
 -* E-ACSL       [2014/08/04] Fix bug #1831 about argc and argv.
 -* E-ACSL       [2014/07/19] Fix bug #1836 about one-off error when
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
new file mode 100644
index 0000000000000000000000000000000000000000..e7a5a17ddbb6c85997ea761ae6f789b4757d35cf
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/init.c
@@ -0,0 +1,14 @@
+/* run.config
+   COMMENT: initialization of globals (bts #1818)
+   EXECNOW: LOG gen_init.c BIN gen_init.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init.c > /dev/null && ./gcc_test.sh init
+   EXECNOW: LOG gen_init2.c BIN gen_init2.out @frama-c@ -machdep x86_64 -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/init.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_init2.c > /dev/null && ./gcc_test.sh init2
+*/
+
+int a = 0, b;
+
+int main(void) {
+  int *p = &a, *q = &b;
+  /*@assert \initialized(&b) ; */
+  /*@assert \initialized(q) ; */
+  /*@assert \initialized(p) ; */
+}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
index 44f5c5647e533e34a56c2c4b04532469f429e81c..889dfbfd3a5cde9c6c356d03622b18d284ee8ccb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
@@ -20,6 +20,7 @@
   global_i ∈ {0}
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
+[value] using specification for function __full_init
 tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
index 76d0e9b7e0a3933965f5588a5277d0e5b8be81a3..d794b166518c314ac820ce69a6e95c2abef54049 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
@@ -20,6 +20,7 @@
   global_i ∈ {0}
   global_i_ptr ∈ {{ &global_i }}
 [value] using specification for function __store_block
+[value] using specification for function __full_init
 tests/e-acsl-runtime/bts1478.c:10:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
 tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
index 515980fc04bd935fcd40953580a5dcf5786888e0..1af8751dd51f9760cb8039b01141539f42961079 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
@@ -39,6 +39,9 @@ extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
 /*@ ensures \result ≡ 0 ∨ \result ≡ 1;
     ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
     assigns \result;
@@ -93,7 +96,9 @@ void __e_acsl_loop(void)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& global_i_ptr),4U);
+  __full_init((void *)(& global_i_ptr));
   __store_block((void *)(& global_i),4U);
+  __full_init((void *)(& global_i));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
index 83ff924f0a41a71e21bf755542f5ca340025c386..b0fc6e014d1298110aa720dbd57bb8eb0410f290 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
@@ -62,6 +62,9 @@ extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
 /*@ assigns \nothing; */
 extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
 
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
 /*@ ensures \result ≡ 0 ∨ \result ≡ 1;
     ensures \result ≡ 1 ⇒ \valid((char *)\old(ptr)+(0 .. \old(size)-1));
     assigns \result;
@@ -125,7 +128,9 @@ void __e_acsl_loop(void)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& global_i_ptr),4U);
+  __full_init((void *)(& global_i_ptr));
   __store_block((void *)(& global_i),4U);
+  __full_init((void *)(& global_i));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
index a58680ab4e8972cc8848311c76fb93be9781e9ab..764d3802ca85918046da77820e1c9fb73c802af8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost.c
@@ -89,7 +89,9 @@ int *P;
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& P),4U);
+  __full_init((void *)(& P));
   __store_block((void *)(& G),4U);
+  __full_init((void *)(& G));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
index 82da68f4bfd047bcfdea7fa41fa2a56a91549172..818ce62654dcf88fdc6e93621abded71c5039d33 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ghost2.c
@@ -103,7 +103,9 @@ int *P;
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& P),4U);
+  __full_init((void *)(& P));
   __store_block((void *)(& G),4U);
+  __full_init((void *)(& G));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
new file mode 100644
index 0000000000000000000000000000000000000000..0bc419bf7d38a8f6c9d6edc9b80cb4f0d2ba2212
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
@@ -0,0 +1,117 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+   int _mp_alloc ;
+   int _mp_size ;
+   unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+    assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+                                                           char *kind,
+                                                           char *fct,
+                                                           char *pred_txt,
+                                                           int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+  dynamic_allocation {
+  predicate is_allocable{L}(size_t n) 
+    reads __fc_heap_status;
+  
+  }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+                                                            size_t size);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+    ensures
+      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+    assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+                                                          size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+    assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+  \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int a = 0;
+int b;
+void __e_acsl_memory_init(void)
+{
+  __store_block((void *)(& b),4U);
+  __full_init((void *)(& b));
+  __store_block((void *)(& a),4U);
+  __full_init((void *)(& a));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int *p;
+  int *q;
+  __e_acsl_memory_init();
+  __store_block((void *)(& q),8U);
+  __store_block((void *)(& p),8U);
+  __full_init((void *)(& p));
+  p = & a;
+  __full_init((void *)(& q));
+  q = & b;
+  /*@ assert \initialized(&b); */
+  e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+                (char *)"\\initialized(&b)",11);
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized;
+    __e_acsl_initialized = __initialized((void *)q,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(q)",12);
+  }
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized_2;
+    __e_acsl_initialized_2 = __initialized((void *)p,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(p)",13);
+  }
+  __retres = 0;
+  __delete_block((void *)(& b));
+  __delete_block((void *)(& a));
+  __delete_block((void *)(& q));
+  __delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
new file mode 100644
index 0000000000000000000000000000000000000000..0bc419bf7d38a8f6c9d6edc9b80cb4f0d2ba2212
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
@@ -0,0 +1,117 @@
+/* Generated by Frama-C */
+struct __anonstruct___mpz_struct_1 {
+   int _mp_alloc ;
+   int _mp_size ;
+   unsigned long *_mp_d ;
+};
+typedef struct __anonstruct___mpz_struct_1 __mpz_struct;
+typedef __mpz_struct ( __attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef unsigned int size_t;
+/*@ requires predicate ≢ 0;
+    assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void e_acsl_assert(int predicate,
+                                                           char *kind,
+                                                           char *fct,
+                                                           char *pred_txt,
+                                                           int line);
+
+/*@
+model __mpz_struct { ℤ n };
+*/
+int random_counter __attribute__((__unused__));
+unsigned long const rand_max = (unsigned long)32767;
+/*@ ghost extern int __fc_heap_status; */
+
+/*@
+axiomatic
+  dynamic_allocation {
+  predicate is_allocable{L}(size_t n) 
+    reads __fc_heap_status;
+  
+  }
+ */
+/*@ ghost extern int __e_acsl_init; */
+
+/*@ assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1)); */
+extern  __attribute__((__FC_BUILTIN__)) void *__store_block(void *ptr,
+                                                            size_t size);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __delete_block(void *ptr);
+
+/*@ assigns \nothing; */
+extern  __attribute__((__FC_BUILTIN__)) void __full_init(void *ptr);
+
+/*@ ensures \result ≡ 0 ∨ \result ≡ 1;
+    ensures
+      \result ≡ 1 ⇒ \initialized((char *)\old(ptr)+(0 .. \old(size)-1));
+    assigns \result;
+    assigns \result \from *((char *)ptr+(0 .. size-1));
+ */
+extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
+                                                          size_t size);
+
+/*@ ghost extern int __e_acsl_internal_heap; */
+
+/*@ assigns __e_acsl_internal_heap;
+    assigns __e_acsl_internal_heap \from __e_acsl_internal_heap;
+ */
+extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
+
+extern size_t __memory_size;
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+  \at(__memory_size,L1)-\at(__memory_size,L2) ≡ i;
+ */
+int a = 0;
+int b;
+void __e_acsl_memory_init(void)
+{
+  __store_block((void *)(& b),4U);
+  __full_init((void *)(& b));
+  __store_block((void *)(& a),4U);
+  __full_init((void *)(& a));
+  return;
+}
+
+int main(void)
+{
+  int __retres;
+  int *p;
+  int *q;
+  __e_acsl_memory_init();
+  __store_block((void *)(& q),8U);
+  __store_block((void *)(& p),8U);
+  __full_init((void *)(& p));
+  p = & a;
+  __full_init((void *)(& q));
+  q = & b;
+  /*@ assert \initialized(&b); */
+  e_acsl_assert(1,(char *)"Assertion",(char *)"main",
+                (char *)"\\initialized(&b)",11);
+  /*@ assert \initialized(q); */
+  {
+    int __e_acsl_initialized;
+    __e_acsl_initialized = __initialized((void *)q,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(q)",12);
+  }
+  /*@ assert \initialized(p); */
+  {
+    int __e_acsl_initialized_2;
+    __e_acsl_initialized_2 = __initialized((void *)p,(size_t)sizeof(int));
+    e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
+                  (char *)"\\initialized(p)",13);
+  }
+  __retres = 0;
+  __delete_block((void *)(& b));
+  __delete_block((void *)(& a));
+  __delete_block((void *)(& q));
+  __delete_block((void *)(& p));
+  __e_acsl_memory_clean();
+  return __retres;
+}
+
+
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 7dc20a96cfd53a58c2441d391c0a10475e3f8804..6d0b1e9d48c392c949b7b676ca5dfd10a7f9a17d 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
@@ -125,10 +125,13 @@ void __e_acsl_memory_init(void)
   __store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __full_init((void *)(& S2));
   S2 = (char *)__e_acsl_literal_string_3;
   __store_block((void *)(& S),4U);
+  __full_init((void *)(& S));
   S = (char *)__e_acsl_literal_string_2;
   __store_block((void *)(& T),4U);
+  __full_init((void *)(& T));
   T = (char *)__e_acsl_literal_string;
   return;
 }
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 c89ae2de7fdf427a3e34a07402e1ea342ed387cb..d508166dd141edde5be93ab955fa8de8e56ec875 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
@@ -153,10 +153,13 @@ void __e_acsl_memory_init(void)
   __store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __full_init((void *)(& S2));
   S2 = (char *)__e_acsl_literal_string_3;
   __store_block((void *)(& S),4U);
+  __full_init((void *)(& S));
   S = (char *)__e_acsl_literal_string_2;
   __store_block((void *)(& T),4U);
+  __full_init((void *)(& T));
   T = (char *)__e_acsl_literal_string;
   return;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
index b741ebe03b2ecdfe3cfe29da6ccfca233aa931b5..f0adb7fbb68ea72f6ca8f6f908b4f4f62fd63ab2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs.c
@@ -83,7 +83,7 @@ extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
  */
 extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
 
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
 
 /*@
 predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
index cf644234f2a23491775ec663d077c6419fa887ec..7159fdafd4d8381e1668d883ad45e834133a4620 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_mainargs2.c
@@ -157,7 +157,7 @@ extern  __attribute__((__FC_BUILTIN__)) int __initialized(void *ptr,
  */
 extern  __attribute__((__FC_BUILTIN__)) void __e_acsl_memory_clean(void);
 
-/*@ ghost extern size_t __memory_size; */
+extern size_t __memory_size;
 
 /*@
 predicate diffSize{L1, L2}(ℤ i) =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
index b1589c044de5177f7ae5b0d0faf0b94ba4086f67..e9b68efc6f6686046d1a12246a369c6e46605b69 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init.c
@@ -141,7 +141,9 @@ void g(int *C, int *D)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& B),4U);
+  __full_init((void *)(& B));
   __store_block((void *)(& A),4U);
+  __full_init((void *)(& A));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
index b1589c044de5177f7ae5b0d0faf0b94ba4086f67..e9b68efc6f6686046d1a12246a369c6e46605b69 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_ptr_init2.c
@@ -141,7 +141,9 @@ void g(int *C, int *D)
 void __e_acsl_memory_init(void)
 {
   __store_block((void *)(& B),4U);
+  __full_init((void *)(& B));
   __store_block((void *)(& A),4U);
+  __full_init((void *)(& A));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
index 03dcbc74fe611054e145e0798225bfd325e5628f..e2164673fd7b2e2a44bd1647031306d1f3d702c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout.c
@@ -98,7 +98,8 @@ FILE fopen[512];
 FILE const *_p__fc_fopen = (FILE const *)(fopen);
 void __e_acsl_memory_init(void)
 {
-  __store_block((void *)(& stdout),8UL);
+  __store_block((void *)(& stdout),8U);
+  __full_init((void *)(& stdout));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
index 03dcbc74fe611054e145e0798225bfd325e5628f..e2164673fd7b2e2a44bd1647031306d1f3d702c9 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_stdout2.c
@@ -98,7 +98,8 @@ FILE fopen[512];
 FILE const *_p__fc_fopen = (FILE const *)(fopen);
 void __e_acsl_memory_init(void)
 {
-  __store_block((void *)(& stdout),8UL);
+  __store_block((void *)(& stdout),8U);
+  __full_init((void *)(& stdout));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
index 9452c7c80b690a16922d612bb72d0f01a14021f7..785d099d300863e0107e4ad1a9ed22255ab73978 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid.c
@@ -296,8 +296,10 @@ void g(void)
 
 void __e_acsl_memory_init(void)
 {
-  __store_block((void *)(& Z),4UL);
-  __store_block((void *)(& X),8UL);
+  __store_block((void *)(& Z),4U);
+  __full_init((void *)(& Z));
+  __store_block((void *)(& X),8U);
+  __full_init((void *)(& X));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
index 9452c7c80b690a16922d612bb72d0f01a14021f7..785d099d300863e0107e4ad1a9ed22255ab73978 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid2.c
@@ -296,8 +296,10 @@ void g(void)
 
 void __e_acsl_memory_init(void)
 {
-  __store_block((void *)(& Z),4UL);
-  __store_block((void *)(& X),8UL);
+  __store_block((void *)(& Z),4U);
+  __full_init((void *)(& Z));
+  __store_block((void *)(& X),8U);
+  __full_init((void *)(& X));
   return;
 }
 
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1818385f4b262bd98cbccf6310ee6d9b9ca0db19
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
@@ -0,0 +1,34 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/init.c"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+  random_counter ∈ {0}
+  rand_max ∈ {32767}
+  __fc_heap_status ∈ [--..--]
+  __e_acsl_init ∈ [--..--]
+  __e_acsl_internal_heap ∈ [--..--]
+  __memory_size ∈ [--..--]
+  a ∈ {0}
+  b ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid.
+[value] using specification for function __initialized
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.err.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1818385f4b262bd98cbccf6310ee6d9b9ca0db19
--- /dev/null
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle
@@ -0,0 +1,34 @@
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc tests/e-acsl-runtime/init.c"
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[value] Analyzing a complete application starting at main
+[value] Computing initial state
+[value] Initial state computed
+[value] Values of globals at initialization
+  random_counter ∈ {0}
+  rand_max ∈ {32767}
+  __fc_heap_status ∈ [--..--]
+  __e_acsl_init ∈ [--..--]
+  __e_acsl_internal_heap ∈ [--..--]
+  __memory_size ∈ [--..--]
+  a ∈ {0}
+  b ∈ {0}
+[value] using specification for function __store_block
+[value] using specification for function __full_init
+tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid.
+[value] using specification for function e_acsl_assert
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid.
+[value] using specification for function __initialized
+FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid.
+[value] using specification for function __delete_block
+[value] using specification for function __e_acsl_memory_clean
+[value] done for function main
+[value] ====== VALUES COMPUTED ======
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 a1560e2852e3d123c9dc97e800fab132681dc3b2..98f7a282a28bbefebdcaef4efa928c712a50ba70 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
@@ -1,23 +1,23 @@
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
-[kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/ptr_init.c"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/ptr_init.c"
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:144:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:157:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
                   Ignoring annotation.
-FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+FRAMAC_SHARE/libc/stdlib.h:162:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
                   Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
 [value] Analyzing a complete application starting at main
@@ -33,11 +33,11 @@ FRAMAC_SHARE/libc/stdlib.h:149:[e-acsl] warning: E-ACSL construct `logic functio
   A ∈ {0}
   B ∈ {0}
 [value] using specification for function __store_block
+[value] using specification for function __full_init
 [value] using specification for function __malloc
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:147:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:152:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-[value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:160:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:165:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
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 eb6c803cd0a727404577df3647fe0ba810cce596..621c88042bb4330764653e23641263653d6d1acd 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
@@ -1,12 +1,12 @@
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
-[kernel] preprocessing with "gcc -C -E -I.  -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/ptr_init.c"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -IFRAMAC_SHARE/e-acsl -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -DE_ACSL_MACHDEP=x86_32 -IFRAMAC_SHARE/libc -IFRAMAC_SHARE/libc tests/e-acsl-runtime/ptr_init.c"
 [e-acsl] beginning translation.
-FRAMAC_SHARE/libc/stdlib.h:156:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
+FRAMAC_SHARE/libc/stdlib.h:169:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
@@ -29,11 +29,11 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun
   A ∈ {0}
   B ∈ {0}
 [value] using specification for function __store_block
+[value] using specification for function __full_init
 [value] using specification for function __malloc
 [value] using specification for function __delete_block
-FRAMAC_SHARE/libc/stdlib.h:147:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-FRAMAC_SHARE/libc/stdlib.h:152:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-[value] using specification for function __full_init
+FRAMAC_SHARE/libc/stdlib.h:160:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+FRAMAC_SHARE/libc/stdlib.h:165:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid.
 [value] using specification for function e_acsl_assert
 FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index f3658d1f0e18c34d28919dd812e9642973078e32..1035b8e2d0c69cfc56702c4310463c4fe5f17d09 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -128,6 +128,13 @@ class e_acsl_visitor prj generate = object (self)
                     let new_vi = Cil.get_varinfo self#behavior old_vi in
                     let model blk =
                       if Pre_analysis.must_model_vi old_vi then
+                        let blk =
+                          if Kernel.LibEntry.get () then blk
+                          else
+                            Misc.mk_initialize ~loc:Location.unknown
+                              (Cil.var new_vi)
+                            :: blk
+                        in
                         Misc.mk_store_stmt new_vi :: blk
                       else
                         stmts
@@ -208,7 +215,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
                   f.globals <- f.globals @ [ cil_fct ]
             in
             Project.on prj build_initializer ()
-	  end; (* must_init *)
+          end; (* must_init *)
 	  let must_init_args = match main_fct with
 	    | Some main ->
 	       let charPtrPtrType = TPtr(Cil.charPtrType,[]) in
@@ -216,10 +223,11 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
 		  where int/char** arguments is not necessarily
 		  valid *)
 	       (match main.sformals with
-		| vi1::vi2::_ when
-		       vi1.vtype = Cil.intType && vi2.vtype = charPtrPtrType
-		       && Pre_analysis.must_model_vi vi2 -> true
-		| _ -> false)
+               | vi1 :: vi2 :: _ when
+                    vi1.vtype = Cil.intType
+                    && vi2.vtype = charPtrPtrType
+                      && Pre_analysis.must_model_vi vi2 -> true
+               | _ -> false)
 	    | None -> false
 	  in
 	  if must_init_args then begin