diff --git a/src/plugins/e-acsl/gcc_test.sh b/src/plugins/e-acsl/gcc_test.sh
index 44e68c2ae9a041fa8d80bdb5933b7591940d5be1..537be69e917113cc86da38e874c4309d1bb6d639 100755
--- a/src/plugins/e-acsl/gcc_test.sh
+++ b/src/plugins/e-acsl/gcc_test.sh
@@ -1,2 +1,8 @@
#!/bin/sh
gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_bittree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_list.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_splay_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
+
+gcc -std=c99 -pedantic -Wall -Wno-long-long -Wno-attributes -Wno-unused-but-set-variable -fno-builtin $2 -o ./tests/e-acsl-runtime/result/gen_$1.out ./share/e-acsl/e_acsl.c ./share/e-acsl/memory_model/e_acsl_tree.c ./share/e-acsl/memory_model/e_acsl_mmodel.c ./tests/e-acsl-runtime/result/gen_$1.c -lgmp && ./tests/e-acsl-runtime/result/gen_$1.out
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
new file mode 100644
index 0000000000000000000000000000000000000000..0a92ae1f278ce7841358340c237fe9958c08b70e
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_list.c
@@ -0,0 +1,132 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "e_acsl_mmodel_api.h"
+#include "e_acsl_mmodel.h"
+#include "stdio.h"
+
+struct _node {
+ struct _block * value;
+ struct _node * next;
+};
+
+struct _node * __list = NULL;
+
+
+void __remove_element(struct _block* ptr) {
+ struct _node * tmp1 = __list, * tmp2;
+ if(tmp1 == NULL) return;
+ tmp2 = tmp1->next;
+
+ /* first element */
+ if(tmp1->value->ptr == ptr->ptr) {
+ __list = tmp1->next;
+ free(tmp1);
+ }
+
+ for(; tmp2 != NULL && tmp2->value->ptr < ptr->ptr;) {
+ tmp1 = tmp2;
+ tmp2 = tmp2->next;
+ }
+ if(tmp2 == NULL) return;
+ if(tmp2->value->ptr == ptr->ptr) {
+ tmp1->next = tmp2->next;
+ free(tmp2);
+ }
+}
+
+
+void __add_element(struct _block* ptr) {
+ struct _node * tmp1 = __list, * tmp2, * new;
+ new = malloc(sizeof(struct _node));
+ if(new == NULL) return;
+ new->value = ptr;
+ new->next = NULL;
+
+ if(__list == NULL) {
+ __list = new;
+ return;
+ }
+ if(__list->value->ptr >= ptr->ptr) {
+ new->next = __list;
+ __list = new;
+ return;
+ }
+ tmp2 = tmp1->next;
+
+ for(; tmp2 != NULL && tmp2->value->ptr < ptr->ptr;) {
+ tmp1 = tmp2;
+ tmp2 = tmp2->next;
+ }
+
+ tmp1->next = new;
+ new->next = tmp2;
+}
+
+
+struct _block* __get_exact(void* ptr) {
+ struct _node * tmp = __list;
+ for(; tmp != NULL;) {
+ if(tmp->value->ptr == (size_t)ptr)
+ return tmp->value;
+ if(tmp->value->ptr > (size_t)ptr)
+ break;
+ tmp = tmp->next;
+ }
+ return NULL;
+}
+
+
+struct _block* __get_cont(void* ptr) {
+ struct _node * tmp = __list;
+ for(; tmp != NULL; tmp = tmp->next) {
+ if(tmp->value->ptr <= (size_t)ptr
+ && (size_t)ptr < tmp->value->ptr + tmp->value->size)
+ return tmp->value;
+ else if(tmp->value->ptr > (size_t)ptr)
+ break;
+ }
+ return NULL;
+}
+
+
+void __clean_struct() {
+ struct _node * next;
+ for(; __list != NULL ;) {
+ __clean_block(__list->value);
+ next = __list->next;
+ free(__list);
+ __list = next;
+ }
+}
+
+
+void __debug_struct() {
+ struct _node * tmp = __list;
+ printf("\t\t\t------------DEBUG\n");
+ for(; tmp != NULL; tmp = tmp->next) {
+ printf("\t\t\t");
+ __print_block(tmp->value);
+ }
+ printf("\t\t\t-----------------\n");
+}
+
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
new file mode 100644
index 0000000000000000000000000000000000000000..8b485fccd7a79d3272c11bf45db54f9983885cf9
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_splay_tree.c
@@ -0,0 +1,196 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "e_acsl_mmodel_api.h"
+#include "e_acsl_mmodel.h"
+#include "stdio.h"
+
+struct _node {
+ struct _block * value;
+ struct _node * left, * right, * parent;
+};
+
+struct _node * __root = NULL;
+
+void left_rotate(struct _node * x) {
+ struct _node* y = x->right;
+ x->right = y->left;
+ if( y->left ) y->left->parent = x;
+ y->parent = x->parent;
+ if( !x->parent ) __root = y;
+ else if( x == x->parent->left ) x->parent->left = y;
+ else x->parent->right = y;
+ y->left = x;
+ x->parent = y;
+}
+
+void right_rotate(struct _node *x ) {
+ struct _node *y = x->left;
+ x->left = y->right;
+ if( y->right ) y->right->parent = x;
+ y->parent = x->parent;
+ if( !x->parent ) __root = y;
+ else if( x == x->parent->left ) x->parent->left = y;
+ else x->parent->right = y;
+ y->right = x;
+ x->parent = y;
+}
+
+void splay(struct _node *x ) {
+ while( x->parent ) {
+ if( !x->parent->parent ) {
+ if( x->parent->left == x ) right_rotate( x->parent );
+ else left_rotate( x->parent );
+ }
+ else if( x->parent->left == x && x->parent->parent->left == x->parent ) {
+ right_rotate( x->parent->parent );
+ right_rotate( x->parent );
+ }
+ else if( x->parent->right == x && x->parent->parent->right == x->parent ) {
+ left_rotate( x->parent->parent );
+ left_rotate( x->parent );
+ }
+ else if( x->parent->left == x && x->parent->parent->right == x->parent ) {
+ right_rotate( x->parent );
+ left_rotate( x->parent );
+ }
+ else {
+ left_rotate( x->parent );
+ right_rotate( x->parent );
+ }
+ }
+}
+
+struct _node* subtree_minimum(struct _node *u ) {
+ while( u->left ) u = u->left;
+ return u;
+}
+
+struct _node* subtree_maximum(struct _node *u ) {
+ while( u->right ) u = u->right;
+ return u;
+}
+
+void replace(struct _node *u, struct _node *v ) {
+ if( !u->parent ) __root = v;
+ else if( u == u->parent->left ) u->parent->left = v;
+ else u->parent->right = v;
+ if( v ) v->parent = u->parent;
+}
+
+void __remove_element(struct _block* ptr) {
+ struct _node * z = __root;
+ while(z != NULL) {
+ if(z->value->ptr > ptr->ptr) z = z->left;
+ else if(z->value->ptr < ptr->ptr) z = z->right;
+ else break;
+ }
+ if( !z ) return;
+ splay( z );
+
+ if( !z->left ) replace( z, z->right );
+ else if( !z->right ) replace( z, z->left );
+ else {
+ struct _node *y = subtree_minimum( z->right );
+ if( y->parent != z ) {
+ replace( y, y->right );
+ y->right = z->right;
+ y->right->parent = y;
+ }
+ replace( z, y );
+ y->left = z->left;
+ y->left->parent = y;
+ }
+}
+
+
+void __add_element(struct _block* ptr) {
+ struct _node *z = __root, *p = NULL;
+ while( z ) {
+ p = z;
+ if(z->value->ptr > ptr->ptr) z = z->left;
+ else if(z->value->ptr < ptr->ptr) z = z->right;
+ else return;
+ }
+ z = malloc(sizeof(struct _node));
+ z->left = z->right = NULL;
+ z->value = ptr;
+ z->parent = p;
+ if( !p ) __root = z;
+ else if(p->value->ptr < z->value->ptr) p->right = z;
+ else p->left = z;
+ splay( z );
+}
+
+
+struct _block* __get_exact(void* ptr) {
+ struct _node * tmp = __root;
+ while(tmp != NULL) {
+ if(tmp->value->ptr > (size_t)ptr) tmp = tmp->left;
+ else if(tmp->value->ptr < (size_t)ptr) tmp = tmp->right;
+ else return tmp->value;
+ }
+ return NULL;
+}
+
+
+struct _block* _get_cont_rec(struct _node * node, void* ptr) {
+ if(node == NULL) return NULL;
+ else if(node->value->ptr > (size_t)ptr) return _get_cont_rec(node->left, ptr);
+ else if(node->value->ptr+node->value->size > (size_t)ptr) return node->value;
+ else return _get_cont_rec(node->right, ptr);
+}
+
+
+struct _block* __get_cont(void* ptr) {
+ return _get_cont_rec(__root, ptr);
+}
+
+
+void __clean_rec(struct _node * ptr) {
+ if(ptr == NULL) return;
+ __clean_block(ptr->value);
+ __clean_rec(ptr->left);
+ __clean_rec(ptr->right);
+ free(ptr);
+ ptr = NULL;
+}
+
+void __clean_struct() {
+ __clean_rec(__root);
+}
+
+
+void __debug_rec(struct _node * ptr) {
+ if(ptr == NULL) return;
+ __debug_rec(ptr->left);
+ printf("\t\t\t");
+ __print_block(ptr->value);
+ __debug_rec(ptr->right);
+}
+
+void __debug_struct() {
+ printf("\t\t\t------------DEBUG\n");
+ __debug_rec(__root);
+ printf("\t\t\t-----------------\n");
+}
+
diff --git a/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
new file mode 100644
index 0000000000000000000000000000000000000000..6c66e508520f1757f43b4feb45796b2c39ce7751
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/memory_model/e_acsl_tree.c
@@ -0,0 +1,151 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2013 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "e_acsl_mmodel_api.h"
+#include "e_acsl_mmodel.h"
+#include "stdio.h"
+
+struct _node {
+ struct _block * value;
+ struct _node * left, * right;
+};
+
+struct _node * __root = NULL;
+
+void __remove_element(struct _block* ptr) {
+ struct _node * tmp = __root, * father = NULL;
+
+ while(tmp != NULL) {
+ if(tmp->value->ptr > ptr->ptr) { father = tmp; tmp = tmp->left; }
+ else if(tmp->value->ptr < ptr->ptr) { father = tmp; tmp = tmp->right; }
+ else break;
+ }
+ if(tmp == NULL) return;
+
+ if(tmp->left == NULL) {
+ if(__root == tmp) __root = tmp->right;
+ else {
+ if(father->left == tmp) father->left = tmp->right;
+ else father->right = tmp->right;
+ }
+ free(tmp);
+ }
+ else if(tmp->right == NULL) {
+ if(__root == tmp) __root = tmp->left;
+ else {
+ if(father->left == tmp) father->left = tmp->left;
+ else father->right = tmp->left;
+ }
+ free(tmp);
+ }
+ else { /* two children */
+ struct _node * cursor = tmp->right;
+ father = tmp;
+ while(cursor->left != NULL) { father = cursor; cursor = cursor->left; }
+ tmp->value = cursor->value;
+ if(father->left == cursor) father->left = cursor->right;
+ else father->right = cursor->right;
+ free(cursor);
+ }
+}
+
+
+void __add_element(struct _block* ptr) {
+ enum {LEFT, RIGHT} pos;
+ struct _node * new, * tmp = __root, * father = NULL;
+ new = malloc(sizeof(struct _node));
+ if(new == NULL) return;
+ new->value = ptr;
+ new->left = new->right = NULL;
+
+ if(__root == NULL) {
+ __root = new;
+ return;
+ }
+ while(tmp != NULL) {
+ father = tmp;
+ if(tmp->value->ptr >= ptr->ptr) {
+ tmp = tmp->left;
+ pos = LEFT;
+ }
+ else {
+ tmp = tmp->right;
+ pos = RIGHT;
+ }
+ }
+ if(pos == LEFT) father->left = new;
+ else father->right = new;
+}
+
+
+struct _block* __get_exact(void* ptr) {
+ struct _node * tmp = __root;
+ while(tmp != NULL) {
+ if(tmp->value->ptr > (size_t)ptr) tmp = tmp->left;
+ else if(tmp->value->ptr < (size_t)ptr) tmp = tmp->right;
+ else return tmp->value;
+ }
+ return NULL;
+}
+
+
+struct _block* _get_cont_rec(struct _node * node, void* ptr) {
+ if(node == NULL) return NULL;
+ else if(node->value->ptr > (size_t)ptr) return _get_cont_rec(node->left, ptr);
+ else if(node->value->ptr+node->value->size > (size_t)ptr) return node->value;
+ else return _get_cont_rec(node->right, ptr);
+}
+
+
+struct _block* __get_cont(void* ptr) {
+ return _get_cont_rec(__root, ptr);
+}
+
+
+void __clean_rec(struct _node * ptr) {
+ if(ptr == NULL) return;
+ __clean_block(ptr->value);
+ __clean_rec(ptr->left);
+ __clean_rec(ptr->right);
+ free(ptr);
+ ptr = NULL;
+}
+
+void __clean_struct() {
+ __clean_rec(__root);
+}
+
+
+void __debug_rec(struct _node * ptr) {
+ if(ptr == NULL) return;
+ __debug_rec(ptr->left);
+ printf("\t\t\t");
+ __print_block(ptr->value);
+ __debug_rec(ptr->right);
+}
+
+void __debug_struct() {
+ printf("\t\t\t------------DEBUG\n");
+ __debug_rec(__root);
+ printf("\t\t\t-----------------\n");
+}
+