diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
index 7355645409e45f1e2dabb0dee62a01a47878c773..964a7c069e78d3f14afaf048af3403977e34960b 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
@@ -340,7 +340,6 @@ static struct _block * __get_exact (void * ptr) {
return tmp->leaf;
}
-
/* return the block B containing ptr, such as :
begin addr of B <= ptr < (begin addr + size) of B
or NULL if such a block does not exist */
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.c b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h
similarity index 84%
rename from src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.c
rename to src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h
index 445484e27cf89f4bf489520b4a45987116b7bfdc..6c86b89e421cab6278b9fc235f608758ae7ef2b2 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.c
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h
@@ -20,18 +20,22 @@
/* */
/**************************************************************************/
-#include "e_acsl_mmodel_api.h"
-#include "e_acsl_mmodel.h"
-#include "stdio.h"
+#ifndef E_ACSL_SPLAYTREE
+#define E_ACSL_SPLAYTREE
-struct _node {
+#include "e_acsl_syscall.h"
+#include "e_acsl_printf.h"
+#include "e_acsl_assert.h"
+#include "e_acsl_adt_api.h"
+
+static struct _node {
struct _block * value;
struct _node * left, * right, * parent;
};
-struct _node * __root = NULL;
+static struct _node * __root = NULL;
-void left_rotate(struct _node * x) {
+static void left_rotate(struct _node * x) {
struct _node* y = x->right;
x->right = y->left;
if( y->left ) y->left->parent = x;
@@ -43,7 +47,7 @@ void left_rotate(struct _node * x) {
x->parent = y;
}
-void right_rotate(struct _node *x ) {
+static void right_rotate(struct _node *x ) {
struct _node *y = x->left;
x->left = y->right;
if( y->right ) y->right->parent = x;
@@ -55,7 +59,7 @@ void right_rotate(struct _node *x ) {
x->parent = y;
}
-void splay(struct _node *x ) {
+static void splay(struct _node *x ) {
while( x->parent ) {
if( !x->parent->parent ) {
if( x->parent->left == x ) right_rotate( x->parent );
@@ -79,25 +83,25 @@ void splay(struct _node *x ) {
}
}
}
-
-struct _node* subtree_minimum(struct _node *u ) {
+
+static struct _node* subtree_minimum(struct _node *u ) {
while( u->left ) u = u->left;
return u;
}
-
-struct _node* subtree_maximum(struct _node *u ) {
+
+static struct _node* subtree_maximum(struct _node *u ) {
while( u->right ) u = u->right;
return u;
}
-void replace(struct _node *u, struct _node *v ) {
+static 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) {
+static void __remove_element(struct _block* ptr) {
struct _node * z = __root;
while(z != NULL) {
if(z->value->ptr > ptr->ptr) z = z->left;
@@ -122,8 +126,7 @@ void __remove_element(struct _block* ptr) {
}
}
-
-void __add_element(struct _block* ptr) {
+static void __add_element(struct _block* ptr) {
struct _node *z = __root, *p = NULL;
while( z ) {
p = z;
@@ -141,8 +144,7 @@ void __add_element(struct _block* ptr) {
splay( z );
}
-
-struct _block* __get_exact(void* ptr) {
+static struct _block* __get_exact(void* ptr) {
struct _node * tmp = __root;
while(tmp != NULL) {
if(tmp->value->ptr > (size_t)ptr) tmp = tmp->left;
@@ -152,8 +154,7 @@ struct _block* __get_exact(void* ptr) {
return NULL;
}
-
-struct _block* _get_cont_rec(struct _node * node, void* ptr) {
+static 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->size == 0 && node->value->ptr == (size_t)ptr)
@@ -162,13 +163,11 @@ struct _block* _get_cont_rec(struct _node * node, void* ptr) {
else return _get_cont_rec(node->right, ptr);
}
-
-struct _block* __get_cont(void* ptr) {
+static struct _block* __get_cont(void* ptr) {
return _get_cont_rec(__root, ptr);
}
-
-void __clean_rec(struct _node * ptr) {
+static void __clean_rec(struct _node * ptr) {
if(ptr == NULL) return;
__clean_block(ptr->value);
__clean_rec(ptr->left);
@@ -177,12 +176,11 @@ void __clean_rec(struct _node * ptr) {
ptr = NULL;
}
-void __clean_struct() {
+static void __clean_struct() {
__clean_rec(__root);
}
-
-void __debug_rec(struct _node * ptr) {
+static void __debug_rec(struct _node * ptr) {
if(ptr == NULL) return;
__debug_rec(ptr->left);
printf("\t\t\t");
@@ -190,9 +188,9 @@ void __debug_rec(struct _node * ptr) {
__debug_rec(ptr->right);
}
-void __debug_struct() {
+static void __debug_struct() {
printf("\t\t\t------------DEBUG\n");
__debug_rec(__root);
printf("\t\t\t-----------------\n");
}
-
+#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree_mmodel.c
new file mode 100644
index 0000000000000000000000000000000000000000..459f42e0d053867528d0b7005b05e6e673daf78b
--- /dev/null
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree_mmodel.c
@@ -0,0 +1,24 @@
+/**************************************************************************/
+/* */
+/* This file is part of the Frama-C's E-ACSL plug-in. */
+/* */
+/* Copyright (C) 2012-2016 */
+/* 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 license/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+#include "e_acsl_adt_mmodel.h"
+#include "e_acsl_splaytree.h"