From 7faeaf67956808bfb06859ec7d97a73526395a83 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 18 Mar 2016 15:59:00 +0100
Subject: [PATCH] [RTL] Doxygen-style comments for e_acsl_mmodel_api.h
---
.../e-acsl/share/e-acsl/e_acsl_mmodel_api.h | 128 ++++++++++++------
1 file changed, 83 insertions(+), 45 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
index 8fec227fc0b..05546aaf273 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_mmodel_api.h
@@ -20,71 +20,87 @@
/* */
/**************************************************************************/
+/*! ***********************************************************************
+ * \file e_acsl_mmodel_api.h
+ * \brief Public C API of E-ACSL Runtime Library
+ *
+ * Functions and variables with non-static linkage used for instrumentation.
+***************************************************************************/
+
#ifndef E_ACSL_MMODEL
#define E_ACSL_MMODEL
#include <stddef.h>
-/* Runtime assertion verifying a predicate */
+/*! \brief Runtime assertion verifying a predicate
+ * \param pred integer code of a predicate
+ * \param kind a C string representing an annotation's
+ * kind (e.g., "Assertion")
+ * \param fct
+ * \param pred_txt stringified predicate
+ * \param line line number of the predicate placement in the
+ * un-instrumented file */
/*@ requires pred != 0;
@ assigns \nothing; */
void e_acsl_assert(int pred, char *kind, char *fct, char *pred_txt, int line)
__attribute__((FC_BUILTIN));
-/* allocate size bytes and store the returned block
- * for further information, see malloc */
+/*! \brief Drop-in replacement for \p malloc with memory tracking enabled.
+ *
+ * For further information, see \p malloc(3). */
/*@ assigns \result \from size; */
void * __malloc(size_t size)
__attribute__((FC_BUILTIN)) ;
-/* free the block starting at ptr,
- * for further information, see free */
-/*@ assigns *((char*)ptr) \from ptr; */
-void __free(void * ptr)
- __attribute__((FC_BUILTIN));
-
-/* evaluate to a non-zero value if ptr points to a start address of a block
- * allocated via a memory allocation function (e.g., malloc, realloc etc) */
-/*@ assigns \result \from ptr; */
-int __freeable(void * ptr)
+/*! \brief Drop-in replacement for \p calloc with memory tracking enabled.
+ *
+ * For further information, see \p calloc(3). */
+/*@ assigns \result \from nbr_elt,size_elt; */
+void * __calloc(size_t nbr_elt, size_t size_elt)
__attribute__((FC_BUILTIN));
-/* resize the block starting at ptr to fit its new size,
- * for further information, see realloc */
+/*! \brief Drop-in replacement for \p realloc with memory tracking enabled.
+ *
+ * For further information, see realloc(3) */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
void * __realloc(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* allocate memory for an array of nbr_block elements of size_block size,
- * this memory is set to zero, the returned block is stored,
- * for further information, see calloc */
-/*@ assigns \result \from nbr_elt,size_elt; */
-void * __calloc(size_t nbr_elt, size_t size_elt)
+/*! \brief Drop-in replacement for \p free with memory tracking enabled.
+ *
+ * For further information, see \p free(3). */
+/*@ assigns *((char*)ptr) \from ptr; */
+void __free(void * ptr)
__attribute__((FC_BUILTIN));
-/* From outside the library, the following functions have no side effect */
-
-/* store the block of size bytes starting at ptr */
+/*! \brief Store stack or globally-allocated memory block
+ * starting at an address given by \p ptr.
+ *
+ * \param ptr base address of the tracked memory block
+ * \param size size of the tracked block in bytes */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
void * __store_block(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* remove the block starting at ptr */
+/*! \brief Remove a memory block which base address is \p ptr from tracking. */
/*@ assigns \nothing; */
void __delete_block(void * ptr)
__attribute__((FC_BUILTIN));
-/* mark the size bytes of ptr as initialized */
+/*! \brief Mark the \p size bytes starting at an address given by \p ptr as
+ * initialized. */
/*@ assigns \nothing; */
void __initialize(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* mark all bytes of ptr as initialized */
+/*! \brief Mark all bytes belonging to a memory block which start address is
+ * given by \p ptr as initialized. */
/*@ assigns \nothing; */
void __full_init(void * ptr)
__attribute__((FC_BUILTIN));
-/* marks a block as read-only */
+/*! \brief Mark a memory block which start address is given by \ptr as
+ * read-only. */
/*@ assigns \nothing; */
void __readonly(void * ptr)
__attribute__((FC_BUILTIN));
@@ -93,34 +109,57 @@ void __readonly(void * ptr)
/* E-ACSL annotations */
/* ****************** */
-/* return whether the first size bytes of ptr are readable/writable */
+/*!\brief Implementation of the \b \\freeable predicate of E-ACSL.
+ *
+ * Evaluate to a non-zero value if \p ptr points to a start address of
+ * a block allocated via \p malloc, \p calloc or \p realloc. */
+/*@ assigns \result \from ptr; */
+int __freeable(void * ptr)
+ __attribute__((FC_BUILTIN));
+
+/*! \brief Implementation of the \b \\valid predicate of E-ACSL.
+ *
+ * Return a non-zero value if the first \p size bytes starting at an address given
+ * by \p ptr are readable and writable and 0 otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __valid(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* return whether the first size bytes of ptr are readable */
+/*! \brief Implementation of the \b \\valid_read predicate of E-ACSL.
+ *
+ * Return a non-zero value if the first \p size bytes starting at an address
+ * given by \p ptr are readable and 0 otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \valid_read(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __valid_read(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* return the base address of the block containing ptr */
+/*! \brief Implementation of the \b \\base_addr predicate of E-ACSL.
+ *
+ * Return the base address of the memory block containing an address given
+ * by \p ptr */
/*@ ensures \result == \base_addr(ptr);
@ assigns \result \from ptr; */
void * __base_addr(void * ptr)
__attribute__((FC_BUILTIN));
-/* return the length (in bytes) of the block containing ptr */
+/*! \brief Implementation of the \b \\block_length predicate of E-ACSL.
+ *
+ * Return the byte length of the memory block of the block containing a memory
+ * address given by \p ptr */
/*@ ensures \result == \block_length(ptr);
@ assigns \result \from ptr; */
size_t __block_length(void * ptr)
__attribute__((FC_BUILTIN));
-/* return the offset of ptr within its block
- * FIXME: The return type of __offset should be changed to size_t.
+/*! \brief Implementation of the \b \\offset predicate of E-ACSL.
+ *
+ * Return the byte offset of address given by \p ptr within a memory blocks
+ * it belongs to */
+/* FIXME: The return type of __offset should be changed to size_t.
* In the current E-ACSL/Frama-C implementation, however, this change
* leads to a Frama-C failure. */
/*@ ensures \result == \offset(ptr);
@@ -128,41 +167,40 @@ size_t __block_length(void * ptr)
int __offset(void * ptr)
__attribute__((FC_BUILTIN));
-/* return whether the size bytes of ptr are initialized */
+/*! \brief Implementation of the \b \\initialized predicate of E-ACSL.
+ *
+ * Return a non-zero value if \p size bytes starting from an address given by
+ * \p ptr are initialized and zero otherwise. */
/*@ ensures \result == 0 || \result == 1;
@ ensures \result == 1 ==> \initialized(((char *)ptr)+(0..size-1));
@ assigns \result \from *(((char*)ptr)+(0..size-1)); */
int __initialized(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/* print the content of the abstract structure */
-void __e_acsl_memory_debug(void)
- __attribute__((FC_BUILTIN));
-
/*@ ghost int extern __e_acsl_internal_heap; */
-/* erase the content of the abstract structure
- * have to be called at the end of the `main` */
+/*! \brief Clean-up memory tracking state before a program's termination. */
/*@ assigns \nothing; */
void __e_acsl_memory_clean(void)
__attribute__((FC_BUILTIN));
-/* initialize the abstract structure
- * have to be called before any other statement in `main` */
+/*! \brief Initialize memory tracking state.
+ *
+ * Called before any other statement in \p main */
/*@ assigns \nothing; */
void __e_acsl_memory_init(int *argc_ref, char ***argv, size_t ptr_size)
__attribute__((FC_BUILTIN));
-/* return the number of bytes dynamically allocated */
+/*! \brief Return the cumulative size (in bytes) of tracked heap allocation. */
/*@ assigns \result \from __e_acsl_internal_heap; */
size_t __get_heap_size(void)
__attribute__((FC_BUILTIN));
-/* for predicates */
+/*! \brief A variable holding a cumulative size (in bytes) of tracked
+ * heap allocation. */
extern size_t __heap_size;
/*@ predicate diffSize{L1,L2}(integer i) =
\at(__heap_size, L1) - \at(__heap_size, L2) == i;
*/
-
#endif
--
GitLab