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 29b252410276d9a12e93a6f1ef1a58c19b459df6..0b05eb4afd87e82eb3a2d9fac0dd2d3bd13488cc 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 @@ -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) { 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 6161ac9ab3cf5e12ce8c9853b037e3b0d7dd1721..ae226007f1f36e6cfb5be29ff07d006015bff823 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 @@ -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); 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 2ffcba07229d40c2924cf787b900f96a4fa893eb..bf3b9b79c82063f8fce311957ca0f633f5dac747 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 @@ -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