From 5c353fc579047e02098819cdf59b2b326c1fc8be Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 22 Mar 2016 13:11:41 +0100
Subject: [PATCH] [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
---
.../e-acsl/bittree_model/e_acsl_bittree.h | 17 +++++++++++++-
.../e-acsl/bittree_model/e_acsl_bittree_api.h | 18 +++++++--------
.../bittree_model/e_acsl_bittree_mmodel.c | 23 -------------------
3 files changed, 25 insertions(+), 33 deletions(-)
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 29b25241027..0b05eb4afd8 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 6161ac9ab3c..ae226007f1f 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 2ffcba07229..bf3b9b79c82 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
--
GitLab