[RTL] Updates in bittree RTL to enfornce SOC. This is such that:

  - e_acsl_bittree_api.h -- internal API of a Patricie Trie
  - e_acsl_bittree.h -- full implementation of the API
  - e_acsl_bittree_mmodel.c -- implementation of the E-ACSL public API
    using functions from e_acsl_bittree_api.h

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

@@ -411,6 +411,22 @@ static struct _block * __get_cont (void * ptr) {
 /*******************/
 /* CLEAN           */
 /*******************/
+/* erase information about initialization of a block */
+static void __clean_init (struct _block * ptr) {
+  if(ptr->init_ptr != NULL) {
+    native_free(ptr->init_ptr);
+    ptr->init_ptr = NULL;
+  }
+  ptr->init_cpt = 0;
+}
+
+/* erase all information about a block */
+static void __clean_block (struct _block * ptr) {
+  if(ptr) {
+    __clean_init(ptr);
+    native_free(ptr);
+  }
+}
 
 /* called from __clean_struct */
 /* recursively erase the content of the structure */
@@ -454,7 +470,6 @@ static void __print_block(struct _block * ptr) {
   }
 }
 
-/* called from __debug_struct */
 /* recursively print the content of the structure starting from a given node */
 /*@ assigns \nothing; */
 static void print_bittree_node(struct bittree * ptr, int depth) {

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

@@ -42,15 +42,6 @@ struct _block {
   _Bool freeable;
 };
 
-/* print the information about a block */
-static void __print_block(struct _block * ptr );
-
-/* erase information about initialization of a block */
-static void __clean_init(struct _block * ptr );
-
-/* erase all information about a block */
-static void __clean_block(struct _block * ptr);
-
 /* remove the block from the structure */
 static void  __remove_element(struct _block *);
 
@@ -69,6 +60,15 @@ static struct _block * __get_cont(void *);
 /* erase the content of the structure */
 static void __clean_struct(void);
 
+/* print the information about a block */
+static void __print_block(struct _block * ptr );
+
+/* erase information about initialization of a block */
+static void __clean_init(struct _block * ptr );
+
+/* erase all information about a block */
+static void __clean_block(struct _block * ptr);
+
 /* print the content of the structure */
 static void  __debug_struct(void);
 

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

@@ -63,23 +63,6 @@ size_t __get_memory_size(void) {
 /* ALLOCATION             */
 /**************************/
 
-/* erase information about initialization of a block */
-static void __clean_init (struct _block * ptr) {
-  if(ptr->init_ptr != NULL) {
-    native_free(ptr->init_ptr);
-    ptr->init_ptr = NULL;
-  }
-  ptr->init_cpt = 0;
-}
-
-/* erase all information about a block */
-static void __clean_block (struct _block * ptr) {
-  if(ptr) {
-    __clean_init(ptr);
-    native_free(ptr);
-  }
-}
-
 /* store the block of size bytes starting at ptr, the new block is returned.
  * Warning: the return type is implicitly (struct _block*). */
 void* __store_block(void* ptr, size_t size) {
@@ -414,10 +397,6 @@ static void __init_argv(int argc, char **argv) {
   }
 }
 
-/* initialize contents of the abstract structure and record arguments
- *  'argc_ref` address the variable holding the argc parameter
- *  'argv_ref` address the variable holding the argv parameter
- *  'ptr_size` the size of the pointer computed during instrumentation. */
 void __e_acsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
   arch_assert(ptr_size);
   if (argc_ref)
@@ -428,7 +407,6 @@ 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);
@@ -438,6 +416,5 @@ void __e_acsl_print_block (struct _block * ptr) {
 void __e_acsl_print_bittree() {
   print_bittree();
 }
-
 #endif
 #endif