diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 505eb087adc2a58c262ce7141d96848383e686fb..c0b61d74d730b413cfed16eb1768ad03b8d11eb2 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -25,14 +25,13 @@
   (voir test result.i, cas -e-acsl-gmp-only)
 - générer les delete des globals dans une fonction séparée, comme pour les init.
 - variadic functions are not yet duplicated
-- generate guard for \offset & co (\offset(p) must ensures that p is valid)
-- improve computation of the initial state of the dataflow analysis
+- generate guard for \offset, \block_length and \base_addr
+  (\offset(p) must ensures that p is valid)
 - don't generate code for properties with status valid_under_hyp when we know
   that the hyp will be generated
 - use value analysis whenever possible instead of our own imprecise analysis
 - use checked assigns whenever possible in the analysis
   checked property = valid property or property for which code will be generated
-- fix \offset, \block_length and \base_addr
 - RTE avec du code GMP
 
 ##############
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 8a01e0e43700384ceb72dbb4d7c4d15ad3201c71..b0e13ff81d64b490448366acf53667f069a32d0b 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -285,7 +285,7 @@ module rec Transfer
       (fun state ->
 	let state = Env.default_varinfos state in
 	let state = 
-	  if is_first || is_last then 
+	  if (is_first || is_last) && Misc.is_generated_kf kf then 
 	    Annotations.fold_behaviors
 	      (fun _ bhv s -> 
 		let handle_annot test f s =
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index 81e304bee5105ddd19e19628a299d91e01f74de0..701e70d1ec9f0990ad82def463e48f1ada25a498 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -48,10 +48,10 @@ share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got s
 tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
 tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
 tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-[value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
+[value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index a4a9ff1b0dba1cd395ea1bf8fadd7f10444e18e9..3f65dd22867327a387486af6bdd8f2be5fa768b4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -22,9 +22,9 @@
 [value] using specification for function e_acsl_assert
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
 tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-[value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
 tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
index 5d1ddfc9fb538cb14184069331353046f9d48d9a..1421ddbabe9ad8159dfefdc0287b533231296cca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
@@ -64,8 +64,6 @@ int sorted(int *t, int n)
 {
   int __retres;
   int b;
-  __store_block((void *)(& t),4U);
-  __full_init((void *)(& t));
   b = 1;
   if (n <= 1) {
     __retres = 1;
@@ -80,9 +78,7 @@ int sorted(int *t, int n)
     b ++;
   }
   __retres = 1;
-  return_label: /* internal */
-    __delete_block((void *)(& t));
-    return __retres;
+  return_label: /* internal */ return __retres;
 }
 
 /*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
index 2b3a02ae35b50a7521af610e483745a6fe2bb6c7..990bc56bd1be6c3efedc0af2de495da594dec760 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
@@ -119,8 +119,6 @@ int sorted(int *t, int n)
 {
   int __retres;
   int b;
-  __store_block((void *)(& t),4U);
-  __full_init((void *)(& t));
   b = 1;
   if (n <= 1) {
     __retres = 1;
@@ -135,9 +133,7 @@ int sorted(int *t, int n)
     b ++;
   }
   __retres = 1;
-  return_label: /* internal */
-    __delete_block((void *)(& t));
-    return __retres;
+  return_label: /* internal */ return __retres;
 }
 
 /*@ behavior yes:
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 6b73631e3229d7ed6bb139ddefabc0c543c284a6..eed220126b040cfe038005172621b8c94a826f96 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
@@ -74,29 +74,21 @@ void *memchr(void const *buf, int c, size_t n)
   void *__retres;
   int i;
   char *s;
-  __store_block((void *)(& s),4U);
-  __store_block((void *)(& __retres),4U);
   __store_block((void *)(& buf),4U);
   __full_init((void *)(& buf));
-  __full_init((void *)(& s));
   s = (char *)buf;
   i = 0;
   while ((size_t)i < n) {
     if ((int)*s == c) {
-      __full_init((void *)(& __retres));
       __retres = (void *)s;
       goto return_label;
     }
-    __full_init((void *)(& s));
     s ++;
     i ++;
   }
-  __full_init((void *)(& __retres));
   __retres = (void *)0;
   return_label: /* internal */
     __delete_block((void *)(& buf));
-    __delete_block((void *)(& s));
-    __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 b20cf19b813b018170aa87bb2339791970c22550..29aaa98132faf8dfb64fe08fa8714c02e03bf6e0 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
@@ -129,29 +129,21 @@ void *memchr(void const *buf, int c, size_t n)
   void *__retres;
   int i;
   char *s;
-  __store_block((void *)(& s),4U);
-  __store_block((void *)(& __retres),4U);
   __store_block((void *)(& buf),4U);
   __full_init((void *)(& buf));
-  __full_init((void *)(& s));
   s = (char *)buf;
   i = 0;
   while ((size_t)i < n) {
     if ((int)*s == c) {
-      __full_init((void *)(& __retres));
       __retres = (void *)s;
       goto return_label;
     }
-    __full_init((void *)(& s));
     s ++;
     i ++;
   }
-  __full_init((void *)(& __retres));
   __retres = (void *)0;
   return_label: /* internal */
     __delete_block((void *)(& buf));
-    __delete_block((void *)(& s));
-    __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 3ec6a39d6edc5759a804fd816bc5e1e283e035b7..aaf10d25d9a1221e5eb3980fe937259d7f09aa79 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
@@ -186,7 +186,6 @@ int *f(int *x)
     e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"f",
                   (char *)"!\\valid(y)",19);
   }
-  __full_init((void *)(& y));
   y = x;
   /*@ assert \valid(x); */
   {
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 3ec6a39d6edc5759a804fd816bc5e1e283e035b7..aaf10d25d9a1221e5eb3980fe937259d7f09aa79 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
@@ -186,7 +186,6 @@ int *f(int *x)
     e_acsl_assert(! __e_acsl_and,(char *)"Assertion",(char *)"f",
                   (char *)"!\\valid(y)",19);
   }
-  __full_init((void *)(& y));
   y = x;
   /*@ assert \valid(x); */
   {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
index 359dfcc485cadb7a88cf3bf70620784c4b858ce0..9f2f6dba7d3e4253a47cfa7de9ddad372872a030 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract.c
@@ -79,8 +79,6 @@ predicate diffSize{L1, L2}(ℤ i) =
 struct list *f(struct list *l)
 {
   struct list *__retres;
-  __store_block((void *)(& l),4U);
-  __full_init((void *)(& l));
   if (l == (void *)0) {
     __retres = l;
     goto return_label;
@@ -90,9 +88,7 @@ struct list *f(struct list *l)
     goto return_label;
   }
   __retres = (struct list *)((void *)0);
-  return_label: /* internal */
-    __delete_block((void *)(& l));
-    return __retres;
+  return_label: /* internal */ return __retres;
 }
 
 /*@ behavior B1:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
index 359dfcc485cadb7a88cf3bf70620784c4b858ce0..9f2f6dba7d3e4253a47cfa7de9ddad372872a030 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_valid_in_contract2.c
@@ -79,8 +79,6 @@ predicate diffSize{L1, L2}(ℤ i) =
 struct list *f(struct list *l)
 {
   struct list *__retres;
-  __store_block((void *)(& l),4U);
-  __full_init((void *)(& l));
   if (l == (void *)0) {
     __retres = l;
     goto return_label;
@@ -90,9 +88,7 @@ struct list *f(struct list *l)
     goto return_label;
   }
   __retres = (struct list *)((void *)0);
-  return_label: /* internal */
-    __delete_block((void *)(& l));
-    return __retres;
+  return_label: /* internal */ return __retres;
 }
 
 /*@ behavior B1:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 4dc384ce71db9502e73b7630b65cc4696c89ec3c..23998488d262f3bc55b41cf20e824a572e3faa22 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -27,10 +27,10 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
 tests/e-acsl-runtime/valid_in_contract.c:21:[value] all evaluations are invalid for function call argument
         (void *)l->next
-[value] using specification for function __delete_block
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 4dc384ce71db9502e73b7630b65cc4696c89ec3c..23998488d262f3bc55b41cf20e824a572e3faa22 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -27,10 +27,10 @@ share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status
 tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next);
 tests/e-acsl-runtime/valid_in_contract.c:21:[value] all evaluations are invalid for function call argument
         (void *)l->next
-[value] using specification for function __delete_block
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 share/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
+[value] using specification for function __delete_block
 tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid.
 tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
 [kernel] warning: Neither code nor specification for function __clean, generating default assigns from the prototype