Renamed the main structure representing a memory block in a bittree

src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree.h

@@ -102,7 +102,7 @@ static struct bittree {
   _Bool is_leaf;
   size_t addr,  mask;
   struct bittree * left, * right, * father;
-  struct _block * leaf;
+  bt_block * leaf;
 } * bt_root = NULL;
 
 /*unsigned cpt_mask = 0;*/
@@ -153,7 +153,7 @@ static size_t mask(size_t a, size_t b) {
   @ ensures \valid(\result);
   @ ensures \result->leaf == ptr;
   @*/
-static struct bittree * __get_leaf_from_block (struct _block * ptr) {
+static struct bittree * __get_leaf_from_block (bt_block * ptr) {
   struct bittree * curr = bt_root;
   assert(bt_root != NULL);
   assert(ptr != NULL);
@@ -185,7 +185,7 @@ 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 bt_remove (struct _block * ptr) {
+static void bt_remove (bt_block * ptr) {
   struct bittree * leaf_to_delete = __get_leaf_from_block (ptr);
   assert(leaf_to_delete->leaf == ptr);
 
@@ -229,7 +229,7 @@ static void bt_remove (struct _block * ptr) {
   @ assigns \nothing;
   @ ensures \valid(\result);
   @*/
-static struct bittree * __most_similar_node (struct _block * ptr) {
+static struct bittree * __most_similar_node (bt_block * ptr) {
   struct bittree * curr = bt_root;
   size_t left_prefix, right_prefix;
   assert(ptr != NULL);
@@ -253,7 +253,7 @@ static struct bittree * __most_similar_node (struct _block * ptr) {
 /* add a block in the structure */
 /*@ requires \valid(ptr);
   @*/
-static void bt_insert (struct _block * ptr) {
+static void bt_insert (bt_block * ptr) {
   struct bittree * new_leaf;
   assert(ptr != NULL);
 
@@ -321,7 +321,7 @@ static void bt_insert (struct _block * ptr) {
   @ ensures \valid(\result);
   @ ensures \result == \null || \result->ptr == (size_t)ptr;
   @*/
-static struct _block * bt_lookup (void * ptr) {
+static bt_block * bt_lookup (void * ptr) {
   struct bittree * tmp = bt_root;
   assert(bt_root != NULL);
   assert(ptr != NULL);
@@ -350,7 +350,7 @@ static struct _block * bt_lookup (void * ptr) {
 /* 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 * bt_find (void * ptr) {
+static bt_block * bt_find (void * ptr) {
   struct bittree * tmp = bt_root;
   if(bt_root == NULL || ptr == NULL) return NULL;
 
@@ -396,7 +396,7 @@ static struct _block * bt_find (void * ptr) {
 /* CLEAN           */
 /*******************/
 /* erase information about initialization of a block */
-static void bt_clean_block_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;
@@ -405,7 +405,7 @@ static void bt_clean_block_init (struct _block * ptr) {
 }
 
 /* erase all information about a block */
-static void bt_clean_block (struct _block * ptr) {
+static void bt_clean_block (bt_block * ptr) {
   if(ptr) {
     bt_clean_block_init(ptr);
     native_free(ptr);
@@ -440,7 +440,7 @@ static void bt_clean () {
 
 #ifdef E_ACSL_DEBUG
 
-static void bt_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,

src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_api.h

@@ -32,7 +32,7 @@
 #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
@@ -41,30 +41,32 @@ struct _block {
   _Bool freeable; //!< True if a block can be de-allocated using `free`
 };
 
+typedef struct bt_block bt_block;
+
 /*! \brief Remove a block from the structure */
-static void bt_remove(struct _block *b);
+static void bt_remove(bt_block *b);
 
 /*! \brief Add a block to the structure */
-static void bt_insert(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 * bt_lookup(void *ptr);
+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 * bt_find(void *ptr);
+static bt_block * bt_find(void *ptr);
 
 /*! \brief Erase the contents of the structure */
 static void bt_clean(void);
 
 /*! \brief Print information about a given block */
-static void bt_print_block(struct _block *b);
+static void bt_print_block(bt_block *b);
 
 /*! \brief Erase information about a block's initialization */
-static void bt_clean_block_init(struct _block *b);
+static void bt_clean_block_init(bt_block *b);
 
 /*! \brief Erase all information about a given block */
-static void bt_clean_block(struct _block *b);
+static void bt_clean_block(bt_block *b);
 #endif

src/plugins/e-acsl/share/e-acsl/bittree_model/e_acsl_bittree_mmodel.c

@@ -64,11 +64,11 @@ 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;
@@ -83,7 +83,7 @@ void* __store_block(void* ptr, size_t size) {
 /* remove the block starting at ptr */
 void __delete_block(void* ptr) {
   DASSERT(ptr != NULL);
-  struct _block * tmp = bt_lookup(ptr);
+  bt_block * tmp = bt_lookup(ptr);
   DASSERT(tmp != NULL);
   bt_clean_block_init(tmp);
   bt_remove(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,7 +110,7 @@ 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 = bt_lookup(ptr);
@@ -123,7 +123,7 @@ void __free(void* ptr) {
 }
 
 int __freeable(void* ptr) {
-  struct _block * tmp;
+  bt_block * tmp;
   if(ptr == NULL)
     return false;
   tmp = bt_lookup(ptr);
@@ -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)
@@ -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);
@@ -226,7 +226,7 @@ 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;
 
@@ -276,7 +276,7 @@ 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;
 
@@ -294,7 +294,7 @@ void __full_init (void * ptr) {
 
 /* mark a block as read-only */
 void __readonly (void * ptr) {
-  struct _block * tmp;
+  bt_block * tmp;
   if (ptr == NULL)
     return;
   tmp = bt_lookup(ptr);
@@ -310,7 +310,7 @@ 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 = bt_find(ptr);
+  bt_block * tmp = bt_find(ptr);
   if(tmp == NULL)
     return false;
 
@@ -334,7 +334,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 = bt_find(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,7 +342,7 @@ 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 = bt_find(ptr);
@@ -353,7 +353,7 @@ 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 = bt_find(ptr);
@@ -363,14 +363,14 @@ int __valid_read(void* ptr, size_t size) {
 
 /* return the base address of the block containing ptr */
 void* __base_addr(void* ptr) {
-  struct _block * tmp = bt_find(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 = bt_find(ptr);
+  bt_block * tmp = bt_find(ptr);
   vassert(tmp != NULL, "\\offset of unallocated memory", NULL);
   return ((size_t)ptr - tmp->ptr);
 }
@@ -408,7 +408,7 @@ void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
 /**********************/
 #ifdef E_ACSL_DEBUG
 /*! \brief print the information about a block */
-void __e_acsl_print_block (struct _block * ptr) {
+void __e_acsl_print_block (bt_block * ptr) {
   bt_print_block(ptr);
 }