From 83970cf6436f87654ebba56297d72a459b3d8220 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 18 Feb 2016 10:18:52 +0100
Subject: [PATCH] [RTL] Make debug functions in ADT-based models be compilable
only with debug macro
---
.../e-acsl/adt_models/e_acsl_adt_mmodel.h | 19 ++++++++++-----
.../share/e-acsl/adt_models/e_acsl_bittree.h | 22 +++++++++--------
.../share/e-acsl/adt_models/e_acsl_list.h | 17 ++++++++-----
.../e-acsl/adt_models/e_acsl_splaytree.h | 24 ++++++++++++-------
.../share/e-acsl/adt_models/e_acsl_tree.h | 23 +++++++++++-------
5 files changed, 65 insertions(+), 40 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
index e2f7516b178..bc59349979d 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_adt_mmodel.h
@@ -20,6 +20,9 @@
/* */
/**************************************************************************/
+#ifndef E_ACSL_ADT_MMODEL
+#define E_ACSL_ADT_MMODEL
+
#include "e_acsl_string.h"
#include "e_acsl_printf.h"
#include "e_acsl_assert.h"
@@ -386,11 +389,12 @@ void __e_acsl_memory_init(int *argc_ref, char ***argv_ref) { }
/**********************/
/* DEBUG */
/**********************/
+#ifdef E_ACSL_DEBUG
/* print the information about a block */
-void __print_block (struct _block * ptr) {
+void __e_acsl_print_block (struct _block * ptr) {
if (ptr != NULL) {
- printf("%p; %zu Bytes; %slitteral; [init] : %li ",
+ DLOG("%p; %zu Bytes; %slitteral; [init] : %li ",
(char*)ptr->ptr, ptr->size,
ptr->is_litteral_string ? "" : "not ", ptr->init_cpt);
if(ptr->init_ptr != NULL) {
@@ -398,14 +402,17 @@ void __print_block (struct _block * ptr) {
for(i = 0; i < ptr->size; i++) {
int ind = i / 8;
int one_bit = (unsigned)1 << (8 - (i % 8) - 1);
- printf("%i", (ptr->init_ptr[ind] & one_bit) != 0);
+ DLOG("%i", (ptr->init_ptr[ind] & one_bit) != 0);
}
}
- printf("\n");
+ DLOG("\n");
}
}
/* print the content of the abstract structure */
-void __debug() {
- __debug_struct();
+void __e_acsl_debug() {
+ __e_acsl_debug_struct();
}
+
+#endif
+#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
index f91d0123bd1..f02290d5df7 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_bittree.h
@@ -431,31 +431,33 @@ static void __clean_struct () {
/* DEBUG */
/*********************/
+#ifdef E_ACSL_DEBUG
/* called from __debug_struct */
/* recursively print the content of the structure */
/*@ assigns \nothing;
@*/
-static void __debug_rec (struct bittree * ptr, int depth) {
+static void debug_rec (struct bittree * ptr, int depth) {
int i;
if(ptr == NULL)
return;
for(i = 0; i < depth; i++)
- printf(" ");
+ DLOG(" ");
if(ptr->is_leaf)
- __print_block(ptr->leaf);
+ __e_acsl_print_block(ptr->leaf);
else {
- printf("%p -- %p\n", (void*)ptr->mask, (void*)ptr->addr);
- __debug_rec(ptr->left, depth+1);
- __debug_rec(ptr->right, depth+1);
+ DLOG("%p -- %p\n", (void*)ptr->mask, (void*)ptr->addr);
+ debug_rec(ptr->left, depth+1);
+ debug_rec(ptr->right, depth+1);
}
}
/* print the content of the structure */
/*@ assigns \nothing;
@*/
-static void __debug_struct () {
- printf("------------DEBUG\n");
- __debug_rec(__root, 0);
- printf("-----------------\n");
+void __e_acsl_debug_struct () {
+ DLOG("------------DEBUG\n");
+ debug_rec(__root, 0);
+ DLOG("-----------------\n");
}
#endif
+#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_list.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_list.h
index 04e2e34f7cb..4ccfb00d097 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_list.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_list.h
@@ -123,14 +123,19 @@ static void __clean_struct() {
}
}
-
-static void __debug_struct() {
+/*********************/
+/* DEBUG */
+/*********************/
+#ifdef E_ACSL_DEBUG
+void __e_acsl_debug_struct() {
struct _node * tmp = __list;
- printf("\t\t\t------------DEBUG\n");
+ DLOG("\t\t\t------------DEBUG\n");
for(; tmp != NULL; tmp = tmp->next) {
- printf("\t\t\t");
- __print_block(tmp->value);
+ DLOG("\t\t\t");
+ __e_acsl_print_block(tmp->value);
}
- printf("\t\t\t-----------------\n");
+ DLOG("\t\t\t-----------------\n");
}
+
+#endif
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h
index 6c86b89e421..8fe4837efbf 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_splaytree.h
@@ -180,17 +180,23 @@ static void __clean_struct() {
__clean_rec(__root);
}
-static void __debug_rec(struct _node * ptr) {
+/*********************/
+/* DEBUG */
+/*********************/
+#ifdef E_ACSL_DEBUG
+static void debug_rec(struct _node * ptr) {
if(ptr == NULL) return;
- __debug_rec(ptr->left);
- printf("\t\t\t");
- __print_block(ptr->value);
- __debug_rec(ptr->right);
+ debug_rec(ptr->left);
+ DLOG("\t\t\t");
+ __e_acsl_print_block(ptr->value);
+ debug_rec(ptr->right);
}
-static void __debug_struct() {
- printf("\t\t\t------------DEBUG\n");
- __debug_rec(__root);
- printf("\t\t\t-----------------\n");
+void __e_acsl_debug_struct() {
+ DLOG("\t\t\t------------DEBUG\n");
+ debug_rec(__root);
+ DLOG("\t\t\t-----------------\n");
}
+
+#endif
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_tree.h b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_tree.h
index d10bf1bef72..4e55bd5fde0 100644
--- a/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_tree.h
+++ b/src/plugins/e-acsl/share/e-acsl/adt_models/e_acsl_tree.h
@@ -140,18 +140,23 @@ static void __clean_struct() {
__clean_rec(__root);
}
-
-static void __debug_rec(struct _node * ptr) {
+/*********************/
+/* DEBUG */
+/*********************/
+#ifdef E_ACSL_DEBUG
+static void debug_rec(struct _node * ptr) {
if(ptr == NULL) return;
- __debug_rec(ptr->left);
- printf("\t\t\t");
- __print_block(ptr->value);
- __debug_rec(ptr->right);
+ debug_rec(ptr->left);
+ DLOG("\t\t\t");
+ __e_acsl_print_block(ptr->value);
+ debug_rec(ptr->right);
}
-static void __debug_struct() {
- printf("\t\t\t------------DEBUG\n");
+void __e_acsl_debug_struct() {
+ DLOG("\t\t\t------------DEBUG\n");
__debug_rec(__root);
- printf("\t\t\t-----------------\n");
+ DLOF("\t\t\t-----------------\n");
}
+
+#endif
#endif
--
GitLab