diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
index 989a640c1e938df2ff8644daff47db829b32da94..7f3d799a5653c5f96f1b2d490869d534a460cd4a 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h
@@ -98,14 +98,8 @@ static const int Tneq[] =
#endif
-static struct bittree {
- _Bool is_leaf;
- size_t addr, mask;
- struct bittree * left, * right, * father;
- struct _block * leaf;
-} * __root = NULL;
-
-/*unsigned cpt_mask = 0;*/
+/*! \brief Root node of the bitree */
+bt_node * bt_root = NULL;
/* common prefix of two addresses */
/*@ assigns \nothing;
@@ -140,32 +134,32 @@ static size_t mask(size_t a, size_t b) {
//@ assert -WORDBITS <= i <= 0;
ret = Tmasks[-i];
- assert ((a & ret) == (b & ret));
+ DASSERT ((a & ret) == (b & ret));
return ret;
}
-/* called from remove_element */
+/* called from bt_remove */
/* the block we are looking for has to be in the tree */
/*@ requires \valid(ptr);
- @ requires \valid(__root);
+ @ requires \valid(bt_root);
@ assigns \nothing;
@ ensures \valid(\result);
@ ensures \result->leaf == ptr;
@*/
-static struct bittree * __get_leaf_from_block (struct _block * ptr) {
- struct bittree * curr = __root;
- assert(__root != NULL);
- assert(ptr != NULL);
+static bt_node * bt_get_leaf_from_block (bt_block * ptr) {
+ bt_node * curr = bt_root;
+ DASSERT(bt_root != NULL);
+ DASSERT(ptr != NULL);
/*@ loop assigns curr;
@*/
while(!curr->is_leaf) {
// the prefix is consistent
- assert((curr->addr & curr->mask) == (ptr->ptr & curr->mask));
- // two sons
- assert(curr->left != NULL && curr->right != NULL);
- // the prefix of one son is consistent
+ DASSERT((curr->addr & curr->mask) == (ptr->ptr & curr->mask));
+ // two children
+ DASSERT(curr->left != NULL && curr->right != NULL);
+ // the prefix of one child is consistent
if((curr->right->addr & curr->right->mask)
== (ptr->ptr & curr->right->mask))
curr = curr->right;
@@ -175,8 +169,8 @@ static struct bittree * __get_leaf_from_block (struct _block * ptr) {
else
assert(0);
}
- assert(curr->is_leaf);
- assert(curr->leaf == ptr);
+ DASSERT(curr->is_leaf);
+ DASSERT(curr->leaf == ptr);
return curr;
}
@@ -185,36 +179,36 @@ static struct bittree * __get_leaf_from_block (struct _block * ptr) {
/* the block we are looking for has to be in the tree */
/*@ requires \valid(ptr);
@*/
-static void remove_element (struct _block * ptr) {
- struct bittree * leaf_to_delete = __get_leaf_from_block (ptr);
- assert(leaf_to_delete->leaf == ptr);
+static void bt_remove (bt_block * ptr) {
+ bt_node * leaf_to_delete = bt_get_leaf_from_block (ptr);
+ DASSERT(leaf_to_delete->leaf == ptr);
- if(leaf_to_delete->father == NULL)
+ if(leaf_to_delete->parent == NULL)
// the leaf is the root
- __root = NULL;
+ bt_root = NULL;
else {
- struct bittree * brother, * father;
- father = leaf_to_delete->father;
- brother = (leaf_to_delete == father->left) ? father->right : father->left;
- assert(brother != NULL);
- // copying all brother's fields into the father's
- father->is_leaf = brother->is_leaf;
- father->addr = brother->addr;
- father->mask = brother->mask;
- father->left = brother->left;
- father->right = brother->right;
- father->leaf = brother->leaf;
- if(!brother->is_leaf) {
- brother->left->father = father;
- brother->right->father = father;
+ bt_node * sibling, * parent;
+ parent = leaf_to_delete->parent;
+ sibling = (leaf_to_delete == parent->left) ? parent->right : parent->left;
+ DASSERT(sibling != NULL);
+ // copying all sibling's fields into the parent's
+ parent->is_leaf = sibling->is_leaf;
+ parent->addr = sibling->addr;
+ parent->mask = sibling->mask;
+ parent->left = sibling->left;
+ parent->right = sibling->right;
+ parent->leaf = sibling->leaf;
+ if(!sibling->is_leaf) {
+ sibling->left->parent = parent;
+ sibling->right->parent = parent;
}
- native_free(brother);
+ native_free(sibling);
/* necessary ? -- begin */
- if(father->father != NULL) {
- father->father->mask = mask(father->father->left->addr
- & father->father->left->mask,
- father->father->right->addr
- & father->father->right->mask);
+ if(parent->parent != NULL) {
+ parent->parent->mask = mask(parent->parent->left->addr
+ & parent->parent->left->mask,
+ parent->parent->right->addr
+ & parent->parent->right->mask);
}
/* necessary ? -- end */
}
@@ -222,23 +216,23 @@ static void remove_element (struct _block * ptr) {
}
-/* called from add_element */
-/* the returned node will be the brother of the soon to be added node */
+/* called from bt_insert */
+/* the returned node will be the sibling of the soon to be added node */
/*@ requires \valid(ptr);
- @ requires \valid(__root);
+ @ requires \valid(bt_root);
@ assigns \nothing;
@ ensures \valid(\result);
@*/
-static struct bittree * __most_similar_node (struct _block * ptr) {
- struct bittree * curr = __root;
+static bt_node * bt_most_similar_node (bt_block * ptr) {
+ bt_node * curr = bt_root;
size_t left_prefix, right_prefix;
- assert(ptr != NULL);
- assert(__root != NULL);
+ DASSERT(ptr != NULL);
+ DASSERT(bt_root != NULL);
while(1) {
if(curr->is_leaf)
return curr;
- assert(curr->left != NULL && curr->right != NULL);
+ DASSERT(curr->left != NULL && curr->right != NULL);
left_prefix = mask(curr->left->addr & curr->left->mask, ptr->ptr);
right_prefix = mask(curr->right->addr & curr->right->mask, ptr->ptr);
if(left_prefix > right_prefix)
@@ -253,66 +247,65 @@ static struct bittree * __most_similar_node (struct _block * ptr) {
/* add a block in the structure */
/*@ requires \valid(ptr);
@*/
-static void add_element (struct _block * ptr) {
- struct bittree * new_leaf;
- assert(ptr != NULL);
+static void bt_insert (bt_block * ptr) {
+ bt_node * new_leaf;
+ DASSERT(ptr != NULL);
- new_leaf = native_malloc(sizeof(struct bittree));
- assert(new_leaf != NULL);
+ new_leaf = native_malloc(sizeof(bt_node));
+ DASSERT(new_leaf != NULL);
new_leaf->is_leaf = true;
new_leaf->addr = ptr->ptr;
new_leaf->mask = Tmasks[WORDBITS]; /* ~0ul */
new_leaf->left = NULL;
new_leaf->right = NULL;
- new_leaf->father = NULL;
+ new_leaf->parent = NULL;
new_leaf->leaf = ptr;
- if(__root == NULL)
- __root = new_leaf;
+ if(bt_root == NULL)
+ bt_root = new_leaf;
else {
- struct bittree * brother = __most_similar_node (ptr), * father, * aux;
-
- assert(brother != NULL);
- father = native_malloc(sizeof(struct bittree));
- assert(father != NULL);
- father->is_leaf = false;
- father->addr = brother->addr & new_leaf->addr;
- /*father->mask = mask(brother->addr & brother->mask, ptr->ptr);*/
- father->leaf = NULL;
- if(new_leaf->addr <= brother->addr) {
- father->left = new_leaf;
- father->right = brother;
+ bt_node * sibling = bt_most_similar_node (ptr), * parent, * aux;
+
+ DASSERT(sibling != NULL);
+ parent = native_malloc(sizeof(bt_node));
+ DASSERT(parent != NULL);
+ parent->is_leaf = false;
+ parent->addr = sibling->addr & new_leaf->addr;
+ /*parent->mask = mask(sibling->addr & sibling->mask, ptr->ptr);*/
+ parent->leaf = NULL;
+ if(new_leaf->addr <= sibling->addr) {
+ parent->left = new_leaf;
+ parent->right = sibling;
} else {
- father->left = brother;
- father->right = new_leaf;
+ parent->left = sibling;
+ parent->right = new_leaf;
}
- new_leaf->father = father;
+ new_leaf->parent = parent;
- if(brother == __root) {
- father->father = NULL;
- father->mask = mask(brother->addr & brother->mask, ptr->ptr);
- __root = father;
- }
- else {
- if (brother->father->left == brother)
- brother->father->left = father;
+ if(sibling == bt_root) {
+ parent->parent = NULL;
+ parent->mask = mask(sibling->addr & sibling->mask, ptr->ptr);
+ bt_root = parent;
+ } else {
+ if (sibling->parent->left == sibling)
+ sibling->parent->left = parent;
else
- brother->father->right = father;
- father->father = brother->father;
+ sibling->parent->right = parent;
+ parent->parent = sibling->parent;
/* necessary ? -- begin */
- aux = father;
+ aux = parent;
aux->mask = mask(aux->left->addr & aux->left->mask,
aux->right->addr & aux->right->mask);
/* necessary ? -- end */
}
- brother->father = father;
- if(!brother->is_leaf)
- brother->mask = mask(brother->left->addr & brother->left->mask,
- brother->right->addr & brother->right->mask);
+ sibling->parent = parent;
+ if(!sibling->is_leaf)
+ sibling->mask = mask(sibling->left->addr & sibling->left->mask,
+ sibling->right->addr & sibling->right->mask);
- assert((father->left == brother && father->right == new_leaf)
- || (father->left == new_leaf && father->right == brother));
+ DASSERT((parent->left == sibling && parent->right == new_leaf)
+ || (parent->left == new_leaf && parent->right == sibling));
}
}
@@ -322,87 +315,79 @@ static void add_element (struct _block * ptr) {
@ ensures \valid(\result);
@ ensures \result == \null || \result->ptr == (size_t)ptr;
@*/
-static struct _block * get_exact (void * ptr) {
- struct bittree * tmp = __root;
- assert(__root != NULL);
- assert(ptr != NULL);
+static bt_block * bt_lookup (void * ptr) {
+ bt_node * tmp = bt_root;
+ DASSERT(bt_root != NULL);
+ DASSERT(ptr != NULL);
/*@ loop assigns tmp;
@*/
while(!tmp->is_leaf) {
// 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
+ if((tmp->addr & tmp->mask) != ((size_t)ptr & tmp->mask))
+ return NULL;
+
+ // two children
+ DASSERT(tmp->left != NULL && tmp->right != NULL);
+ // the prefix of one child is consistent
if((tmp->right->addr & tmp->right->mask)
== ((size_t)ptr & tmp->right->mask))
tmp = tmp->right;
else if((tmp->left->addr & tmp->left->mask)
== ((size_t)ptr & tmp->left->mask))
tmp = tmp->left;
- else return NULL;
+ else
+ return NULL;
}
- if(tmp->leaf->ptr != (size_t)ptr) return NULL;
+ if(tmp->leaf->ptr != (size_t)ptr)
+ return NULL;
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 */
-static struct _block * get_cont (void * ptr) {
- struct bittree * tmp = __root;
- if(__root == NULL || ptr == NULL) return NULL;
+static bt_block * bt_find (void * ptr) {
+ bt_node * tmp = bt_root;
+ if(bt_root == NULL || ptr == NULL)
+ return NULL;
- struct bittree * t [WORDBITS];
- short ind = -1;
+ bt_node * other_choice = NULL;
while(1) {
if(tmp->is_leaf) {
/* tmp cannot contain ptr because its begin addr is higher */
- if(tmp->addr > (size_t)ptr) {
- if(ind == -1)
- return NULL;
- else {
- tmp = t[ind];
- ind--;
- continue;
- }
- }
+ if(tmp->addr > (size_t)ptr)
+ return NULL;
+
/* tmp->addr <= ptr, tmp may contain ptr
- ptr is contained if tmp is large enough (begin addr + size) */
+ ptr is contained if tmp is large enough (begin addr + size) */
else if((size_t)ptr < tmp->leaf->size + tmp->addr
|| (tmp->leaf->size == 0 && (size_t)ptr == tmp->leaf->ptr))
- return tmp->leaf;
+ return tmp->leaf;
/* tmp->addr <= ptr, but tmp->addr is not large enough */
- else if (ind == -1)
- return NULL;
- else {
- tmp = t[ind];
- ind--;
- continue;
- }
+ else
+ return NULL;
}
- assert(tmp->left != NULL && tmp->right != NULL);
+ DASSERT(tmp->left != NULL && tmp->right != NULL);
/* the right child has the highest address, so we test it first */
if(((size_t)tmp->right->addr & tmp->right->mask)
<= ((size_t)ptr & tmp->right->mask)) {
- ind++;
- t[ind] = tmp->left;
+ other_choice = tmp->left;
tmp = tmp->right;
}
else if(((size_t)tmp->left->addr & tmp->left->mask)
<= ((size_t)ptr & tmp->left->mask))
tmp = tmp->left;
else {
- if(ind == -1)
- return NULL;
+ if(other_choice == NULL)
+ return NULL;
else {
- tmp = t[ind];
- ind--;
+ tmp = other_choice;
+ other_choice = NULL;
}
}
}
@@ -412,55 +397,53 @@ static struct _block * get_cont (void * ptr) {
/* CLEAN */
/*******************/
/* erase information about initialization of a block */
-static void clean_init (struct _block * ptr) {
+static void bt_clean_block_init (bt_block * ptr) {
if(ptr->init_ptr != NULL) {
native_free(ptr->init_ptr);
ptr->init_ptr = NULL;
}
- ptr->init_cpt = 0;
+ ptr->init_bytes = 0;
}
/* erase all information about a block */
-static void clean_block (struct _block * ptr) {
+static void bt_clean_block (bt_block * ptr) {
if(ptr) {
- clean_init(ptr);
+ bt_clean_block_init(ptr);
native_free(ptr);
}
}
-/* called from clean_struct */
+/* called from bt_clean */
/* recursively erase the content of the structure */
-static void __clean_rec (struct bittree * ptr) {
+static void bt_clean_rec (bt_node * ptr) {
if(ptr == NULL) return;
else if(ptr->is_leaf) {
- clean_block(ptr->leaf);
+ bt_clean_block(ptr->leaf);
ptr->leaf = NULL;
}
else {
- __clean_rec(ptr->left);
- __clean_rec(ptr->right);
+ bt_clean_rec(ptr->left);
+ bt_clean_rec(ptr->right);
ptr->left = ptr->right = NULL;
}
native_free(ptr);
}
/* erase the content of the structure */
-static void clean_struct () {
- __clean_rec(__root);
- __root = NULL;
+static void bt_clean () {
+ bt_clean_rec(bt_root);
+ bt_root = NULL;
}
/*********************/
/* DEBUG */
/*********************/
-
#ifdef E_ACSL_DEBUG
-
-static void print_block(struct _block * ptr) {
+static void bt_print_block(bt_block * ptr) {
if (ptr != NULL) {
DLOG("%a; %lu Bytes; %slitteral; [init] : %d ",
(char*)ptr->ptr, ptr->size,
- ptr->is_readonly ? "" : "not ", ptr->init_cpt);
+ ptr->is_readonly ? "" : "not ", ptr->init_bytes);
if(ptr->init_ptr != NULL) {
unsigned i;
for(i = 0; i < ptr->size/8; i++)
@@ -470,28 +453,24 @@ static void print_block(struct _block * ptr) {
}
}
-/* recursively print the content of the structure starting from a given node */
-/*@ assigns \nothing; */
-static void print_bittree_node(struct bittree * ptr, int depth) {
+static void bt_print_node(bt_node * ptr, int depth) {
int i;
if(ptr == NULL)
return;
for(i = 0; i < depth; i++)
DLOG(" ");
if(ptr->is_leaf)
- print_block(ptr->leaf);
+ bt_print_block(ptr->leaf);
else {
DLOG("%p -- %p\n", (void*)ptr->mask, (void*)ptr->addr);
- print_bittree_node(ptr->left, depth+1);
- print_bittree_node(ptr->right, depth+1);
+ bt_print_node(ptr->left, depth+1);
+ bt_print_node(ptr->right, depth+1);
}
}
-/* print the contents of the entire bittree */
-/*@ assigns \nothing; */
-static void print_bittree() {
+static void bt_print() {
DLOG("------------DEBUG\n");
- print_bittree_node(__root, 0);
+ bt_print_node(bt_root, 0);
DLOG("-----------------\n");
}
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
index 1297ccf38b8eade87fefe3fffbc8ae7886af5b35..5f32ca605431b54c86ca074f0eb03e52c5b273ab 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h
@@ -32,39 +32,65 @@
#include "stdbool.h"
/*! \brief Structure representing an allocated memory block */
-struct _block {
+struct bt_block {
size_t ptr; //!< Base address
size_t size; //!< Block length (in bytes)
unsigned char * init_ptr; //!< Per-bit initialization
- size_t init_cpt; //!< Number of initialized bytes
+ size_t init_bytes; //!< Number of initialized bytes within a block
_Bool is_readonly; //!< True if a block is marked read-only
_Bool freeable; //!< True if a block can be de-allocated using `free`
};
+typedef struct bt_block bt_block;
+
+/*! \brief Structure representing a bittree node */
+struct bt_node {
+ _Bool is_leaf;
+ size_t addr, mask;
+ struct bt_node * left, * right, * parent;
+ bt_block * leaf;
+};
+
+typedef struct bt_node bt_node;
+
/*! \brief Remove a block from the structure */
-static void remove_element(struct _block *b);
+static void bt_remove(bt_block *b);
/*! \brief Add a block to the structure */
-static void add_element(struct _block *b);
+static void bt_insert(bt_block *b);
-/*! \brief Return block B such that: `\base_addr(B->ptr) == ptr`.
-NB: The function assumes that such a block exists. */
-static struct _block * get_exact(void *ptr);
+/*! \brief Look-up a memory block by its base address
+ NB: The function assumes that such a block exists. */
+static bt_block * bt_lookup(void *ptr);
-/*! \brief Return block B such that:
- `\base_addr(B->ptr) <= ptr < (\base_addr(B->ptr) + size)`
- or NULL if such a block does not exist. */
-static struct _block * get_cont(void *ptr);
+/*! \brief Find a memory block containing a given memory address
+ *
+ * Return block B such that:
+ * `\base_addr(B->ptr) <= ptr < (\base_addr(B->ptr) + size)`
+ * or NULL if such a block does not exist. */
+static bt_block * bt_find(void *ptr);
/*! \brief Erase the contents of the structure */
-static void clean_struct(void);
-
-/*! \brief Print information about a given block */
-static void print_block(struct _block *b);
+static void bt_clean(void);
/*! \brief Erase information about a block's initialization */
-static void clean_init(struct _block *b);
+static void bt_clean_block_init(bt_block *b);
/*! \brief Erase all information about a given block */
-static void clean_block(struct _block *b);
+static void bt_clean_block(bt_block *b);
+
+#ifdef E_ACSL_DEBUG
+/*! \brief Print information about a given block */
+static void bt_print_block(bt_block *b);
+
+/*! \brief Recursively print the contents of the bittree starting from a
+ * given node */
+/*@ assigns \nothing; */
+static void bt_print_node(bt_node * ptr, int depth);
+
+/*! \brief Print the contents of the entire bittree */
+/*@ assigns \nothing; */
+static void bt_print();
+#endif
+
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
index 45bbbc15ff54129b788b97cdc25f3ea5b87157b2..ca41bd5182e2d1f98a78f4dabb1999204ff46de3 100644
--- a/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
@@ -64,29 +64,29 @@ size_t __get_memory_size(void) {
/**************************/
/* store the block of size bytes starting at ptr, the new block is returned.
- * Warning: the return type is implicitly (struct _block*). */
+ * Warning: the return type is implicitly (bt_block*). */
void* __store_block(void* ptr, size_t size) {
- struct _block * tmp;
+ bt_block * tmp;
DASSERT(ptr != NULL);
- tmp = native_malloc(sizeof(struct _block));
+ tmp = native_malloc(sizeof(bt_block));
DASSERT(tmp != NULL);
tmp->ptr = (size_t)ptr;
tmp->size = size;
tmp->init_ptr = NULL;
- tmp->init_cpt = 0;
+ tmp->init_bytes = 0;
tmp->is_readonly = false;
tmp->freeable = false;
- add_element(tmp);
+ bt_insert(tmp);
return tmp;
}
/* remove the block starting at ptr */
void __delete_block(void* ptr) {
DASSERT(ptr != NULL);
- struct _block * tmp = get_exact(ptr);
+ bt_block * tmp = bt_lookup(ptr);
DASSERT(tmp != NULL);
- clean_init(tmp);
- remove_element(tmp);
+ bt_clean_block_init(tmp);
+ bt_remove(tmp);
native_free(tmp);
}
@@ -94,7 +94,7 @@ void __delete_block(void* ptr) {
* for further information, see malloc */
void* __malloc(size_t size) {
void * tmp;
- struct _block * new_block;
+ bt_block * new_block;
if(size <= 0)
return NULL;
tmp = native_malloc(size);
@@ -110,23 +110,23 @@ void* __malloc(size_t size) {
/* free the block starting at ptr,
* for further information, see free */
void __free(void* ptr) {
- struct _block * tmp;
+ bt_block * tmp;
if(ptr == NULL)
return;
- tmp = get_exact(ptr);
+ tmp = bt_lookup(ptr);
DASSERT(tmp != NULL);
native_free(ptr);
- clean_init(tmp);
+ bt_clean_block_init(tmp);
__heap_size -= tmp->size;
- remove_element(tmp);
+ bt_remove(tmp);
native_free(tmp);
}
int __freeable(void* ptr) {
- struct _block * tmp;
+ bt_block * tmp;
if(ptr == NULL)
return false;
- tmp = get_exact(ptr);
+ tmp = bt_lookup(ptr);
if(tmp == NULL)
return false;
return tmp->freeable;
@@ -135,7 +135,7 @@ int __freeable(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;
+ bt_block * tmp;
void * new_ptr;
/* ptr is NULL - malloc */
if(ptr == NULL)
@@ -145,7 +145,7 @@ void* __realloc(void* ptr, size_t size) {
__free(ptr);
return NULL;
}
- tmp = get_exact(ptr);
+ tmp = bt_lookup(ptr);
DASSERT(tmp != NULL);
new_ptr = native_realloc((void*)tmp->ptr, size);
if(new_ptr == NULL)
@@ -153,18 +153,18 @@ void* __realloc(void* ptr, size_t size) {
__heap_size -= tmp->size;
/* realloc changes start address -- re-enter the element */
if (tmp->ptr != (size_t)new_ptr) {
- remove_element(tmp);
+ bt_remove(tmp);
tmp->ptr = (size_t)new_ptr;
- add_element(tmp);
+ bt_insert(tmp);
}
/* uninitialized, do nothing */
- if(tmp->init_cpt == 0) ;
+ if(tmp->init_bytes == 0) ;
/* already fully initialized block */
- else if (tmp->init_cpt == tmp->size) {
+ else if (tmp->init_bytes == tmp->size) {
/* realloc smaller block */
if(size <= tmp->size)
/* adjust new size, allocation not necessary */
- tmp->init_cpt = size;
+ tmp->init_bytes = size;
/* realloc bigger larger block */
else {
/* size of tmp->init_ptr in the new block */
@@ -185,10 +185,10 @@ void* __realloc(void* ptr, size_t size) {
tmp->init_ptr = native_realloc(tmp->init_ptr, nb);
for(i = nb_old; i < nb; i++)
tmp->init_ptr[i] = 0;
- tmp->init_cpt = 0;
+ tmp->init_bytes = 0;
for(i = 0; i < nb; i++)
- tmp->init_cpt += nbr_bits_to_1[tmp->init_ptr[i]];
- if(tmp->init_cpt == size || tmp->init_cpt == 0) {
+ tmp->init_bytes += nbr_bits_to_1[tmp->init_ptr[i]];
+ if(tmp->init_bytes == size || tmp->init_bytes == 0) {
native_free(tmp->init_ptr);
tmp->init_ptr = NULL;
}
@@ -205,7 +205,7 @@ void* __realloc(void* ptr, size_t size) {
void* __calloc(size_t nbr_block, size_t size_block) {
void * tmp;
size_t size = nbr_block * size_block;
- struct _block * new_block;
+ bt_block * new_block;
if(size <= 0)
return NULL;
tmp = native_calloc(nbr_block, size_block);
@@ -216,7 +216,7 @@ void* __calloc(size_t nbr_block, size_t size_block) {
DASSERT(new_block != NULL && (void*)new_block->ptr != NULL);
/* Mark allocated block as freeable and initialized */
new_block->freeable = true;
- new_block->init_cpt = size;
+ new_block->init_bytes = size;
return (void*)new_block->ptr;
}
@@ -226,20 +226,20 @@ void* __calloc(size_t nbr_block, size_t size_block) {
/* mark the size bytes of ptr as initialized */
void __initialize (void * ptr, size_t size) {
- struct _block * tmp;
+ bt_block * tmp;
if(!ptr)
return;
- tmp = get_cont(ptr);
+ tmp = bt_find(ptr);
if(tmp == NULL)
return;
/* already fully initialized, do nothing */
- if(tmp->init_cpt == tmp->size)
+ if(tmp->init_bytes == tmp->size)
return;
/* fully uninitialized */
- if(tmp->init_cpt == 0) {
+ if(tmp->init_bytes == 0) {
int nb = needed_bytes(tmp->size);
tmp->init_ptr = native_malloc(nb);
memset(tmp->init_ptr, 0, nb);
@@ -263,12 +263,12 @@ void __initialize (void * ptr, size_t size) {
if (!checkbit(bit, tmp->init_ptr[byte])) { /* if bit is unset ... */
setbit(bit, tmp->init_ptr[byte]); /* ... set the bit ... */
- tmp->init_cpt++; /* ... and increment initialized bytes count */
+ tmp->init_bytes++; /* ... and increment initialized bytes count */
}
}
/* now fully initialized */
- if(tmp->init_cpt == tmp->size) {
+ if(tmp->init_bytes == tmp->size) {
native_free(tmp->init_ptr);
tmp->init_ptr = NULL;
}
@@ -276,11 +276,11 @@ void __initialize (void * ptr, size_t size) {
/* mark all bytes of ptr as initialized */
void __full_init (void * ptr) {
- struct _block * tmp;
+ bt_block * tmp;
if (ptr == NULL)
return;
- tmp = get_exact(ptr);
+ tmp = bt_lookup(ptr);
if (tmp == NULL)
return;
@@ -288,16 +288,15 @@ void __full_init (void * ptr) {
native_free(tmp->init_ptr);
tmp->init_ptr = NULL;
}
-
- tmp->init_cpt = tmp->size;
+ tmp->init_bytes = tmp->size;
}
/* mark a block as read-only */
void __readonly (void * ptr) {
- struct _block * tmp;
+ bt_block * tmp;
if (ptr == NULL)
return;
- tmp = get_exact(ptr);
+ tmp = bt_lookup(ptr);
if (tmp == NULL)
return;
tmp->is_readonly = true;
@@ -310,15 +309,15 @@ void __readonly (void * ptr) {
/* return whether the size bytes of ptr are initialized */
int __initialized (void * ptr, size_t size) {
unsigned i;
- struct _block * tmp = get_cont(ptr);
+ bt_block * tmp = bt_find(ptr);
if(tmp == NULL)
return false;
/* fully uninitialized */
- if(tmp->init_cpt == 0)
+ if(tmp->init_bytes == 0)
return false;
/* fully initialized */
- if(tmp->init_cpt == tmp->size)
+ if(tmp->init_bytes == tmp->size)
return true;
/* see implementation of function __initialize for details */
@@ -334,7 +333,7 @@ int __initialized (void * ptr, size_t size) {
/* return the length (in bytes) of the block containing ptr */
size_t __block_length(void* ptr) {
- struct _block * tmp = get_cont(ptr);
+ bt_block * tmp = bt_find(ptr);
/* Hard failure when un-allocated memory is used */
vassert(tmp != NULL, "\\block_length of unallocated memory", NULL);
return tmp->size;
@@ -342,10 +341,10 @@ size_t __block_length(void* ptr) {
/* return whether the size bytes of ptr are readable/writable */
int __valid(void* ptr, size_t size) {
- struct _block * tmp;
+ bt_block * tmp;
if(ptr == NULL)
return false;
- tmp = get_cont(ptr);
+ tmp = bt_find(ptr);
return (tmp == NULL) ?
false : ( tmp->size - ( (size_t)ptr - tmp->ptr ) >= size
&& !tmp->is_readonly);
@@ -353,24 +352,24 @@ int __valid(void* ptr, size_t size) {
/* return whether the size bytes of ptr are readable */
int __valid_read(void* ptr, size_t size) {
- struct _block * tmp;
+ bt_block * tmp;
if(ptr == NULL)
return false;
- tmp = get_cont(ptr);
+ tmp = bt_find(ptr);
return (tmp == NULL) ?
false : (tmp->size - ((size_t)ptr - tmp->ptr) >= size);
}
/* return the base address of the block containing ptr */
void* __base_addr(void* ptr) {
- struct _block * tmp = get_cont(ptr);
+ bt_block * tmp = bt_find(ptr);
vassert(tmp != NULL, "\\base_addr of unallocated memory", NULL);
return (void*)tmp->ptr;
}
/* return the offset of `ptr` within its block */
int __offset(void* ptr) {
- struct _block * tmp = get_cont(ptr);
+ bt_block * tmp = bt_find(ptr);
vassert(tmp != NULL, "\\offset of unallocated memory", NULL);
return ((size_t)ptr - tmp->ptr);
}
@@ -381,7 +380,7 @@ int __offset(void* ptr) {
/* erase the content of the abstract structure */
void __e_acsl_memory_clean() {
- clean_struct();
+ bt_clean();
}
/* add `argv` to the memory model */
@@ -407,14 +406,14 @@ void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
/* DEBUG */
/**********************/
#ifdef E_ACSL_DEBUG
-/*! \brief print the information about a block */
-void __e_acsl_print_block (struct _block * ptr) {
- print_block(ptr);
+/*! \brief print the information about a tracked block */
+void __e_acsl_print_block (bt_block * ptr) {
+ bt_print_block(ptr);
}
-/*! \brief print the content of the abstract structure */
+/*! \brief print the content of the bittree */
void __e_acsl_print_bittree() {
- print_bittree();
+ bt_print();
}
#endif
#endif