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 04043c6b86ec57f7f8ad37d099faf5fa1977bf55..617807e4b7b2e1b43668884afe979097b3838676 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
@@ -21,7 +21,7 @@
/**************************************************************************/
/*! ***********************************************************************
- * \file e_acsl_bittree.h
+ * \file e_acsl_bittree.h
* \brief Patricia Trie API Implementation
***************************************************************************/
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 5f32ca605431b54c86ca074f0eb03e52c5b273ab..2913a829f55684b268d06caccad8a870389df99c 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
@@ -46,7 +46,7 @@ typedef struct bt_block bt_block;
/*! \brief Structure representing a bittree node */
struct bt_node {
_Bool is_leaf;
- size_t addr, mask;
+ size_t addr, mask;
struct bt_node * left, * right, * parent;
bt_block * leaf;
};
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 afff5c1fb4d543a8f6f3cfed2c05ccc46f19cda1..406eebb83b1f70074012f63812eef6fa62261e73 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
@@ -21,8 +21,8 @@
/**************************************************************************/
/*! ***********************************************************************
- * \file e_acsl_bittree_mmodel.c
- * \brief Implementation of E-ACSL public API using a memory model based
+ * \file e_acsl_bittree_mmodel.c
+ * \brief Implementation of E-ACSL public API using a memory model based
* on Patricia Trie. See e_acsl_mmodel_api.h for details.
***************************************************************************/
@@ -192,7 +192,7 @@ static int initialized(void * ptr, size_t size) {
/* return the length (in bytes) of the block containing ptr */
static size_t block_length(void* ptr) {
bt_block * tmp = bt_find(ptr);
- /* Hard failure when un-allocated memory is used */
+ /* Hard failure when un-allocated memory is used */
vassert(tmp != NULL, "\\block_length of unallocated memory", NULL);
return tmp->size;
}
@@ -242,7 +242,7 @@ static void* store_block(void* ptr, size_t size) {
DASSERT(ptr != NULL);
tmp = native_malloc(sizeof(bt_block));
DASSERT(tmp != NULL);
- tmp->ptr = (size_t)ptr;
+ tmp->ptr = (uintptr_t)ptr;
tmp->size = size;
tmp->init_ptr = NULL;
tmp->init_bytes = 0;
@@ -324,7 +324,7 @@ static int bittree_posix_memalign(void **memptr, size_t alignment, size_t size)
/* Make sure that the first argument to posix memalign is indeed allocated */
vassert(valid(memptr, sizeof(void*)),
- "\\invalid memptr in posix_memalign", NULL);
+ "\\invalid memptr in posix_memalign", NULL);
int res = native_posix_memalign(memptr, alignment, size);
if (!res) {
@@ -369,7 +369,7 @@ static void* bittree_realloc(void* ptr, size_t size) {
tmp->init_bytes = size;
/* realloc bigger larger block */
} else {
- /* size of tmp->init_ptr in the new block */
+ /* size of tmp->init_ptr in the new block */
int nb = needed_bytes(size);
/* number of bits that need to be set in tmp->init_ptr */
int nb_old = needed_bytes(tmp->size);
@@ -465,7 +465,7 @@ public_alias(block_length)
public_alias(initialized)
public_alias(freeable)
public_alias(readonly)
-/* Block initialization */
+/* Block initialization */
public_alias(initialize)
public_alias(full_init)
/* Memory state initialization */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
index 0ba0811c54f2f3f54be11dae6d6752fd728cb493..1640746c7642518bd18f214fe892bda589f0c501 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_malloc.h
@@ -21,7 +21,7 @@
/**************************************************************************/
/*! ***********************************************************************
- * \file e_acsl_malloc.h
+ * \file e_acsl_malloc.h
*
* \brief E-ACSL memory allocation bindings.
***************************************************************************/
@@ -34,12 +34,12 @@
#ifndef E_ACSL_MALLOC
#define E_ACSL_MALLOC
-/* Define ALIASNAME as a strong alias for NAME. */
+/** Define `aliasname` as a strong alias for `name`. */
# define strong_alias(name, aliasname) _strong_alias(name, aliasname)
# define _strong_alias(name, aliasname) \
extern __typeof (name) aliasname __attribute__ ((alias (#name)));
-/* Define ALIASNAME as a weak alias for NAME. */
+/** Define `aliasname` as a weak alias for `name`. */
# define weak_alias(name, aliasname) _weak_alias (name, aliasname)
# define _weak_alias(name, aliasname) \
extern __typeof (name) aliasname __attribute__ ((weak, alias (#name)));
@@ -47,16 +47,24 @@
# define preconcat(x,y) x ## y
# define concat(x,y) preconcat(x,y)
-/* Prefix added to all jemalloc functions, e.g., an actual jemalloc `malloc`
+/** Prefix added to all jemalloc functions, e.g., an actual jemalloc `malloc`
* is renamed to `__e_acsl_native_malloc` */
-# define native_prefix __e_acsl_native_
+# define native_prefix __e_acsl_native_
# define alloc_func_def(f,...) concat(native_prefix,f)(__VA_ARGS__)
-# define alloc_func_macro(f) concat(native_prefix,f)
+# define alloc_func_macro(f) concat(native_prefix,f)
+/** Prefix added to public functions of E-ACSL public API */
# define public_prefix __e_acsl_
+/** Make a strong alias from some function named `f` to __e_acsl_f */
# define public_alias(f) strong_alias(f, concat(public_prefix,f))
+/** Make a strong alias from some function named `f1` to __e_acsl_f2 */
# define public_alias2(f1,f2) strong_alias(f1, concat(public_prefix,f2))
+/* The following declares jemalloc allocation functions.
+ * For instance:
+ * extern void *alloc_func_def(malloc, size_t);
+ * becomes:
+ * extern void *__e_acsl_native_malloc(size_t); */
extern void *alloc_func_def(malloc, size_t);
extern void *alloc_func_def(calloc, size_t, size_t);
extern void *alloc_func_def(realloc, void*, size_t);
@@ -64,6 +72,9 @@ extern void *alloc_func_def(aligned_alloc, size_t, size_t);
extern int alloc_func_def(posix_memalign, void **, size_t, size_t);
extern void alloc_func_def(free,void*);
+/* Shortcuts for allocation functions used within this RTL (so they are not
+ * tracked). For example:
+ * native_malloc => __e_acsl_native_malloc */
# define native_malloc alloc_func_macro(malloc)
# define native_realloc alloc_func_macro(realloc)
# define native_calloc alloc_func_macro(calloc)
@@ -71,14 +82,10 @@ extern void alloc_func_def(free,void*);
# define native_aligned_alloc alloc_func_macro(aligned_alloc)
# define native_free alloc_func_macro(free)
-/* Return a true value if x is a power of 2 and false otherwise */
-int powof2(size_t x) {
- while (((x & 1) == 0) && x > 1) /* While x is even and > 1 */
- x >>= 1;
- return (x == 1);
+/* \return a true value if x is a power of 2 and false otherwise */
+static int powof2(size_t x) {
+ while (((x & 1) == 0) && x > 1) /* while x is even and > 1 */
+ x >>= 1;
+ return (x == 1);
}
-
#endif
-
-
-