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 760054a5f81f41fb83b706e126045cbb259c6ea5..9eebfaf1efc3b86358c55b47d57bbf89ea766db6 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 @@ -324,7 +324,9 @@ static bt_block * bt_lookup (void * ptr) { @*/ 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; + 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 @@ -334,10 +336,12 @@ static bt_block * bt_lookup (void * ptr) { 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; } @@ -346,14 +350,16 @@ static bt_block * bt_lookup (void * ptr) { or NULL if such a block does not exist */ static bt_block * bt_find (void * ptr) { bt_node * tmp = bt_root; - if(bt_root == NULL || ptr == NULL) return NULL; + if(bt_root == NULL || ptr == NULL) + return NULL; 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) return NULL; + 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) */ else if((size_t)ptr < tmp->leaf->size + tmp->addr 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 1f74cf52e0aed16786ac846432189ce47c1c6ea6..6d02033d33fe1f1fb7a97489c7bd70ac050370ac 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 @@ -59,13 +59,15 @@ static void bt_remove(bt_block *b); /*! \brief Add a block to the structure */ 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. */ +/*! \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. */ +/*! \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 */