From 383ce8f44a1bd863da4bcbb65e10ed7f9b2b273b Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Tue, 22 Mar 2016 13:52:42 +0100
Subject: [PATCH] [Bittree RTL] Doxygen comments
---
.../e-acsl/bittree_model/e_acsl_bittree_api.h | 51 +++++++++----------
.../bittree_model/e_acsl_bittree_mmodel.c | 4 +-
2 files changed, 27 insertions(+), 28 deletions(-)
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 ed710021fa6..1297ccf38b8 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
@@ -31,41 +31,40 @@
#include "stdlib.h"
#include "stdbool.h"
-/* Memory block allocated and may be deallocated */
+/*! \brief Structure representing an allocated memory block */
struct _block {
- size_t ptr; /* base address */
- size_t size; /* block length */
-/* Keep trace of initialized sub-blocks within a memory block */
- unsigned char * init_ptr; /* dynamic array of booleans */
- size_t init_cpt;
- _Bool is_readonly;
- _Bool freeable;
+ size_t ptr; //!< Base address
+ size_t size; //!< Block length (in bytes)
+ unsigned char * init_ptr; //!< Per-bit initialization
+ size_t init_cpt; //!< Number of initialized bytes
+ _Bool is_readonly; //!< True if a block is marked read-only
+ _Bool freeable; //!< True if a block can be de-allocated using `free`
};
-/* remove the block from the structure */
-static void remove_element(struct _block *);
+/*! \brief Remove a block from the structure */
+static void remove_element(struct _block *b);
-/* add a block in the structure */
-static void add_element(struct _block *);
+/*! \brief Add a block to the structure */
+static void add_element(struct _block *b);
-/* return the block B such as : begin addr of B == ptr
- we suppose that such a block exists, but we could return NULL if not */
-static struct _block * get_exact(void *);
+/*! \brief Return block B such that: `\base_addr(B->ptr) == ptr`.
+NB: The function assumes that such a block exists. */
+static struct _block * get_exact(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 * get_cont(void *);
+/*! \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 * get_cont(void *ptr);
-/* erase the content of the structure */
+/*! \brief Erase the contents of the structure */
static void clean_struct(void);
-/* print the information about a block */
-static void print_block(struct _block * ptr );
+/*! \brief Print information about a given block */
+static void print_block(struct _block *b);
-/* erase information about initialization of a block */
-static void clean_init(struct _block * ptr );
+/*! \brief Erase information about a block's initialization */
+static void clean_init(struct _block *b);
-/* erase all information about a block */
-static void clean_block(struct _block * ptr);
+/*! \brief Erase all information about a given block */
+static void clean_block(struct _block *b);
#endif
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 e1b24ea2268..45bbbc15ff5 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
@@ -368,7 +368,7 @@ void* __base_addr(void* ptr) {
return (void*)tmp->ptr;
}
-/* return the offset of ptr within its block */
+/* return the offset of `ptr` within its block */
int __offset(void* ptr) {
struct _block * tmp = get_cont(ptr);
vassert(tmp != NULL, "\\offset of unallocated memory", NULL);
@@ -384,7 +384,7 @@ void __e_acsl_memory_clean() {
clean_struct();
}
-/* adds argv to the memory model */
+/* add `argv` to the memory model */
static void __init_argv(int argc, char **argv) {
int i;
--
GitLab