From 72f9bfb7d7482cee5ef1fa4841679e9751782428 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 5 Aug 2014 13:44:05 +0200
Subject: [PATCH] fixed bug #1818 about initialization of globals

---
 src/plugins/e-acsl/doc/Changelog              |   1 +
 .../e-acsl/tests/e-acsl-runtime/init.c        |  14 +++
 .../oracle/bts1478.1.res.oracle               |   1 +
 .../e-acsl-runtime/oracle/bts1478.res.oracle  |   1 +
 .../tests/e-acsl-runtime/oracle/gen_bts1478.c |   5 +
 .../e-acsl-runtime/oracle/gen_bts14782.c      |   5 +
 .../tests/e-acsl-runtime/oracle/gen_ghost.c   |   2 +
 .../tests/e-acsl-runtime/oracle/gen_ghost2.c  |   2 +
 .../tests/e-acsl-runtime/oracle/gen_init.c    | 117 ++++++++++++++++++
 .../tests/e-acsl-runtime/oracle/gen_init2.c   | 117 ++++++++++++++++++
 .../oracle/gen_literal_string.c               |   3 +
 .../oracle/gen_literal_string2.c              |   3 +
 .../e-acsl-runtime/oracle/gen_mainargs.c      |   2 +-
 .../e-acsl-runtime/oracle/gen_mainargs2.c     |   2 +-
 .../e-acsl-runtime/oracle/gen_ptr_init.c      |   2 +
 .../e-acsl-runtime/oracle/gen_ptr_init2.c     |   2 +
 .../tests/e-acsl-runtime/oracle/gen_stdout.c  |   3 +-
 .../tests/e-acsl-runtime/oracle/gen_stdout2.c |   3 +-
 .../tests/e-acsl-runtime/oracle/gen_valid.c   |   6 +-
 .../tests/e-acsl-runtime/oracle/gen_valid2.c  |   6 +-
 .../e-acsl-runtime/oracle/init.1.err.oracle   |   0
 .../e-acsl-runtime/oracle/init.1.res.oracle   |  34 +++++
 .../e-acsl-runtime/oracle/init.err.oracle     |   0
 .../e-acsl-runtime/oracle/init.res.oracle     |  34 +++++
 .../oracle/ptr_init.1.res.oracle              |  28 ++---
 .../e-acsl-runtime/oracle/ptr_init.res.oracle |  22 ++--
 src/plugins/e-acsl/visit.ml                   |  18 ++-
 27 files changed, 395 insertions(+), 38 deletions(-)
 create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/init.c
 create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init.c
 create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_init2.c
 create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.err.oracle
 create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle
 create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.err.oracle
 create mode 100644 src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.res.oracle

diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 611e2eb01bd..a0cc7fef9f4 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 00000000000..e7a5a17ddbb
--- /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 44f5c5647e5..889dfbfd3a5 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 76d0e9b7e0a..d794b166518 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 515980fc04b..1af8751dd51 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 83ff924f0a4..b0fc6e014d1 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 a58680ab4e8..764d3802ca8 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 82da68f4bfd..818ce62654d 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 00000000000..0bc419bf7d3
--- /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 00000000000..0bc419bf7d3
--- /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 7dc20a96cfd..6d0b1e9d48c 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 c89ae2de7fd..d508166dd14 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 b741ebe03b2..f0adb7fbb68 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 cf644234f2a..7159fdafd4d 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 b1589c044de..e9b68efc6f6 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 b1589c044de..e9b68efc6f6 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 03dcbc74fe6..e2164673fd7 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 03dcbc74fe6..e2164673fd7 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 9452c7c80b6..785d099d300 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 9452c7c80b6..785d099d300 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 00000000000..e69de29bb2d
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 00000000000..1818385f4b2
--- /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 00000000000..e69de29bb2d
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 00000000000..1818385f4b2
--- /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 a1560e2852e..98f7a282a28 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 eb6c803cd0a..621c88042bb 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 f3658d1f0e1..1035b8e2d0c 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
-- 
GitLab