diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index b9b703500a4b055166fccb6160c075e4374578cc..8f2368d634f247696727ea6a94b8d3fd774f8143 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -41,8 +41,7 @@ module Env: sig
   val clear: unit -> unit
   val add: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t -> unit
   val find: kernel_function -> Varinfo.Set.t option Stmt.Hashtbl.t 
-  module StartData: Dataflow.StmtStartData with type key = stmt
-					   and type data = Varinfo.Set.t option
+  module StartData: Dataflow.StmtStartData with type data = Varinfo.Set.t option
   val is_consolidated: unit -> bool
   val consolidate: Varinfo.Set.t -> unit
   val consolidated_mem: varinfo -> bool
@@ -104,7 +103,6 @@ let reset = Env.clear
 
 module rec Transfer
   : Dataflow.BackwardsTransfer with type t = Varinfo.Set.t option
-			       and type StmtStartData.key = stmt
   = struct
 
   let name = "E_ACSL.Pre_analysis"
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
index c1e242e49a2a2a92c279f72f8d8a02f6190ce688..ffe00ca28e047e11a153cc0376db8599dc62a91b 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.c
@@ -77,7 +77,7 @@ void _free(void* ptr) {
 /* resize the block starting at ptr to fit its new size,
  * for further information, see realloc */
 void* _realloc(void* ptr, size_t size) {
-  struct _block * tmp, * next;
+  struct _block * tmp;
   void * new_ptr;
   if(ptr == NULL) return _malloc(size);
   if(size <= 0) {
@@ -99,7 +99,7 @@ void* _realloc(void* ptr, size_t size) {
       tmp->init_cpt = size;
     /* realloc bigger larger block */
     else {
-      int i, nb = needed_bytes(size);
+      int nb = needed_bytes(size);
       tmp->init_ptr = malloc(nb);
       memset(tmp->init_ptr, 0xFF, nb);
       if(size%8 != 0)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index bcab71e5a5dfee855d4bc2f39661759f8a15c49f..35ae99fd497aaedd2a43ba674396ef4ea8b6d60f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -198,8 +198,7 @@ tests/e-acsl-runtime/bts1307.i:13:[value] warning: converting value to float: as
 [value] computing for function __gmpz_clear <- foo <- main.
         Called from tests/e-acsl-runtime/bts1307.i:13.
 [value] Done for function __gmpz_clear
-tests/e-acsl-runtime/bts1307.i:17:[value] warning: converting value to float: assert(Ook)
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status unknown.
+tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
 [value] Recording results for foo
 [value] Done for function foo
 [value] computing for function bar <- main.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index 1fa6df12114d9df4373348f679028429a0fcd8e6..5e00a8753fae41d83232209d60512d67d5d63d93 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -140,8 +140,7 @@ tests/e-acsl-runtime/bts1307.i:13:[value] warning: converting value to float: as
 [value] computing for function _delete_block <- foo <- main.
         Called from tests/e-acsl-runtime/bts1307.i:15.
 [value] Done for function _delete_block
-tests/e-acsl-runtime/bts1307.i:17:[value] warning: converting value to float: assert(Ook)
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status unknown.
+tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
 [value] Recording results for foo
 [value] Done for function foo
 [value] computing for function bar <- main.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index 312f7e539055e4d383e91f9360960d7fd9f497b2..155a286ac5d66d4761f7464ede9253398e686d3d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -112,8 +112,8 @@ tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/literal_string.i:25.
 [value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
 [value] Done for function _initialized
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/literal_string.i:25.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index 8dea4c78dfa8153796717f0a11565b47c21862a8..543300f7810f2541ad9f7bfd6706e9d158158897 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -90,8 +90,8 @@ tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid.
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/literal_string.i:25.
 [value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
 [value] Done for function _initialized
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/literal_string.i:25.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index 56eeebe5710de12e5fa4d5067cd2cd5c0b06cb73..0946a1304328f8061303bcf6240c5429262fa89a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -40,8 +40,8 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] computing for function _initialized <- add <- main.
         Called from tests/e-acsl-runtime/localvar.c:20.
 [value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
 [value] Done for function _initialized
 [value] computing for function _valid <- add <- main.
         Called from tests/e-acsl-runtime/localvar.c:20.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index 56eeebe5710de12e5fa4d5067cd2cd5c0b06cb73..0946a1304328f8061303bcf6240c5429262fa89a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -40,8 +40,8 @@ tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid.
 [value] computing for function _initialized <- add <- main.
         Called from tests/e-acsl-runtime/localvar.c:20.
 [value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
 [value] Done for function _initialized
 [value] computing for function _valid <- add <- main.
         Called from tests/e-acsl-runtime/localvar.c:20.
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 f48806548695a518d3ffeedf1922575aed36f20e..9e384cf660ad4adf1649cc1eb38319db362b4948 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
@@ -46,8 +46,8 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/valid_alias.c:12.
 [value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
 [value] Done for function _initialized
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
@@ -78,7 +78,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/valid_alias.c:16.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
 [value] Done for function _initialized
 [value] computing for function _valid <- main.
         Called from tests/e-acsl-runtime/valid_alias.c:16.
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 de38f7f5a09f14e7a66b0b4e920cdbd0d510de15..ab2d470262fd15f8318e1d45f68473912133b056 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
@@ -45,8 +45,8 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid.
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/valid_alias.c:12.
 [value] using specification for function _initialized
-./share/e-acsl/memory_model/e_acsl_mmodel.h:57:[value] Function _initialized: postcondition got status unknown.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:84:[value] Function _initialized: postcondition got status unknown.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status unknown.
 [value] Done for function _initialized
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: accessing uninitialized left-value: assert \initialized(&a);
 tests/e-acsl-runtime/valid_alias.c:12:[kernel] warning: completely indeterminate value in a.
@@ -77,7 +77,7 @@ tests/e-acsl-runtime/valid_alias.c:12:[value] Non-termination in evaluation of f
 tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 [value] computing for function _initialized <- main.
         Called from tests/e-acsl-runtime/valid_alias.c:16.
-./share/e-acsl/memory_model/e_acsl_mmodel.h:58:[value] Function _initialized: postcondition got status valid.
+./share/e-acsl/memory_model/e_acsl_mmodel.h:85:[value] Function _initialized: postcondition got status valid.
 [value] Done for function _initialized
 [value] computing for function _valid <- main.
         Called from tests/e-acsl-runtime/valid_alias.c:16.