diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 2519fb0064de0576bc86fe79f00129b195023b8a..2272cd6fbf17f394290913ac25c51555eb882f92 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -347,10 +347,10 @@ module rec Transfer
     let state = Env.default_varinfos state in
     let extend_to_expr state lhost e =
       let add_vi state vi =
-	if Varinfo.Set.mem vi state then 
+	if is_ptr_or_array_exp e && Varinfo.Set.mem vi state then 
 	  match base_addr e with
 	  | None -> state
-	  | Some vi -> Varinfo.Set.add vi state
+	  | Some vi_e -> Varinfo.Set.add vi_e state
 	else 
 	  state
       in
@@ -423,6 +423,8 @@ module rec Transfer
 	in
 	Dataflow.Done (Some state)
       | _ ->
+	Options.warning "function pointers may introduce too limited \
+instrumentation.";
 	(* imprecise function call: keep each argument *)
 	Dataflow.Done 
 	  (Some
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
index b627514fc2bbf8c68000599673c21213630c9f87..dd75426e2710d1c80972fc4fbf5e138c015e3fee 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
@@ -119,8 +119,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
   void *__retres;
   __store_block((void *)(& __retres),4U);
   __store_block((void *)(& buf),4U);
-  __store_block((void *)(& c),4U);
-  __store_block((void *)(& n),4U);
   {
     int __e_acsl_forall_2;
     unsigned int __e_acsl_k;
@@ -146,7 +144,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
     e_acsl_end_loop3: /* internal */ ;
     __e_acsl_at_4 = __e_acsl_forall_2;
   }
-  __store_block((void *)(& __e_acsl_at_3),4U);
   __e_acsl_at_3 = c;
   __store_block((void *)(& __e_acsl_at_2),4U);
   __e_acsl_at_2 = buf;
@@ -220,8 +217,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
                   (char *)"\\old(\\forall integer k; 0 <= k && k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
                   16);
     __delete_block((void *)(& buf));
-    __delete_block((void *)(& c));
-    __delete_block((void *)(& n));
     __delete_block((void *)(& __retres));
     return __retres;
   }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
index 94bb2b9325de1b9d9312d38501a7201f23f051c4..a63bb3b6309790b40b10d5a0194fcab82cef7b23 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
@@ -174,8 +174,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
   void *__retres;
   __store_block((void *)(& __retres),4U);
   __store_block((void *)(& buf),4U);
-  __store_block((void *)(& c),4U);
-  __store_block((void *)(& n),4U);
   {
     int __e_acsl_forall_2;
     mpz_t __e_acsl_k;
@@ -232,7 +230,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
     __e_acsl_at_4 = __e_acsl_forall_2;
     __gmpz_clear(__e_acsl_k);
   }
-  __store_block((void *)(& __e_acsl_at_3),4U);
   __e_acsl_at_3 = c;
   __store_block((void *)(& __e_acsl_at_2),4U);
   __e_acsl_at_2 = buf;
@@ -365,8 +362,6 @@ void *__e_acsl_memchr(void const *buf, int c, size_t n)
                   (char *)"\\old(\\forall integer k; 0 <= k && k < n ==> (int)*((char *)buf+k) != c) ==>\n\\result == (void *)0",
                   16);
     __delete_block((void *)(& buf));
-    __delete_block((void *)(& c));
-    __delete_block((void *)(& n));
     __delete_block((void *)(& __retres));
     return __retres;
   }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
index c272c755172f972c62f2d40a0f1d9ebbe1015363..6b1383de20e5c18e4a3b2e6ea647b8234839e958 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
@@ -135,9 +135,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
index 92292d850149214b83d2e7c45b1b6e3e2cf9192c..41010eccee50a97cf2ade4e491786553b9c04ce2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
@@ -182,9 +182,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
index 9908ad514ecb92f741442f58cbd217132b8f2f00..d861adcd1f81db381fff27d586e4872a235d5882 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar.c
@@ -107,9 +107,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
index 9908ad514ecb92f741442f58cbd217132b8f2f00..d861adcd1f81db381fff27d586e4872a235d5882 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_localvar2.c
@@ -107,9 +107,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
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 8f6be0936163a0e009bbdf3eb04d47c0a3c11d3c..14648a95ec46a915185e1bd4fc65d1819f890536 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
@@ -100,9 +100,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
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 8f6be0936163a0e009bbdf3eb04d47c0a3c11d3c..14648a95ec46a915185e1bd4fc65d1819f890536 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
@@ -100,9 +100,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
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 81f667be94f9891ae1b3d445da839f2d8234b3d2..6e1b00a2313c1aa1fcea5a814774eedee63e57f4 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
@@ -124,9 +124,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
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 81f667be94f9891ae1b3d445da839f2d8234b3d2..6e1b00a2313c1aa1fcea5a814774eedee63e57f4 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
@@ -124,9 +124,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
index c2f4f1fbc0727b4631ded1f9e41fac8e1c5b8c46..39bfc7e30e1b573b90baa6948ae335d9f9c17abd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias.c
@@ -132,9 +132,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
@@ -180,10 +178,8 @@ int main(void)
   int *a;
   int *b;
   int n;
-  __store_block((void *)(& n),4U);
   __store_block((void *)(& b),4U);
   __store_block((void *)(& a),4U);
-  __full_init((void *)(& n));
   n = 0;
   /*@ assert ¬\valid(a) ∧ ¬\valid(b); */
   {
@@ -293,7 +289,6 @@ int main(void)
                   (char *)"!\\valid(a) && !\\valid(b)",19);
   }
   __retres = 0;
-  __delete_block((void *)(& n));
   __delete_block((void *)(& b));
   __delete_block((void *)(& a));
   __clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
index 6365593033b77078bff5aadbcc81b24c93fcc91f..5c79ab7a56794d4e4751a1357951ec09cbf6a4d3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_alias2.c
@@ -148,9 +148,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
@@ -196,10 +194,8 @@ int main(void)
   int *a;
   int *b;
   int n;
-  __store_block((void *)(& n),4U);
   __store_block((void *)(& b),4U);
   __store_block((void *)(& a),4U);
-  __full_init((void *)(& n));
   n = 0;
   /*@ assert ¬\valid(a) ∧ ¬\valid(b); */
   {
@@ -307,7 +303,6 @@ int main(void)
                   (char *)"!\\valid(a) && !\\valid(b)",19);
   }
   __retres = 0;
-  __delete_block((void *)(& n));
   __delete_block((void *)(& b));
   __delete_block((void *)(& a));
   __clean();
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
index 2b9123b2a6a669af3389bf7703440addc0b764a3..7c4d9feda33f606ed1f721fa26a87bb4ab301a84 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector.c
@@ -125,9 +125,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
@@ -170,7 +168,6 @@ int *new_inversed(int len, int *v)
   int i;
   int *p;
   __store_block((void *)(& p),4U);
-  __store_block((void *)(& v),4U);
   __full_init((void *)(& p));
   p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned int)len);
   i = 0;
@@ -179,7 +176,6 @@ int *new_inversed(int len, int *v)
     *(p + i) = *(v + ((len - i) - 1));
     i ++;
   }
-  __delete_block((void *)(& v));
   __delete_block((void *)(& p));
   return p;
 }
@@ -187,23 +183,25 @@ int *new_inversed(int len, int *v)
 int main(void)
 {
   int __retres;
+  int x;
   int v1[3];
   int *v2;
   __store_block((void *)(& v2),4U);
   __store_block((void *)(v1),12U);
+  x = 3;
   __initialize((void *)(v1),sizeof(int));
   v1[0] = 1;
   __initialize((void *)(& v1[1]),sizeof(int));
   v1[1] = 2;
   __initialize((void *)(& v1[2]),sizeof(int));
-  v1[2] = 3;
+  v1[2] = x;
   LAST = v1[2];
   /*@ assert \initialized(&v1[2]); */
   {
     int __e_acsl_initialized;
     __e_acsl_initialized = __initialized((void *)(& v1[2]),sizeof(int));
     e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&v1[2])",25);
+                  (char *)"\\initialized(&v1[2])",26);
   }
   __full_init((void *)(& v2));
   v2 = new_inversed(3,v1);
@@ -213,11 +211,11 @@ int main(void)
     int __e_acsl_initialized_2;
     __e_acsl_initialized_2 = __initialized((void *)(v2 + 2),sizeof(int));
     e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(v2+2)",28);
+                  (char *)"\\initialized(v2+2)",29);
   }
   /*@ assert LAST ≡ 1; */
   e_acsl_assert(LAST == 1,(char *)"Assertion",(char *)"main",
-                (char *)"LAST == 1",29);
+                (char *)"LAST == 1",30);
   __e_acsl_free((void *)v2);
   __retres = 0;
   __delete_block((void *)(& v2));
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
index abb78f1e956f115eddbe068624b04945a396d804..3756d1802cf72398ac90c143f79d678defd0baf3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_vector2.c
@@ -145,9 +145,7 @@ void *__e_acsl_malloc(size_t size)
 {
   void *__retres;
   __store_block((void *)(& __retres),4U);
-  __store_block((void *)(& size),4U);
   __retres = __malloc(size);
-  __delete_block((void *)(& size));
   __delete_block((void *)(& __retres));
   return __retres;
 }
@@ -190,7 +188,6 @@ int *new_inversed(int len, int *v)
   int i;
   int *p;
   __store_block((void *)(& p),4U);
-  __store_block((void *)(& v),4U);
   __full_init((void *)(& p));
   p = (int *)__e_acsl_malloc(sizeof(int) * (unsigned int)len);
   i = 0;
@@ -199,7 +196,6 @@ int *new_inversed(int len, int *v)
     *(p + i) = *(v + ((len - i) - 1));
     i ++;
   }
-  __delete_block((void *)(& v));
   __delete_block((void *)(& p));
   return p;
 }
@@ -207,23 +203,25 @@ int *new_inversed(int len, int *v)
 int main(void)
 {
   int __retres;
+  int x;
   int v1[3];
   int *v2;
   __store_block((void *)(& v2),4U);
   __store_block((void *)(v1),12U);
+  x = 3;
   __initialize((void *)(v1),sizeof(int));
   v1[0] = 1;
   __initialize((void *)(& v1[1]),sizeof(int));
   v1[1] = 2;
   __initialize((void *)(& v1[2]),sizeof(int));
-  v1[2] = 3;
+  v1[2] = x;
   LAST = v1[2];
   /*@ assert \initialized(&v1[2]); */
   {
     int __e_acsl_initialized;
     __e_acsl_initialized = __initialized((void *)(& v1[2]),sizeof(int));
     e_acsl_assert(__e_acsl_initialized,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(&v1[2])",25);
+                  (char *)"\\initialized(&v1[2])",26);
   }
   __full_init((void *)(& v2));
   v2 = new_inversed(3,v1);
@@ -234,7 +232,7 @@ int main(void)
     __e_acsl_initialized_2 = __initialized((void *)(v2 + (long)2),
                                            sizeof(int));
     e_acsl_assert(__e_acsl_initialized_2,(char *)"Assertion",(char *)"main",
-                  (char *)"\\initialized(v2+2)",28);
+                  (char *)"\\initialized(v2+2)",29);
   }
   /*@ assert LAST ≡ 1; */
   {
@@ -246,7 +244,7 @@ int main(void)
     __e_acsl_eq = __gmpz_cmp((__mpz_struct const *)(__e_acsl_LAST),
                              (__mpz_struct const *)(__e_acsl));
     e_acsl_assert(__e_acsl_eq == 0,(char *)"Assertion",(char *)"main",
-                  (char *)"LAST == 1",29);
+                  (char *)"LAST == 1",30);
     __gmpz_clear(__e_acsl_LAST);
     __gmpz_clear(__e_acsl);
   }
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 fa36eac9c68d7c64a68cc5f48989060590612542..359ee4a6b87ddd15e006a6a9d4b7f824a5df4afe 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
@@ -27,7 +27,6 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
         __fc_heap_status ∈ [--..--]
         __memory_size ∈ [--..--]
 [value] using specification for function __store_block
-[value] using specification for function __full_init
 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.
@@ -42,6 +41,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
         (void *)b
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __full_init
 [value] using specification for function __delete_block
 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.)
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 8dda7f0f77591ff2133b577cc88278ec9cb7a493..8badb6e0c194fec989ba560e19476152fcc07f41 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
@@ -27,7 +27,6 @@ tests/e-acsl-runtime/valid_alias.c:10:[e-acsl] warning: E-ACSL construct `\alloc
         __fc_heap_status ∈ [--..--]
         __memory_size ∈ [--..--]
 [value] using specification for function __store_block
-[value] using specification for function __full_init
 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.
@@ -42,6 +41,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] all evaluations are invalid for fu
         (void *)b
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __full_init
 [value] using specification for function __delete_block
 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.)
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 4cbe715e4e6230f70cd527878a3594a574ae1ec5..7d4344f8717d6c437f48a4a0541b4f3829d6a17e 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
@@ -29,7 +29,7 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
         LAST ∈ {0}
 [value] using specification for function __store_block
 [value] using specification for function __initialize
-tests/e-acsl-runtime/vector.c:25:[value] Assertion got status valid.
+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.
@@ -40,9 +40,9 @@ 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/vector.c:16:[value] entering loop for the first time
-tests/e-acsl-runtime/vector.c:28:[value] Assertion got status unknown.
 tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
 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.
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
@@ -62,6 +62,7 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
 [value] Values at end of function main:
           __fc_heap_status ∈ [--..--]
           LAST ∈ {1; 2; 3} or UNINITIALIZED
+          x ∈ {3}
           v1[0] ∈ {1}
             [1] ∈ {2}
             [2] ∈ {3}
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 1d5f127b3f4aedb90a6a920aa9b4f43c52a80d18..3b69442f242a9eb2aa78b7675862d5c5c297ee00 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
@@ -29,7 +29,7 @@ tests/e-acsl-runtime/vector.c:21:[e-acsl] warning: E-ACSL construct `\allocate'
         LAST ∈ {0}
 [value] using specification for function __store_block
 [value] using specification for function __initialize
-tests/e-acsl-runtime/vector.c:25:[value] Assertion got status valid.
+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.
@@ -40,9 +40,9 @@ 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/vector.c:16:[value] entering loop for the first time
-tests/e-acsl-runtime/vector.c:28:[value] Assertion got status unknown.
 tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown.
-tests/e-acsl-runtime/vector.c:29:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
+tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown.
+tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value: assert \initialized(&LAST);
 [value] using specification for function __gmpz_init_set_si
 share/e-acsl/e_acsl_gmp.h:61:[value] Function __gmpz_init_set_si: precondition got status valid.
 share/e-acsl/e_acsl_gmp.h:63:[value] Function __gmpz_init_set_si: postcondition got status valid.
@@ -71,6 +71,7 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
 [value] Values at end of function main:
           __fc_heap_status ∈ [--..--]
           LAST ∈ {1; 2; 3} or UNINITIALIZED
+          x ∈ {3}
           v1[0] ∈ {1}
             [1] ∈ {2}
             [2] ∈ {3}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
index a2870eb277ce7b69cb12adeca76d90f4d6853fd3..d86ef57b989320be2d4c754d7a373a14fc15e93e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/vector.c
@@ -19,7 +19,8 @@ int* new_inversed(int len, int *v) {
 }
 
 int main(void) {
-  int v1[3]= { 1, 2, 3}, *v2;
+  int x = 3;
+  int v1[3]= { 1, 2, x }, *v2;
   // @ assert \valid(&v1[2]);
   LAST = v1[2]; 
   //@ assert \initialized(v1+2);