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 f4f2bd82c7303ad74f4ea205e2162b7e9bbb4dbc..d582bada43fd03200bdeecec3e274de97d17d867 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
@@ -108,7 +108,7 @@ static const int nbr_bits_to_1[256] = {
/**************************/
size_t heap_allocation_size = 0;
-static size_t get_heap_allocation_size(void) {
+size_t get_heap_allocation_size(void) {
return heap_allocation_size;
}
/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h
index a0bbc70310d73d2b99b54541c08771fe540dfe64..51cba9d6a7ab0235d8943068568345140938b93f 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_alias.h
@@ -35,6 +35,8 @@
# define ext_prefix __e_acsl_
# define export_alias(_n) concat(public_prefix, _n)
+/* 'strong' and 'weak' aliases are not portable */
+
/** Define `aliasname` as a strong alias for `name`. */
# define strong_alias(name, aliasname) _strong_alias(name, aliasname)
# define _strong_alias(name, aliasname) \
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
index fe14b1403c6139445d972c596161efbf3f378028..5b9eed9159df5b8c10c0e882e00c2794d6c3f5aa 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_mmodel.c
@@ -26,17 +26,46 @@
* model. See e_acsl_mmodel_api.h for details.
***************************************************************************/
-#include "e_acsl_shadow_layout.h"
-#include "e_acsl_segment_tracking.h"
#include "e_acsl_mmodel_api.h"
-/* Forward declarations */
-static int valid(void*, size_t, void*, void*);
-static int valid_read(void*, size_t, void*, void*);
+/* Public API Bindings {{{ */
+/* Heap allocation (native) */
+#define shadow_malloc malloc
+#define shadow_calloc calloc
+#define shadow_realloc realloc
+#define shadow_free free
+#define shadow_aligned_alloc aligned_alloc
+#define shadow_posix_memalign posix_memalign
+/* Explicit tracking */
+#define delete_block export_alias(delete_block)
+#define store_block export_alias(store_block)
+#define store_block_duplicate export_alias(store_block_duplicate)
+/* Predicates */
+#define segment_offset export_alias(offset)
+#define segment_base_addr export_alias(base_addr)
+#define segment_block_length export_alias(block_length)
+#define valid_read export_alias(valid_read)
+#define valid export_alias(valid)
+#define initialized export_alias(initialized)
+#define freeable export_alias(freeable)
+/* Block initialization */
+#define mark_readonly export_alias(mark_readonly)
+#define initialize export_alias(initialize)
+#define full_init export_alias(full_init)
+/* Memory state initialization */
+#define memory_clean export_alias(memory_clean)
+#define memory_init export_alias(memory_init)
+/* Heap size */
+#define heap_allocation_size export_alias(heap_allocation_size)
+#define get_heap_allocation_size export_alias(get_heap_allocation_size)
+/* }}} */
+
+#include "e_acsl_shadow_layout.h"
+#include "e_acsl_segment_tracking.h"
#define ALLOCATED(_ptr,_size) allocated((uintptr_t)_ptr, _size, (uintptr_t)_ptr)
-static void * store_block(void * ptr, size_t size) {
+void * store_block(void * ptr, size_t size) {
/* Only stack-global memory blocks are recorded explicitly via this function.
* Heap blocks should be tracked internally using memory allocation functions
* such as malloc or calloc. */
@@ -44,24 +73,34 @@ static void * store_block(void * ptr, size_t size) {
return ptr;
}
-static void delete_block(void * ptr) {
+void delete_block(void * ptr) {
/* Block deletion should be performed on stack/global addresses only,
* heap blocks should be deallocated manually via free/cfree/realloc. */
shadow_freea(ptr);
}
-static void * store_block_duplicate(void * ptr, size_t size) {
+void * store_block_duplicate(void * ptr, size_t size) {
if (allocated((uintptr_t)ptr, size, (uintptr_t)ptr))
delete_block(ptr);
shadow_alloca(ptr, size);
return ptr;
}
-static void full_init(void * ptr) {
+/*! \brief Initialize a chunk of memory given by its start address (`addr`)
+ * and byte length (`n`). */
+void initialize(void *ptr, size_t n) {
+ TRY_SEGMENT(
+ (uintptr_t)ptr,
+ initialize_heap_region((uintptr_t)ptr, n),
+ initialize_static_region((uintptr_t)ptr, n)
+ )
+}
+
+void full_init(void * ptr) {
initialize(ptr, block_length(ptr));
}
-static void mark_readonly(void * ptr) {
+void mark_readonly(void * ptr) {
mark_readonly_region((uintptr_t)ptr, block_length(ptr));
}
@@ -75,7 +114,7 @@ static int readonly (void *ptr) {
return IS_ON_GLOBAL(addr) && global_readonly(addr) ? 1 : 0;
}
-static int valid(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
+int valid(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
return
allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
&& !readonly(ptr)
@@ -85,7 +124,7 @@ static int valid(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
;
}
-static int valid_read(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
+int valid_read(void * ptr, size_t size, void *ptr_base, void *addrof_base) {
return allocated((uintptr_t)ptr, size, (uintptr_t)ptr_base)
#ifdef E_ACSL_TEMPORAL
&& temporal_valid(ptr_base, addrof_base)
@@ -97,7 +136,7 @@ static int valid_read(void * ptr, size_t size, void *ptr_base, void *addrof_base
/*! NB: The implementation for this function can also be specified via
* \p base_addr macro that will eventually call ::TRY_SEGMENT. The following
* implementation is preferred for performance reasons. */
-static void * segment_base_addr(void * ptr) {
+void * segment_base_addr(void * ptr) {
TRY_SEGMENT(ptr,
return (void*)heap_info((uintptr_t)ptr, 'B'),
return (void*)static_info((uintptr_t)ptr, 'B'));
@@ -107,7 +146,7 @@ static void * segment_base_addr(void * ptr) {
/*! NB: Implementation of the following function can also be specified
* via \p block_length macro. A more direct approach via ::TRY_SEGMENT
* is preferred for performance reasons. */
-static size_t segment_block_length(void * ptr) {
+size_t segment_block_length(void * ptr) {
TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'L'),
return static_info((uintptr_t)ptr, 'L'))
@@ -117,14 +156,14 @@ static size_t segment_block_length(void * ptr) {
/*! NB: Implementation of the following function can also be specified
* via \p offset macro. A more direct approach via ::TRY_SEGMENT
* is preferred for performance reasons. */
-static int segment_offset(void *ptr) {
+int segment_offset(void *ptr) {
TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'O'),
return static_info((uintptr_t)ptr, 'O'));
return 0;
}
-static int initialized(void * ptr, size_t size) {
+int initialized(void * ptr, size_t size) {
uintptr_t addr = (uintptr_t)ptr;
TRY_SEGMENT_WEAK(addr,
return heap_initialized(addr, size),
@@ -132,7 +171,7 @@ static int initialized(void * ptr, size_t size) {
return 0;
}
-static size_t get_heap_allocation_size(void) {
+size_t get_heap_allocation_size(void) {
return heap_allocation_size;
}
/* }}} */
@@ -197,7 +236,7 @@ static void argv_alloca(int *argc_ref, char *** argv_ref) {
/* Program initialization {{{ */
extern int main(void);
-static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
+void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
describe_run();
/** Verify that the given size of a pointer matches the one in the present
* architecture. This is a guard against Frama-C instrumentations using
@@ -231,44 +270,11 @@ static void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
}
}
-static void memory_clean(void) {
+void memory_clean(void) {
clean_shadow_layout();
}
/* }}} */
-/* Public API Bindings {{{ */
-/* Heap allocation (native) */
-strong_alias(shadow_malloc, malloc)
-strong_alias(shadow_calloc, calloc)
-strong_alias(shadow_realloc, realloc)
-strong_alias(shadow_free, free)
-strong_alias(shadow_free, cfree)
-strong_alias(shadow_aligned_alloc, aligned_alloc)
-strong_alias(shadow_posix_memalign, posix_memalign)
-/* Explicit tracking */
-public_alias(delete_block)
-public_alias(store_block)
-public_alias(store_block_duplicate)
-/* Predicates */
-public_alias2(segment_offset, offset)
-public_alias2(segment_base_addr, base_addr)
-public_alias2(segment_block_length, block_length)
-public_alias(valid_read)
-public_alias(valid)
-public_alias(initialized)
-public_alias(freeable)
-/* Block initialization */
-public_alias(mark_readonly)
-public_alias(initialize)
-public_alias(full_init)
-/* Memory state initialization */
-public_alias(memory_clean)
-public_alias(memory_init)
-/* Heap size */
-public_alias(get_heap_allocation_size)
-public_alias(heap_allocation_size)
-/* }}} */
-
/* Local operations on temporal timestamps {{{ */
/* Remaining functionality (shared between all models) is located in e_acsl_temporal.h */
#ifdef E_ACSL_TEMPORAL
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index d44c7d0c19ff586913c7de3f7cb15c9b3e59dcad..0ea99de90e65b0c94eb969e26f736797cc4224ec 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -430,7 +430,6 @@ static uintptr_t static_info(uintptr_t addr, char type);
static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr);
static int static_allocated(uintptr_t addr, long size, uintptr_t base_ptr);
static int allocated(uintptr_t addr, long size, uintptr_t base_ptr);
-static int freeable(void *ptr);
/*! \brief Quick test to check if a static location belongs to allocation.
* This macro really belongs where static_allocated is defined, but
@@ -584,7 +583,7 @@ static void shadow_alloca(void *ptr, size_t size) {
/*! \brief Nullifies shadow regions of a memory block given by its address.
* \param ptr - base memory address of the stack memory block. */
-static void shadow_freea(void *ptr) {
+void shadow_freea(void *ptr) {
DVALIDATE_STATIC_LOCATION(ptr);
DASSERT(ptr == (void*)base_addr(ptr));
size_t size = block_length(ptr);
@@ -827,7 +826,7 @@ static void mark_readonly_region (uintptr_t addr, long size) {
/*! \brief Amount of heap memory allocated by the program.
* Variable visible externally. */
-static size_t heap_allocation_size = 0;
+size_t heap_allocation_size = 0;
/*! \brief Create a heap shadow for an allocated memory block starting at `ptr`
* and of length `size`. Optionally mark it as initialized if `init`
@@ -892,7 +891,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
* implementation-defined: either a null pointer is returned, or the
* behaviour is as if the size were some non-zero value, except that the
* returned pointer shall not be used to access an object." */
-static void* shadow_malloc(size_t size) {
+void* shadow_malloc(size_t size) {
size_t alloc_size = ALLOC_SIZE(size);
/* Return NULL if the size is too large to be aligned */
@@ -907,7 +906,7 @@ static void* shadow_malloc(size_t size) {
}
/*! \brief Replacement for `calloc` that enables memory tracking */
-static void* shadow_calloc(size_t nmemb, size_t size) {
+void* shadow_calloc(size_t nmemb, size_t size) {
/* Since both `nmemb` and `size` are both of size `size_t` the multiplication
* of the arguments (which gives the actual allocation size) might lead to an
* integer overflow. The below code checks for an overflow and sets the
@@ -969,7 +968,7 @@ static void unset_heap_segment(void *ptr, int init, const char *function) {
}
/*! \brief Replacement for `free` with memory tracking */
-static void shadow_free(void *ptr) {
+void shadow_free(void *ptr) {
if (ptr != NULL) { /* NULL is a valid behaviour */
if (freeable(ptr)) {
unset_heap_segment(ptr, 1, "free");
@@ -982,7 +981,7 @@ static void shadow_free(void *ptr) {
/* }}} */
/* Heap reallocation (realloc) {{{ */
-static void* shadow_realloc(void *ptr, size_t size) {
+void* shadow_realloc(void *ptr, size_t size) {
char *res = NULL; /* Resulting pointer */
/* If the pointer is NULL then realloc is equivalent to malloc(size) */
if (ptr == NULL)
@@ -1043,7 +1042,7 @@ static void* shadow_realloc(void *ptr, size_t size) {
/* Heap aligned allocation (aligned_alloc) {{{ */
/*! \brief Replacement for `aligned_alloc` with memory tracking */
-static void *shadow_aligned_alloc(size_t alignment, size_t size) {
+void *shadow_aligned_alloc(size_t alignment, size_t size) {
/* Check if:
* - size and alignment are greater than zero
* - alignment is a power of 2
@@ -1063,7 +1062,7 @@ static void *shadow_aligned_alloc(size_t alignment, size_t size) {
/* Heap aligned allocation (posix_memalign) {{{ */
/*! \brief Replacement for `posix_memalign` with memory tracking */
-static int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
+int shadow_posix_memalign(void **memptr, size_t alignment, size_t size) {
/* Check if:
* - size and alignment are greater than zero
* - alignment is a power of 2 and a multiple of sizeof(void*) */
@@ -1130,7 +1129,7 @@ static int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) {
* As some of the other functions, \b \\freeable can be expressed using
* ::IS_ON_HEAP, ::heap_allocated and ::base_addr. Here direct
* implementation is preferred for performance reasons. */
-static int freeable(void *ptr) { /* + */
+int freeable(void *ptr) { /* + */
uintptr_t addr = (uintptr_t)ptr;
/* Address is not on the program's heap, so cannot be freed */
if (!IS_ON_HEAP(addr))
@@ -1281,18 +1280,6 @@ static int allocated(uintptr_t addr, long size, uintptr_t base) {
}
/* }}} */
-/* Any initialization {{{ */
-/*! \brief Initialize a chunk of memory given by its start address (`addr`)
- * and byte length (`n`). */
-static void initialize(void *ptr, size_t n) {
- TRY_SEGMENT(
- (uintptr_t)ptr,
- initialize_heap_region((uintptr_t)ptr, n),
- initialize_static_region((uintptr_t)ptr, n)
- )
-}
-/* }}} */
-
/* Internal state print (debug mode) {{{ */
#ifdef E_ACSL_DEBUG
/* ! \brief Print human-readable representation of a byte in a primary