diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
index e38e2dfb3f63a53aeb64b7909e1dc66d90511768..1ab256f0b6655b131a7bad31ad715881335ce8bb 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_bittree.c
@@ -312,11 +312,11 @@ void __add_element (struct _block * ptr) {
 }
 
 
-/* return the block B such as : begin addr of B == ptr
-   we suppose that such a block exists, but we could return NULL if not */
+/* return the block B such as: begin addr of B == ptr if such a block exists,
+   return NULL otherwise */
 /*@ assigns \nothing;
   @ ensures \valid(\result);
-  @ ensures \result->ptr == (size_t)ptr;
+  @ ensures \result == \null || \result->ptr == (size_t)ptr;
   @*/
 struct _block * __get_exact (void * ptr) {
   struct bittree * tmp = __root;
@@ -326,8 +326,8 @@ struct _block * __get_exact (void * ptr) {
   /*@ loop assigns tmp;
     @*/
   while(!tmp->is_leaf) {
-    // prefix is consistent
-    assert((tmp->addr & tmp->mask) == ((size_t)ptr & tmp->mask));
+    // if the ptr we are looking for does not share the prefix of tmp
+    if((tmp->addr & tmp->mask) != ((size_t)ptr & tmp->mask)) return NULL;
     // two sons
     assert(tmp->left != NULL && tmp->right != NULL);
     // the prefix of one son is consistent
@@ -337,12 +337,10 @@ struct _block * __get_exact (void * ptr) {
     else if((tmp->left->addr & tmp->left->mask)
 	    == ((size_t)ptr & tmp->left->mask))
       tmp = tmp->left;
-    else
-      assert(0);
+    else return NULL;
   }
 
-  assert(tmp->is_leaf);
-  assert(tmp->leaf->ptr == (size_t)ptr);
+  if(tmp->leaf->ptr != (size_t)ptr) return NULL;
   return tmp->leaf;
 }
 
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 9f252b1a2e1d3655a9dd71d1c9afb24d6b3147a5..f8ea8707d4145c86f9e607cdb3394df2c0e83746 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
@@ -56,6 +56,7 @@ void* __e_acsl_mmodel_memset (void* dest, int val, size_t len) {
 
 
 size_t __memory_size = 0;
+struct _block * last_added_block = NULL; /* proceed with caution */
 /*unsigned cpt_store_block = 0;*/
 
 const int nbr_bits_to_1[256] = {
@@ -103,7 +104,9 @@ void* __store_block(void* ptr, size_t size) {
   tmp->init_cpt = 0;
   tmp->is_litteral_string = false;
   tmp->is_out_of_bound = false;
+  tmp->freeable = false;
   __add_element(tmp);
+  last_added_block = tmp;
   /*cpt_store_block++;*/
   return ptr;
 }
@@ -128,7 +131,8 @@ void* __malloc(size_t size) {
   if(tmp == NULL) return NULL;
   tmp2 = __store_block(tmp, size);
   __memory_size += size;
-  assert(tmp2 != NULL);
+  assert(tmp2 != NULL && last_added_block != NULL);
+  last_added_block->freeable = true;
   return tmp2;
 }
 
@@ -146,6 +150,14 @@ void __free(void* ptr) {
   free(tmp);
 }
 
+int __freeable(void* ptr) {
+  struct _block * tmp;
+  if(ptr == NULL) return false;
+  tmp = __get_exact(ptr);
+  if(tmp == NULL) return false;
+  return tmp->freeable;
+}
+
 /* resize the block starting at ptr to fit its new size,
  * for further information, see realloc */
 void* __realloc(void* ptr, size_t size) {
@@ -197,6 +209,7 @@ void* __realloc(void* ptr, size_t size) {
     }
   }
   tmp->size = size;
+  tmp->freeable = true;
   __memory_size += size;
   return (void*)tmp->ptr;
 }
@@ -211,7 +224,8 @@ void* __calloc(size_t nbr_block, size_t size_block) {
   if(tmp == NULL) return NULL;
   tmp2 = __store_block(tmp, nbr_block * size_block);
   __memory_size += nbr_block * size_block;
-  assert(tmp2 != NULL);
+  assert(tmp2 != NULL && last_added_block != NULL);
+  last_added_block->freeable = true;
   return tmp2;
 }
 
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
index 7dd28d91f6c9b086d45f154f997266a29fef3211..052bde62c82e2c9cc9d508fe7ce1ccd2074abfc0 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel.h
@@ -38,6 +38,10 @@ void * __malloc(size_t size)
 void __free(void * ptr)
   __attribute__((FC_BUILTIN));
 
+/*@ assigns \result \from ptr; */
+int __freeable(void * ptr)
+  __attribute__((FC_BUILTIN));
+
 /* resize the block starting at ptr to fit its new size,
  * for further information, see realloc */
 /*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
index d4cfb55ebf1da59d762fa7dca8de45b08c43a859..2805f60fb51a05929cf95ed9d5630ac9b2f0fdef 100644
--- a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_mmodel_api.h
@@ -47,6 +47,7 @@ struct _block {
   size_t init_cpt;
   _Bool is_litteral_string;
   _Bool is_out_of_bound;
+  _Bool freeable;
 };
 
 /* print the information about a block */