From 82788932c7c7b3bb518584d160d2970b49c384c8 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 30 Sep 2020 11:00:15 +0200
Subject: [PATCH] [eacsl:runtime] Add `eacsl` prefix to C defines
---
.../instrumentation_model/e_acsl_assert.c | 6 +-
.../instrumentation_model/e_acsl_assert.h | 10 +-
.../instrumentation_model/e_acsl_temporal.c | 30 ++---
.../instrumentation_model/e_acsl_temporal.h | 50 ++++----
.../share/e-acsl/internals/e_acsl_malloc.c | 18 +--
.../share/e-acsl/internals/e_acsl_malloc.h | 71 +++++------
.../e-acsl/libc_replacements/e_acsl_stdio.c | 12 +-
.../e-acsl/libc_replacements/e_acsl_stdio.h | 24 ++--
.../e-acsl/libc_replacements/e_acsl_string.c | 30 ++---
.../e-acsl/libc_replacements/e_acsl_string.h | 45 ++++---
.../numerical_model/e_acsl_floating_point.c | 14 +--
.../numerical_model/e_acsl_floating_point.h | 16 +--
.../e-acsl/numerical_model/e_acsl_gmp_api.h | 116 +++++++++---------
.../bittree_model/e_acsl_bittree.c | 6 +-
.../bittree_model/e_acsl_bittree.h | 2 +-
.../e_acsl_bittree_observation_model.c | 92 +++++++-------
.../e_acsl_bittree_timestamp_retrieval.c | 2 +-
.../e-acsl/observation_model/e_acsl_heap.c | 4 +-
.../e-acsl/observation_model/e_acsl_heap.h | 16 +--
.../e_acsl_observation_model.c | 2 +-
.../e_acsl_observation_model.h | 68 +++++-----
.../internals/e_acsl_heap_tracking.c | 4 +-
.../e_acsl_segment_observation_model.c | 40 +++---
.../segment_model/e_acsl_segment_tracking.c | 10 +-
.../segment_model/e_acsl_segment_tracking.h | 5 +-
.../segment_model/e_acsl_shadow_layout.c | 8 +-
26 files changed, 351 insertions(+), 350 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
index 5ede932a5a8..076a44f350f 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.c
@@ -32,13 +32,13 @@
#include "e_acsl_assert.h"
-int runtime_sound_verdict = 1;
+int eacsl_runtime_sound_verdict = 1;
#ifndef E_ACSL_EXTERNAL_ASSERT
/*! \brief Default implementation of E-ACSL runtime assertions */
-void runtime_assert(int predicate, const char *kind, const char *fct,
+void eacsl_runtime_assert(int predicate, const char *kind, const char *fct,
const char *pred_txt, const char * file, int line) {
- if (runtime_sound_verdict) {
+ if (eacsl_runtime_sound_verdict) {
if (! predicate) {
STDERR("%s: In function '%s'\n"
"%s:%d: Error: %s failed:\n"
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
index 9bdf8a8b12e..e9970b9edf5 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_assert.h
@@ -30,14 +30,14 @@
#include "../internals/e_acsl_alias.h"
-#define runtime_sound_verdict export_alias(sound_verdict)
-#define runtime_assert export_alias(assert)
+#define eacsl_runtime_sound_verdict export_alias(sound_verdict)
+#define eacsl_runtime_assert export_alias(assert)
/*! E-ACSL instrumentation automatically sets this global to 0 if its verdict
becomes unsound.
TODO: may only happen for annotations containing memory-related properties.
For arithmetic properties, the verdict is always sound (?). */
-extern int runtime_sound_verdict;
+extern int eacsl_runtime_sound_verdict;
/*! \brief Runtime assertion verifying a given predicate
* \param pred integer code of a predicate
@@ -48,8 +48,8 @@ extern int runtime_sound_verdict;
* \param line line of predicate placement in the un-instrumented file */
/*@ requires pred != 0;
@ assigns \nothing; */
-void runtime_assert(int pred, const char *kind, const char *fct, const char *pred_txt,
- const char * file, int line)
+void eacsl_runtime_assert(int pred, const char *kind, const char *fct,
+ const char *pred_txt, const char * file, int line)
__attribute__((FC_BUILTIN));
#endif // E_ACSL_ASSERT_H
\ No newline at end of file
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c
index 92f8f71d164..399b60cd70c 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.c
@@ -32,17 +32,17 @@
#include "e_acsl_temporal.h"
/* Temporal store {{{ */
-void temporal_store_nblock(void *lhs, void *rhs) {
+void eacsl_temporal_store_nblock(void *lhs, void *rhs) {
store_temporal_referent(lhs, origin_timestamp(rhs));
}
-void temporal_store_nreferent(void *lhs, void *rhs) {
+void eacsl_temporal_store_nreferent(void *lhs, void *rhs) {
store_temporal_referent(lhs, referent_timestamp(rhs));
}
/* }}} */
/* Memcpy/memset {{{ */
-void temporal_memcpy(void *dest, void *src, size_t size) {
+void eacsl_temporal_memcpy(void *dest, void *src, size_t size) {
/* Memcpy is only relevant for pointers here, so if there is a
* copy under a pointer's size then there no point in copying memory*/
if (size >= sizeof(void*)) {
@@ -54,7 +54,7 @@ void temporal_memcpy(void *dest, void *src, size_t size) {
}
}
-void temporal_memset(void *dest, int c, size_t size) {
+void eacsl_temporal_memset(void *dest, int c, size_t size) {
DVALIDATE_WRITEABLE(dest, size, dest);
void *dest_shadow = (void *)temporal_referent_shadow(dest);
memset(dest_shadow, 0, size);
@@ -62,22 +62,22 @@ void temporal_memset(void *dest, int c, size_t size) {
/* }}} */
/* Function parameters {{{ */
-void temporal_save_nblock_parameter(void *ptr, unsigned int param) {
+void eacsl_temporal_save_nblock_parameter(void *ptr, unsigned int param) {
parameter_referents[param].ptr = ptr;
parameter_referents[param].temporal_flow = TBlockN;
}
-void temporal_save_nreferent_parameter(void *ptr, unsigned int param) {
+void eacsl_temporal_save_nreferent_parameter(void *ptr, unsigned int param) {
parameter_referents[param].ptr = ptr;
parameter_referents[param].temporal_flow = TReferentN;
}
-void temporal_save_copy_parameter(void *ptr, unsigned int param) {
+void eacsl_temporal_save_copy_parameter(void *ptr, unsigned int param) {
parameter_referents[param].ptr = ptr;
parameter_referents[param].temporal_flow = TCopy;
}
-void temporal_pull_parameter(void *ptr, unsigned int param, size_t size) {
+void eacsl_temporal_pull_parameter(void *ptr, unsigned int param, size_t size) {
struct temporal_parameter *tpar = ¶meter_referents[param];
switch(tpar->temporal_flow) {
case TBlockN:
@@ -87,36 +87,36 @@ void temporal_pull_parameter(void *ptr, unsigned int param, size_t size) {
store_temporal_referent(ptr, referent_timestamp(tpar->ptr));
break;
case TCopy:
- temporal_memcpy(ptr, tpar->ptr, size);
+ eacsl_temporal_memcpy(ptr, tpar->ptr, size);
break;
default:
private_assert(0, "Unreachable", NULL);
}
}
-void temporal_reset_parameters() {
+void eacsl_temporal_reset_parameters() {
reset_parameter_referents();
}
/* }}} */
/* Return values {{{ */
-void temporal_save_return(void *ptr) {
+void eacsl_temporal_save_return(void *ptr) {
return_referent = (ptr, sizeof(void*)) ? referent_timestamp(ptr) : 0;
}
-void temporal_pull_return(void *ptr) {
+void eacsl_temporal_pull_return(void *ptr) {
store_temporal_referent(ptr, return_referent);
}
-void temporal_reset_return() {
+void eacsl_temporal_reset_return() {
return_referent = 0;
}
/* }}} */
/* Temporal valid {{{ */
int temporal_valid(void *ptr, void *addr_of_ptr) {
- /* Could check for NULL, but since temporal_valid if ran by `valid`, this
- * has been already checked.
+ /* Could check for NULL, but since temporal_valid if ran by `eacsl_valid`,
+ * this has been already checked.
* FIXME: If the address of pointer and the pointer itself reference the same
* address the access is deemed temporally valid by default.
* One issue associated with such checking is the case when a pointer points
diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h
index 37ea0f3a6be..33b822d9d9d 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_temporal.h
@@ -33,31 +33,31 @@
/* No need to encapsulate via ifdef: using these extra definitions does
not hurt, otherwise need to pass additional parameters to frama-c */
-#define temporal_store_nblock export_alias(temporal_store_nblock)
-#define temporal_store_nreferent export_alias(temporal_store_nreferent)
-#define temporal_save_nblock_parameter export_alias(temporal_save_nblock_parameter)
-#define temporal_save_nreferent_parameter export_alias(temporal_save_nreferent_parameter)
-#define temporal_save_copy_parameter export_alias(temporal_save_copy_parameter)
-#define temporal_pull_parameter export_alias(temporal_pull_parameter)
-#define temporal_save_return export_alias(temporal_save_return)
-#define temporal_reset_parameters export_alias(temporal_reset_parameters)
-#define temporal_pull_return export_alias(temporal_pull_return)
-#define temporal_reset_return export_alias(temporal_reset_return)
-#define temporal_memcpy export_alias(temporal_memcpy)
-#define temporal_memset export_alias(temporal_memset)
+#define eacsl_temporal_store_nblock export_alias(temporal_store_nblock)
+#define eacsl_temporal_store_nreferent export_alias(temporal_store_nreferent)
+#define eacsl_temporal_save_nblock_parameter export_alias(temporal_save_nblock_parameter)
+#define eacsl_temporal_save_nreferent_parameter export_alias(temporal_save_nreferent_parameter)
+#define eacsl_temporal_save_copy_parameter export_alias(temporal_save_copy_parameter)
+#define eacsl_temporal_pull_parameter export_alias(temporal_pull_parameter)
+#define eacsl_temporal_save_return export_alias(temporal_save_return)
+#define eacsl_temporal_reset_parameters export_alias(temporal_reset_parameters)
+#define eacsl_temporal_pull_return export_alias(temporal_pull_return)
+#define eacsl_temporal_reset_return export_alias(temporal_reset_return)
+#define eacsl_temporal_memcpy export_alias(temporal_memcpy)
+#define eacsl_temporal_memset export_alias(temporal_memset)
/* Temporal store {{{ */
/*! \brief Take origin number of a memory block containing `block_addr` and
* store it as a referent number of a pointer given by `ptr_addr`. */
/*@ assigns \nothing; */
-void temporal_store_nblock(void *lhs, void *rhs)
+void eacsl_temporal_store_nblock(void *lhs, void *rhs)
__attribute__((FC_BUILTIN));
-/*! \brief Same as `temporal_store_nblock` but take a referent
+/*! \brief Same as `eacsl_temporal_store_nblock` but take a referent
* number of `block_addr` instead */
/*@ assigns \nothing; */
-void temporal_store_nreferent(void *lhs, void *rhs)
+void eacsl_temporal_store_nreferent(void *lhs, void *rhs)
__attribute__((FC_BUILTIN));
/* }}} */
@@ -67,13 +67,13 @@ void temporal_store_nreferent(void *lhs, void *rhs)
/*! \brief Copy temporal shadow data from [src, src + size] to
* [dest, dest + size]. Counterpart of the memcpy function */
/*@ assigns \nothing; */
-void temporal_memcpy(void *dest, void *src, size_t size)
+void eacsl_temporal_memcpy(void *dest, void *src, size_t size)
__attribute__((FC_BUILTIN));
/*! \brief Set temporal shadow data from [src, src + size] to 0.
* Counterpart of memset the function */
/*@ assigns \nothing; */
-void temporal_memset(void *dest, int c, size_t size)
+void eacsl_temporal_memset(void *dest, int c, size_t size)
__attribute__((FC_BUILTIN));
/* }}} */
@@ -82,30 +82,30 @@ void temporal_memset(void *dest, int c, size_t size)
/*! \brief store struct { .ptr = ptr, .temporal_flow = TBlockN }
* in the global parameter array. */
/*@ assigns \nothing; */
-void temporal_save_nblock_parameter(void *ptr, unsigned int param)
+void eacsl_temporal_save_nblock_parameter(void *ptr, unsigned int param)
__attribute__((FC_BUILTIN));
/*! \brief store struct { .ptr = ptr, .temporal_flow = TReferentN }
* in the global parameter array. */
/*@ assigns \nothing; */
-void temporal_save_nreferent_parameter(void *ptr, unsigned int param)
+void eacsl_temporal_save_nreferent_parameter(void *ptr, unsigned int param)
__attribute__((FC_BUILTIN));
/*! \brief store struct { .ptr = ptr, .temporal_flow = TCopy } in the global
* parameter array. */
/*@ assigns \nothing; */
-void temporal_save_copy_parameter(void *ptr, unsigned int param)
+void eacsl_temporal_save_copy_parameter(void *ptr, unsigned int param)
__attribute__((FC_BUILTIN));
/*! \brief Assign a referent number of `ptr` based on the record in the global
* parameter array at index `param`. */
/*@ assigns \nothing; */
-void temporal_pull_parameter(void *ptr, unsigned int param, size_t size)
+void eacsl_temporal_pull_parameter(void *ptr, unsigned int param, size_t size)
__attribute__((FC_BUILTIN));
/*! \brief Nullify global parameter array */
/*@ assigns \nothing; */
-void temporal_reset_parameters()
+void eacsl_temporal_reset_parameters()
__attribute__((FC_BUILTIN));
/* }}} */
@@ -114,19 +114,19 @@ void temporal_reset_parameters()
/*! \brief Save temporal referent number of `ptr` in a placeholder variable
* tracking the referent number of a function's return. */
/*@ assigns \nothing; */
-void temporal_save_return(void *ptr)
+void eacsl_temporal_save_return(void *ptr)
__attribute__((FC_BUILTIN));
/*! \brief Take a temporal referent stored in the placeholder tracking return
* values as a temporal referent number of `ptr`. */
/*@ assigns \nothing; */
-void temporal_pull_return(void *ptr)
+void eacsl_temporal_pull_return(void *ptr)
__attribute__((FC_BUILTIN));
/*! \brief Nullify a placeholder variable tracking the referent number of a
* function's return. */
/*@ assigns \nothing; */
-void temporal_reset_return()
+void eacsl_temporal_reset_return()
__attribute__((FC_BUILTIN));
/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c
index da258a76512..5855ea8586e 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.c
@@ -33,21 +33,21 @@ struct memory_spaces mem_spaces = {
/* \brief Create two memory spaces, one for RTL and the other for application
memory. This function *SHOULD* be called before any allocations are made
otherwise execution fails */
-void make_memory_spaces(size_t rtl_size, size_t heap_size) {
- mem_spaces.rtl_mspace = create_mspace(rtl_size, 0);
- mem_spaces.heap_mspace = create_mspace(heap_size, 0);
- /* Do not use `mspace_least_addr` here, as it returns the address of the
+void eacsl_make_memory_spaces(size_t rtl_size, size_t heap_size) {
+ mem_spaces.rtl_mspace = eacsl_create_mspace(rtl_size, 0);
+ mem_spaces.heap_mspace = eacsl_create_mspace(heap_size, 0);
+ /* Do not use `eacsl_mspace_least_addr` here, as it returns the address of the
mspace header. */
- mem_spaces.heap_start = (uintptr_t)mspace_malloc(mem_spaces.heap_mspace,1);
+ mem_spaces.heap_start = (uintptr_t)eacsl_mspace_malloc(mem_spaces.heap_mspace,1);
mem_spaces.heap_end = mem_spaces.heap_start + heap_size;
/* Save initial least address of heap memspace. This address is used later
to check whether memspace has been moved. */
- mem_spaces.heap_mspace_least = (uintptr_t)mspace_least_addr(mem_spaces.heap_mspace);
+ mem_spaces.heap_mspace_least = (uintptr_t)eacsl_mspace_least_addr(mem_spaces.heap_mspace);
}
-void destroy_memory_spaces() {
- destroy_mspace(mem_spaces.rtl_mspace);
- destroy_mspace(mem_spaces.heap_mspace);
+void eacsl_destroy_memory_spaces() {
+ eacsl_destroy_mspace(mem_spaces.rtl_mspace);
+ eacsl_destroy_mspace(mem_spaces.heap_mspace);
}
int is_pow_of_2(size_t x) {
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h
index 46eab5f161a..bc38137d8f5 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_malloc.h
@@ -28,8 +28,8 @@
* is split into two mspaces (memory spaces). Memory allocation itself is
* delegated to a slightly customised version of dlmalloc shipped with the
* RTL. The overall pattern is as follows:
- * mspace space = create_mspace(capacity, locks);
- * char *p = mspace_malloc(space, size);
+ * mspace space = eacsl_create_mspace(capacity, locks);
+ * char *p = eacsl_mspace_malloc(space, size);
***************************************************************************/
#ifndef E_ACSL_MALLOC_H
@@ -52,16 +52,17 @@
/*** Mspace initialization {{{ ***/
/************************************************************************/
-#define make_memory_spaces export_alias(make_memory_spaces)
-#define destroy_memory_spaces export_alias(destroy_memory_spaces)
+#define eacsl_make_memory_spaces export_alias(make_memory_spaces)
+#define eacsl_destroy_memory_spaces export_alias(destroy_memory_spaces)
/*! \brief Create two memory spaces, one for RTL and the other for application
memory. This function *SHOULD* be called before any allocations are made
otherwise execution fails */
-void make_memory_spaces(size_t rtl_size, size_t heap_size);
+void eacsl_make_memory_spaces(size_t rtl_size, size_t heap_size);
-/*! \brief Destroy the memory spaces created with `make_memory_spaces()`. */
-void destroy_memory_spaces();
+/*! \brief Destroy the memory spaces created with
+ `eacsl_make_memory_spaces()`. */
+void eacsl_destroy_memory_spaces();
/* }}} */
@@ -70,15 +71,15 @@ void destroy_memory_spaces();
/*** Mspace allocators (from dlmalloc) {{{ ***/
/************************************************************************/
-#define create_mspace export_alias(create_mspace)
-#define destroy_mspace export_alias(destroy_mspace)
-#define mspace_least_addr export_alias(mspace_least_addr)
-#define mspace_malloc export_alias(mspace_malloc)
-#define mspace_free export_alias(mspace_free)
-#define mspace_calloc export_alias(mspace_calloc)
-#define mspace_realloc export_alias(mspace_realloc)
-#define mspace_posix_memalign export_alias(mspace_posix_memalign)
-#define mspace_aligned_alloc export_alias(mspace_aligned_alloc)
+#define eacsl_create_mspace export_alias(create_mspace)
+#define eacsl_destroy_mspace export_alias(destroy_mspace)
+#define eacsl_mspace_least_addr export_alias(mspace_least_addr)
+#define eacsl_mspace_malloc export_alias(mspace_malloc)
+#define eacsl_mspace_free export_alias(mspace_free)
+#define eacsl_mspace_calloc export_alias(mspace_calloc)
+#define eacsl_mspace_realloc export_alias(mspace_realloc)
+#define eacsl_mspace_posix_memalign export_alias(mspace_posix_memalign)
+#define eacsl_mspace_aligned_alloc export_alias(mspace_aligned_alloc)
typedef void* mspace;
@@ -91,15 +92,15 @@ struct memory_spaces {
};
extern struct memory_spaces mem_spaces;
-extern mspace create_mspace(size_t, int);
-extern size_t destroy_mspace(mspace);
-extern void* mspace_malloc(mspace, size_t);
-extern void mspace_free(mspace, void*);
-extern void* mspace_calloc(mspace msp, size_t, size_t);
-extern void* mspace_realloc(mspace msp, void*, size_t);
-extern void* mspace_aligned_alloc(mspace, size_t, size_t);
-extern int mspace_posix_memalign(mspace, void **, size_t, size_t);
-extern void* mspace_least_addr(mspace);
+extern mspace eacsl_create_mspace(size_t, int);
+extern size_t eacsl_destroy_mspace(mspace);
+extern void* eacsl_mspace_malloc(mspace, size_t);
+extern void eacsl_mspace_free(mspace, void*);
+extern void* eacsl_mspace_calloc(mspace msp, size_t, size_t);
+extern void* eacsl_mspace_realloc(mspace msp, void*, size_t);
+extern void* eacsl_mspace_aligned_alloc(mspace, size_t, size_t);
+extern int eacsl_mspace_posix_memalign(mspace, void **, size_t, size_t);
+extern void* eacsl_mspace_least_addr(mspace);
/* }}} */
@@ -110,12 +111,12 @@ extern void* mspace_least_addr(mspace);
/* Used within RTL to override standard allocation */
/* Shortcuts for public allocation functions */
-#define public_malloc(...) mspace_malloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_realloc(...) mspace_realloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_calloc(...) mspace_calloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_free(...) mspace_free(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_aligned_alloc(...) mspace_aligned_alloc(mem_spaces.heap_mspace, __VA_ARGS__)
-#define public_posix_memalign(...) mspace_posix_memalign(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_malloc(...) eacsl_mspace_malloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_realloc(...) eacsl_mspace_realloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_calloc(...) eacsl_mspace_calloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_free(...) eacsl_mspace_free(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_aligned_alloc(...) eacsl_mspace_aligned_alloc(mem_spaces.heap_mspace, __VA_ARGS__)
+#define public_posix_memalign(...) eacsl_mspace_posix_memalign(mem_spaces.heap_mspace, __VA_ARGS__)
/* }}} */
@@ -123,10 +124,10 @@ extern void* mspace_least_addr(mspace);
/*** Private allocators usable within RTL and GMP {{{ ***/
/************************************************************************/
-#define private_malloc(...) mspace_malloc(mem_spaces.rtl_mspace, __VA_ARGS__)
-#define private_calloc(...) mspace_calloc(mem_spaces.rtl_mspace, __VA_ARGS__)
-#define private_realloc(...) mspace_realloc(mem_spaces.rtl_mspace, __VA_ARGS__)
-#define private_free(...) mspace_free(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_malloc(...) eacsl_mspace_malloc(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_calloc(...) eacsl_mspace_calloc(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_realloc(...) eacsl_mspace_realloc(mem_spaces.rtl_mspace, __VA_ARGS__)
+#define private_free(...) eacsl_mspace_free(mem_spaces.rtl_mspace, __VA_ARGS__)
/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c
index d2df8a78b73..ea0945d67dc 100644
--- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c
+++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.c
@@ -884,7 +884,7 @@ static void validate_format
/* }}} */
/* Printf and friends {{{ */
-int builtin_printf(const char *fmtdesc, const char *fmt, ...) {
+int eacsl_builtin_printf(const char *fmtdesc, const char *fmt, ...) {
va_list ap;
va_start(ap, fmt);
validate_format(fmtdesc, fmt, ap, "printf", NULL, 0);
@@ -892,7 +892,7 @@ int builtin_printf(const char *fmtdesc, const char *fmt, ...) {
return vprintf(fmt, ap);
}
-int builtin_fprintf(const char *fmtdesc, FILE *stream, const char *fmt, ...) {
+int eacsl_builtin_fprintf(const char *fmtdesc, FILE *stream, const char *fmt, ...) {
va_list ap;
va_start(ap, fmt);
/* First check that stream belongs to allocated space */
@@ -915,7 +915,7 @@ int builtin_fprintf(const char *fmtdesc, FILE *stream, const char *fmt, ...) {
return vfprintf(stream, fmt, ap);
}
-int builtin_dprintf(const char *fmtdesc, int fd, const char *fmt, ...) {
+int eacsl_builtin_dprintf(const char *fmtdesc, int fd, const char *fmt, ...) {
va_list ap;
va_start(ap, fmt);
/* Make sure that the designated file descriptor is open */
@@ -926,7 +926,7 @@ int builtin_dprintf(const char *fmtdesc, int fd, const char *fmt, ...) {
return vdprintf(fd, fmt, ap);
}
-int builtin_sprintf(const char *fmtdesc, char *buffer, const char *fmt, ...) {
+int eacsl_builtin_sprintf(const char *fmtdesc, char *buffer, const char *fmt, ...) {
va_list ap;
/* Make sure that the buffer has sufficient space to store the result of the
function. Luckily this can be accomplished via `snprintf(buf, n, mfmt,...)`
@@ -945,7 +945,7 @@ int builtin_sprintf(const char *fmtdesc, char *buffer, const char *fmt, ...) {
return vsprintf(buffer, fmt, ap);
}
-int builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
+int eacsl_builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
const char *fmt, ...) {
va_list ap;
va_start(ap, fmt);
@@ -959,7 +959,7 @@ int builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
return vsnprintf(buffer, size, fmt, ap);
}
-int builtin_syslog(const char *fmtdesc, int priority, const char *fmt, ...) {
+int eacsl_builtin_syslog(const char *fmtdesc, int priority, const char *fmt, ...) {
va_list ap;
va_start(ap, fmt);
validate_format(fmtdesc, fmt, ap, "syslog", NULL, 0);
diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h
index 00906c5fd2b..4c65357b62b 100644
--- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h
+++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_stdio.h
@@ -82,38 +82,38 @@
/* No need to encapsulate via ifdef: using these extra definitions does
not hurt, otherwise need to pass additional parameters to frama-c */
-#define builtin_printf export_alias(builtin_printf)
-#define builtin_fprintf export_alias(builtin_fprintf)
-#define builtin_dprintf export_alias(builtin_dprintf)
-#define builtin_sprintf export_alias(builtin_sprintf)
-#define builtin_snprintf export_alias(builtin_snprintf)
-#define builtin_syslog export_alias(builtin_syslog)
+#define eacsl_builtin_printf export_alias(builtin_printf)
+#define eacsl_builtin_fprintf export_alias(builtin_fprintf)
+#define eacsl_builtin_dprintf export_alias(builtin_dprintf)
+#define eacsl_builtin_sprintf export_alias(builtin_sprintf)
+#define eacsl_builtin_snprintf export_alias(builtin_snprintf)
+#define eacsl_builtin_syslog export_alias(builtin_syslog)
/* Printf and friends {{{ */
/** \brief `printf` with error checking. */
-int builtin_printf(const char *fmtdesc, const char *fmt, ...)
+int eacsl_builtin_printf(const char *fmtdesc, const char *fmt, ...)
__attribute__((FC_BUILTIN));
/** \brief `fprintf` with error checking. */
-int builtin_fprintf(const char *fmtdesc, FILE *stream, const char *fmt, ...)
+int eacsl_builtin_fprintf(const char *fmtdesc, FILE *stream, const char *fmt, ...)
__attribute__((FC_BUILTIN));
/** \brief `dprintf` with error checking. */
-int builtin_dprintf(const char *fmtdesc, int fd, const char *fmt, ...)
+int eacsl_builtin_dprintf(const char *fmtdesc, int fd, const char *fmt, ...)
__attribute__((FC_BUILTIN));
/** \brief `sprintf` with error checking. */
-int builtin_sprintf(const char *fmtdesc, char *buffer, const char *fmt, ...)
+int eacsl_builtin_sprintf(const char *fmtdesc, char *buffer, const char *fmt, ...)
__attribute__((FC_BUILTIN));
/** \brief `snprintf` with error checking. */
-int builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
+int eacsl_builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
const char *fmt, ...)
__attribute__((FC_BUILTIN));
/** \brief `syslog` with error checking. */
-int builtin_syslog(const char *fmtdesc, int priority, const char *fmt, ...)
+int eacsl_builtin_syslog(const char *fmtdesc, int priority, const char *fmt, ...)
__attribute__((FC_BUILTIN));
/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c
index 05d54981e64..4ab59ec78ea 100644
--- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c
+++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.c
@@ -36,7 +36,7 @@ long valid_nstring(char *s, long n, int wrtbl) {
if (alc) {
if (wrtbl && readonly(s))
return -2; /* Not writeable */
- long size = block_length(s) - offset(s);
+ long size = eacsl_block_length(s) - eacsl_offset(s);
long i;
for (i = 0; i < size; i++) {
if (s[i] == '\0' || n == i)
@@ -59,7 +59,7 @@ long valid_nwstring(wchar_t *s, long n, int wrtbl) {
if (alc) {
if (wrtbl && readonly(s))
return -2; /* Not writeable */
- long size = (block_length(s) - offset(s))/sizeof(wchar_t);
+ long size = (eacsl_block_length(s) - eacsl_offset(s))/sizeof(wchar_t);
long i;
for (i = 0; i < size; i++) {
if (s[i] == L'\0' || n == i)
@@ -146,11 +146,11 @@ static inline void validate_overlapping_spaces
/*** strlen/strcpy/strcat/strcmp {{{ ***/
/************************************************************************/
-size_t builtin_strlen(const char *s) {
+size_t eacsl_builtin_strlen(const char *s) {
return validate_allocated_string((char*)s, -1, "strlen", "input ");
}
-char *builtin_strcpy(char *dest, const char *src) {
+char *eacsl_builtin_strcpy(char *dest, const char *src) {
// `src` string should be a valid NUL-terminated C string
size_t size =
validate_allocated_string((char*)src, -1, "strlen", "source string ");
@@ -163,7 +163,7 @@ char *builtin_strcpy(char *dest, const char *src) {
return strcpy(dest, src);
}
-char *builtin_strncpy(char *dest, const char *src, size_t n) {
+char *eacsl_builtin_strncpy(char *dest, const char *src, size_t n) {
/* `src` should be a valid string up to `nth` character */
validate_allocated_string((char*)src, n, "strncpy", "source string ");
/* `dest` should be allocated and writeable up to `nth` character */
@@ -173,26 +173,26 @@ char *builtin_strncpy(char *dest, const char *src, size_t n) {
return strncpy(dest, src, n);
}
-int builtin_strcmp(const char *s1, const char *s2) {
+int eacsl_builtin_strcmp(const char *s1, const char *s2) {
/* both strings should be valid NUL-terminated strings */
validate_allocated_string((char*)s1, -1, "strcmp", "string 1 ");
validate_allocated_string((char*)s2, -1, "strcmp", "string 2 ");
return strcmp(s1, s2);
}
-int builtin_strncmp(const char *s1, const char *s2, size_t n) {
+int eacsl_builtin_strncmp(const char *s1, const char *s2, size_t n) {
/* both strings should be valid up to nth character */
validate_allocated_string((char*)s1, n, "strncmp", "string 1 ");
validate_allocated_string((char*)s2, n, "strncmp", "string 2 ");
return strncmp(s1, s2, n);
}
-char *builtin_strcat(char *dest, const char *src) {
+char *eacsl_builtin_strcat(char *dest, const char *src) {
long src_sz =
validate_allocated_string((char*)src, -1, "strcat", "source string ");
long dest_sz =
validate_writeable_string((char*)dest, -1, "strcat", "destination string ");
- size_t avail_sz = block_length(dest) - offset(dest);
+ size_t avail_sz = eacsl_block_length(dest) - eacsl_offset(dest);
if (!(avail_sz >= src_sz + dest_sz + 1)) {
private_abort("strcat: insufficient space in destination string, "
"available: %lu bytes, requires at least %lu bytes\n",
@@ -203,11 +203,11 @@ char *builtin_strcat(char *dest, const char *src) {
return strcat(dest, src);
}
-char *builtin_strncat(char *dest, const char *src, size_t n) {
+char *eacsl_builtin_strncat(char *dest, const char *src, size_t n) {
validate_allocated_string((char*)src, n, "strncat", "source string ");
long dest_sz =
validate_writeable_string((char*)dest, -1, "strcat", "destination string ");
- size_t avail_sz = block_length(dest) - offset(dest);
+ size_t avail_sz = eacsl_block_length(dest) - eacsl_offset(dest);
if (!(avail_sz >= n + dest_sz + 1)) {
private_abort("strncat: insufficient space in destination string, "
"available: %lu bytes, requires at least %lu bytes\n",
@@ -223,26 +223,26 @@ char *builtin_strncat(char *dest, const char *src, size_t n) {
/*** memcpy/memcmp/memset/memmove {{{ ***/
/************************************************************************/
-void *builtin_memcpy(void *dest, const void *src, size_t n) {
+void *eacsl_builtin_memcpy(void *dest, const void *src, size_t n) {
validate_allocated_space((void*)src, n, "memcpy", "source space ");
validate_writeable_space((void*)dest, n, "memcpy", "destination space ");
validate_overlapping_spaces((uintptr_t)src, n, (uintptr_t)dest, n, "memcpy");
return memcpy(dest, src, n);
}
-void *builtin_memset(void *s, int c, size_t n) {
+void *eacsl_builtin_memset(void *s, int c, size_t n) {
validate_writeable_space((void*)s, n, "memset", "space ");
return memset(s, c, n);
}
-int builtin_memcmp(const void *s1, const void *s2, size_t n) {
+int eacsl_builtin_memcmp(const void *s1, const void *s2, size_t n) {
validate_allocated_space((void*)s1, n, "memcmp", "space 1 ");
validate_allocated_space((void*)s2, n, "memcmp", "space 1 ");
validate_overlapping_spaces((uintptr_t)s1, n, (uintptr_t)s2, n, "memcpy");
return memcmp(s1, s2, n);
}
-void *builtin_memmove(void *dest, const void *src, size_t n) {
+void *eacsl_builtin_memmove(void *dest, const void *src, size_t n) {
validate_allocated_space((void*)src, n, "memcmp", "source space ");
validate_writeable_space((void*)dest, n, "memcmp", "destination space ");
return memmove(dest, src, n);
diff --git a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h
index e1bb8fdb9a1..c7f28670449 100644
--- a/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h
+++ b/src/plugins/e-acsl/share/e-acsl/libc_replacements/e_acsl_string.h
@@ -33,18 +33,17 @@
#include "../internals/e_acsl_alias.h"
-#define builtin_strlen export_alias(builtin_strlen)
-#define builtin_strcpy export_alias(builtin_strcpy)
-#define builtin_strncpy export_alias(builtin_strncpy)
-#define builtin_strcat export_alias(builtin_strcat)
-#define builtin_strncat export_alias(builtin_strncat)
-#define builtin_strncat export_alias(builtin_strncat)
-#define builtin_strcmp export_alias(builtin_strcmp)
-#define builtin_strncmp export_alias(builtin_strncmp)
-#define builtin_memcpy export_alias(builtin_memcpy)
-#define builtin_memset export_alias(builtin_memset)
-#define builtin_memcmp export_alias(builtin_memcmp)
-#define builtin_memmove export_alias(builtin_memmove)
+#define eacsl_builtin_strlen export_alias(builtin_strlen)
+#define eacsl_builtin_strcpy export_alias(builtin_strcpy)
+#define eacsl_builtin_strncpy export_alias(builtin_strncpy)
+#define eacsl_builtin_strcat export_alias(builtin_strcat)
+#define eacsl_builtin_strncat export_alias(builtin_strncat)
+#define eacsl_builtin_strcmp export_alias(builtin_strcmp)
+#define eacsl_builtin_strncmp export_alias(builtin_strncmp)
+#define eacsl_builtin_memcpy export_alias(builtin_memcpy)
+#define eacsl_builtin_memset export_alias(builtin_memset)
+#define eacsl_builtin_memcmp export_alias(builtin_memcmp)
+#define eacsl_builtin_memmove export_alias(builtin_memmove)
/************************************************************************/
/*** Support functionality {{{ ***/
@@ -101,45 +100,45 @@ int disjoint_spaces(uintptr_t s1, size_t s1_sz, uintptr_t s2, size_t s2_sz);
/* drop-in replacement for `strlen` */
/*@ assigns \result \from s[0..]; */
-size_t builtin_strlen(const char *s)
+size_t eacsl_builtin_strlen(const char *s)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `strcpy` */
/*@ assigns dest[0..] \from src[0..];
@ assigns \result \from dest;
@ ensures \result == dest; */
-char *builtin_strcpy(char *dest, const char *src)
+char *eacsl_builtin_strcpy(char *dest, const char *src)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `strncpy` */
/*@ assigns dest[0..n - 1] \from src[0..n-1];
@ assigns \result \from dest;
@ ensures \result == dest; */
-char *builtin_strncpy(char *dest, const char *src, size_t n)
+char *eacsl_builtin_strncpy(char *dest, const char *src, size_t n)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `strcmp` */
/*@ assigns \result \from s1[0..], s2[0..]; */
-int builtin_strcmp(const char *s1, const char *s2)
+int eacsl_builtin_strcmp(const char *s1, const char *s2)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `strncmp` */
/*@ assigns \result \from s1[0..n-1], s2[0..n-1]; */
-int builtin_strncmp(const char *s1, const char *s2, size_t n)
+int eacsl_builtin_strncmp(const char *s1, const char *s2, size_t n)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `strcat` */
/*@ assigns dest[..] \from src[0..];
@ assigns \result \from dest;
@ ensures \result == dest; */
-char *builtin_strcat(char *dest, const char *src)
+char *eacsl_builtin_strcat(char *dest, const char *src)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `strncat` */
/*@ assigns dest[..] \from src[0..n];
@ assigns \result \from dest;
@ ensures \result == dest; */
-char *builtin_strncat(char *dest, const char *src, size_t n)
+char *eacsl_builtin_strncat(char *dest, const char *src, size_t n)
__attribute__((FC_BUILTIN));
/* }}} */
@@ -151,26 +150,26 @@ char *builtin_strncat(char *dest, const char *src, size_t n)
/*@ assigns ((char*)dest)[0..n-1] \from ((char*)src)[0..n-1];
@ assigns \result \from dest;
@ ensures \result == dest; */
-void *builtin_memcpy(void *dest, const void *src, size_t n)
+void *eacsl_builtin_memcpy(void *dest, const void *src, size_t n)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `memset` */
/*@ assigns ((char*)s)[0..n-1] \from c;
@ assigns \result \from s;
@ ensures \result == s; */
-void *builtin_memset(void *s, int c, size_t n)
+void *eacsl_builtin_memset(void *s, int c, size_t n)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `memcmp` */
/*@ assigns \result \from ((char*)s1)[0..n-1], ((char*)s2)[0..n-1]; */
-int builtin_memcmp(const void *s1, const void *s2, size_t n)
+int eacsl_builtin_memcmp(const void *s1, const void *s2, size_t n)
__attribute__((FC_BUILTIN));
/* drop-in replacement for `memmove` */
/*@ assigns ((char*)dest)[0..n-1] \from ((char*)src)[0..n-1];
@ assigns \result \from dest;
@ ensures \result == dest; */
-void *builtin_memmove(void *dest, const void *src, size_t n)
+void *eacsl_builtin_memmove(void *dest, const void *src, size_t n)
__attribute__((FC_BUILTIN));
/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c
index 5f36c078a23..e357b4b942a 100644
--- a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c
+++ b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.c
@@ -29,20 +29,20 @@
#include "e_acsl_floating_point.h"
// Initialization
-double math_HUGE_VAL = 0.0;
-float math_HUGE_VALF = 0.0;
-double math_INFINITY = 0.0;
+double eacsl_math_HUGE_VAL = 0.0;
+float eacsl_math_HUGE_VALF = 0.0;
+double eacsl_math_INFINITY = 0.0;
void init_infinity_values() {
/* Initialize E-ACSL infinity values */
- math_HUGE_VAL = HUGE_VAL;
- math_HUGE_VALF = HUGE_VALF;
- math_INFINITY = INFINITY;
+ eacsl_math_HUGE_VAL = HUGE_VAL;
+ eacsl_math_HUGE_VALF = HUGE_VALF;
+ eacsl_math_INFINITY = INFINITY;
/* Clear exceptions buffers */
feclearexcept(FE_ALL_EXCEPT);
}
-void floating_point_exception(const char *exp) {
+void eacsl_floating_point_exception(const char *exp) {
int except = fetestexcept(FE_ALL_EXCEPT);
char *resp = NULL;
if (except) {
diff --git a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h
index f9023747544..41a3e44e04e 100644
--- a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h
+++ b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_floating_point.h
@@ -30,10 +30,10 @@
#include "../internals/e_acsl_alias.h"
-#define math_HUGE_VAL export_alias(math_HUGE_VAL)
-#define math_HUGE_VALF export_alias(math_HUGE_VALF)
-#define math_INFINITY export_alias(math_INFINITY)
-#define floating_point_exception export_alias(floating_point_exception)
+#define eacsl_math_HUGE_VAL export_alias(math_HUGE_VAL)
+#define eacsl_math_HUGE_VALF export_alias(math_HUGE_VALF)
+#define eacsl_math_INFINITY export_alias(math_INFINITY)
+#define eacsl_floating_point_exception export_alias(floating_point_exception)
/* Below variables hold infinity values for floating points defined in math.h.
Most of them are defined as macros that expand to built-in function calls.
@@ -50,13 +50,13 @@
*/
/** \brief Positive infinity for doubles: same as HUGE_VAL */
-extern double math_HUGE_VAL
+extern double eacsl_math_HUGE_VAL
__attribute__((FC_BUILTIN));
/** \brief Positive infinity for floats: same as HUGE_VALF */
-extern float math_HUGE_VALF
+extern float eacsl_math_HUGE_VALF
__attribute__((FC_BUILTIN));
/** \brief Representation of infinity value for doubles: same as INFINITY */
-extern double math_INFINITY
+extern double eacsl_math_INFINITY
__attribute__((FC_BUILTIN));
/* FIXME: An additional variable that should be added to this list is
@@ -67,7 +67,7 @@ extern double math_INFINITY
void init_infinity_values();
-void floating_point_exception(const char *exp)
+void eacsl_floating_point_exception(const char *exp)
__attribute__((FC_BUILTIN));
#endif // E_ACSL_FLOATING_POINT_H
diff --git a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h
index f7df545a7bf..aea944fa618 100644
--- a/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/numerical_model/e_acsl_gmp_api.h
@@ -36,36 +36,36 @@
#include <stddef.h>
#include "../internals/e_acsl_alias.h"
-#define mpz_struct export_alias(mpz_struct)
-#define mpz_t export_alias(mpz_t)
-#define mpq_struct export_alias(mpq_struct)
-#define mpq_t export_alias(mpq_t)
-#define mp_bitcnt_t export_alias(mp_bitcnt_t)
+#define eacsl_mpz_struct export_alias(mpz_struct)
+#define eacsl_mpz_t export_alias(mpz_t)
+#define eacsl_mpq_struct export_alias(mpq_struct)
+#define eacsl_mpq_t export_alias(mpq_t)
+#define eacsl_mp_bitcnt_t export_alias(mp_bitcnt_t)
-struct mpz_struct {
+struct eacsl_mpz_struct {
int _mp_alloc;
int _mp_size;
unsigned long *_mp_d;
};
-typedef struct mpz_struct mpz_struct;
-typedef mpz_struct (__attribute__((__FC_BUILTIN__)) mpz_t)[1];
+typedef struct eacsl_mpz_struct eacsl_mpz_struct;
+typedef eacsl_mpz_struct (__attribute__((__FC_BUILTIN__)) eacsl_mpz_t)[1];
-struct mpq_struct {
- mpz_struct _mp_num;
- mpz_struct _mp_den;
+struct eacsl_mpq_struct {
+ eacsl_mpz_struct _mp_num;
+ eacsl_mpz_struct _mp_den;
};
-typedef struct mpq_struct mpq_struct;
-typedef mpq_struct (__attribute__((__FC_BUILTIN__)) mpq_t)[1];
+typedef struct eacsl_mpq_struct eacsl_mpq_struct;
+typedef eacsl_mpq_struct (__attribute__((__FC_BUILTIN__)) eacsl_mpq_t)[1];
/**
* Counts of bits of a multi-precision number are represented in the C type
- * mp_bitcnt_t. Currently this is always an unsigned long, but on some systems
- * it will be an unsigned long long in the future.
+ * eacsl_mp_bitcnt_t. Currently this is always an unsigned long, but on some
+ * systems it will be an unsigned long long in the future.
* @see https://gmplib.org/manual/Nomenclature-and-Types#Nomenclature-and-Types
*/
-typedef unsigned long int mp_bitcnt_t;
+typedef unsigned long int eacsl_mp_bitcnt_t;
/****************/
/* Initializers */
@@ -77,14 +77,14 @@ typedef unsigned long int mp_bitcnt_t;
@ ensures \valid(z);
@ allocates z;
@ assigns *z \from __e_acsl_init; */
-extern void __gmpz_init(mpz_t z)
+extern void __gmpz_init(eacsl_mpz_t z)
__attribute__((FC_BUILTIN));
/*@ requires ! \initialized(q);
@ ensures \valid(q);
@ allocates q;
@ assigns *q \from __e_acsl_init; */
-extern void __gmpq_init(mpq_t q)
+extern void __gmpq_init(eacsl_mpq_t q)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(z_orig);
@@ -93,7 +93,7 @@ extern void __gmpq_init(mpq_t q)
@ ensures \valid(z);
// @ ensures z->n == z_orig->n;
@ assigns *z \from *z_orig; */
-extern void __gmpz_init_set(mpz_t z, const mpz_t z_orig)
+extern void __gmpz_init_set(eacsl_mpz_t z, const eacsl_mpz_t z_orig)
__attribute__((FC_BUILTIN));
/*@ requires ! \initialized(z);
@@ -102,7 +102,7 @@ extern void __gmpz_init_set(mpz_t z, const mpz_t z_orig)
@ ensures \initialized(z);
// @ ensures z->n == n;
@ assigns *z \from n; */
-extern void __gmpz_init_set_ui(mpz_t z, unsigned long int n)
+extern void __gmpz_init_set_ui(eacsl_mpz_t z, unsigned long int n)
__attribute__((FC_BUILTIN));
/*@ requires ! \initialized(z);
@@ -111,7 +111,7 @@ extern void __gmpz_init_set_ui(mpz_t z, unsigned long int n)
@ ensures \initialized(z);
// @ ensures z->n == n;
@ assigns *z \from n; */
-extern void __gmpz_init_set_si(mpz_t z, signed long int n)
+extern void __gmpz_init_set_si(eacsl_mpz_t z, signed long int n)
__attribute__((FC_BUILTIN));
/*@ requires ! \initialized(z);
@@ -120,7 +120,7 @@ extern void __gmpz_init_set_si(mpz_t z, signed long int n)
@ ensures \initialized(z);
@ assigns *z \from str[0..],base;
@ assigns \result \from str[0..],base; */
-extern int __gmpz_init_set_str(mpz_t z, const char *str, int base)
+extern int __gmpz_init_set_str(eacsl_mpz_t z, const char *str, int base)
__attribute__((FC_BUILTIN));
/*@ requires ! \initialized(z);
@@ -128,7 +128,7 @@ extern int __gmpz_init_set_str(mpz_t z, const char *str, int base)
@ ensures \valid(z);
@ ensures \initialized(z);
@ assigns *z \from base; */
-extern void __gmpz_import (mpz_t z, size_t, int, size_t, int, size_t, const void *base)
+extern void __gmpz_import (eacsl_mpz_t z, size_t, int, size_t, int, size_t, const void *base)
__attribute__((FC_BUILTIN));
/***************/
@@ -139,34 +139,34 @@ extern void __gmpz_import (mpz_t z, size_t, int, size_t, int, size_t, const void
@ requires \valid(z);
// @ ensures z->n == z_orig->n;
@ assigns *z \from *z_orig; */
-extern void __gmpz_set(mpz_t z, const mpz_t z_orig)
+extern void __gmpz_set(eacsl_mpz_t z, const eacsl_mpz_t z_orig)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(q_orig);
@ requires \valid(q);
@ assigns *q \from *q_orig; */
-extern void __gmpq_set(mpq_t q, const mpq_t q_orig)
+extern void __gmpq_set(eacsl_mpq_t q, const eacsl_mpq_t q_orig)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q);
@ assigns *q \from d; */
-extern void __gmpq_set_d(mpq_t q, double d)
+extern void __gmpq_set_d(eacsl_mpq_t q, double d)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q);
@ assigns *q \from n,d; */
-extern void __gmpq_set_ui(mpq_t q, unsigned long int n, unsigned long int d)
+extern void __gmpq_set_ui(eacsl_mpq_t q, unsigned long int n, unsigned long int d)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q);
@ assigns *q \from n,d; */
-extern void __gmpq_set_si(mpq_t q, signed long int n, unsigned long int d)
+extern void __gmpq_set_si(eacsl_mpq_t q, signed long int n, unsigned long int d)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(z_orig);
@ requires \valid(q);
@ assigns *q \from *z_orig; */
-extern void __gmpq_set_z(mpq_t q, const mpz_t z_orig)
+extern void __gmpq_set_z(eacsl_mpq_t q, const eacsl_mpz_t z_orig)
__attribute__((FC_BUILTIN));
/*@ allocates q;
@@ -174,24 +174,24 @@ extern void __gmpq_set_z(mpq_t q, const mpz_t z_orig)
@ ensures \initialized(q);
@ assigns *q \from str[0..],base;
@ assigns \result \from str[0..],base; */
-extern int __gmpq_set_str(mpq_t q, const char *str, int base)
+extern int __gmpq_set_str(eacsl_mpq_t q, const char *str, int base)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z);
@ assigns *z \from n; */
-extern void __gmpz_set_ui(mpz_t z, unsigned long int n)
+extern void __gmpz_set_ui(eacsl_mpz_t z, unsigned long int n)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z);
// @ ensures z->n == n;
@ assigns *z \from n; */
-extern void __gmpz_set_si(mpz_t z, signed long int n)
+extern void __gmpz_set_si(eacsl_mpz_t z, signed long int n)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(q_orig);
@ requires \valid(z);
@ assigns *z \from *q_orig; */
-extern void __gmpz_set_q(mpz_t z, const mpq_t q_orig)
+extern void __gmpz_set_q(eacsl_mpz_t z, const eacsl_mpq_t q_orig)
__attribute__((FC_BUILTIN));
/*************/
@@ -201,13 +201,13 @@ extern void __gmpz_set_q(mpz_t z, const mpq_t q_orig)
/*@ requires \valid(x);
// @ frees x;
@ assigns *x \from *x; */
-extern void __gmpz_clear(mpz_t x)
+extern void __gmpz_clear(eacsl_mpz_t x)
__attribute__((FC_BUILTIN));
/*@ requires \valid(x);
// @ frees x;
@ assigns *x \from *x; */
-extern void __gmpq_clear(mpq_t x)
+extern void __gmpq_clear(eacsl_mpq_t x)
__attribute__((FC_BUILTIN));
/********************/
@@ -217,13 +217,13 @@ extern void __gmpq_clear(mpq_t x)
/*@ requires \valid_read(z1);
@ requires \valid_read(z2);
@ assigns \result \from *z1, *z2; */
-extern int __gmpz_cmp(const mpz_t z1, const mpz_t z2)
+extern int __gmpz_cmp(const eacsl_mpz_t z1, const eacsl_mpz_t z2)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(q1);
@ requires \valid_read(q2);
@ assigns \result \from *q1, *q2; */
-extern int __gmpq_cmp(const mpq_t q1, const mpq_t q2)
+extern int __gmpq_cmp(const eacsl_mpq_t q1, const eacsl_mpq_t q2)
__attribute__((FC_BUILTIN));
/************************/
@@ -233,82 +233,82 @@ extern int __gmpq_cmp(const mpq_t q1, const mpq_t q2)
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ assigns *z1 \from *z2; */
-extern void __gmpz_neg(mpz_t z1, const mpz_t z2)
+extern void __gmpz_neg(eacsl_mpz_t z1, const eacsl_mpz_t z2)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_add(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_add(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q1);
@ requires \valid_read(q2);
@ requires \valid_read(q3);
@ assigns *q1 \from *q2, *q3; */
-extern void __gmpq_add(mpq_t q1, const mpq_t q2, const mpq_t q3)
+extern void __gmpq_add(eacsl_mpq_t q1, const eacsl_mpq_t q2, const eacsl_mpq_t q3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_sub(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_sub(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q1);
@ requires \valid_read(q2);
@ requires \valid_read(q3);
@ assigns *q1 \from *q2, *q3; */
-extern void __gmpq_sub(mpq_t q1, const mpq_t q2, const mpq_t q3)
+extern void __gmpq_sub(eacsl_mpq_t q1, const eacsl_mpq_t q2, const eacsl_mpq_t q3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_mul(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ assigns *z1 \from *z2, n; */
-extern void __gmpz_mul_2exp(mpz_t z1, const mpz_t z2, mp_bitcnt_t n)
+extern void __gmpz_mul_2exp(eacsl_mpz_t z1, const eacsl_mpz_t z2, eacsl_mp_bitcnt_t n)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q1);
@ requires \valid_read(q2);
@ requires \valid_read(q3);
@ assigns *q1 \from *q2, *q3; */
-extern void __gmpq_mul(mpq_t q1, const mpq_t q2, const mpq_t q3)
+extern void __gmpq_mul(eacsl_mpq_t q1, const eacsl_mpq_t q2, const eacsl_mpq_t q3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_tdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_tdiv_q(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_tdiv_r(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ assigns *z1 \from *z2, n; */
-extern void __gmpz_tdiv_q_2exp(mpz_t z1, const mpz_t z2, mp_bitcnt_t n)
+extern void __gmpz_tdiv_q_2exp(eacsl_mpz_t z1, const eacsl_mpz_t z2, eacsl_mp_bitcnt_t n)
__attribute__((FC_BUILTIN));
/*@ requires \valid(q1);
@ requires \valid_read(q2);
@ requires \valid_read(q3);
@ assigns *q1 \from *q2, *q3; */
-extern void __gmpq_div(mpq_t q1, const mpq_t q2, const mpq_t q3)
+extern void __gmpq_div(eacsl_mpq_t q1, const eacsl_mpq_t q2, const eacsl_mpq_t q3)
__attribute__((FC_BUILTIN));
/*********************/
@@ -319,28 +319,28 @@ extern void __gmpq_div(mpq_t q1, const mpq_t q2, const mpq_t q3)
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_and(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_and(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_ior(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_ior(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ requires \valid_read(z3);
@ assigns *z1 \from *z2, *z3; */
-extern void __gmpz_xor(mpz_t z1, const mpz_t z2, const mpz_t z3)
+extern void __gmpz_xor(eacsl_mpz_t z1, const eacsl_mpz_t z2, const eacsl_mpz_t z3)
__attribute__((FC_BUILTIN));
/*@ requires \valid(z1);
@ requires \valid_read(z2);
@ assigns *z1 \from *z2;
@ assigns \result \from *z1,*z2; */
-extern int __gmpz_com(mpz_t z1, const mpz_t z2)
+extern int __gmpz_com(eacsl_mpz_t z1, const eacsl_mpz_t z2)
__attribute__((FC_BUILTIN));
/************************/
@@ -350,28 +350,28 @@ extern int __gmpz_com(mpz_t z1, const mpz_t z2)
/** Return non-zero iff the value of z fits in an unsigned long */
/*@ requires \valid_read(z);
@ assigns \result \from *z; */
-extern int __gmpz_fits_ulong_p(const mpz_t z)
+extern int __gmpz_fits_ulong_p(const eacsl_mpz_t z)
__attribute__((FC_BUILTIN));
/** Return non-zero iff the value of z fits in a signed long */
/*@ requires \valid_read(z);
@ assigns \result \from *z; */
-extern int __gmpz_fits_slong_p(const mpz_t z)
+extern int __gmpz_fits_slong_p(const eacsl_mpz_t z)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(z);
@ assigns \result \from *z; */
-extern long __gmpz_get_si(const mpz_t z)
+extern long __gmpz_get_si(const eacsl_mpz_t z)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(q);
@ assigns \result \from *q; */
-extern double __gmpq_get_d(const mpq_t q)
+extern double __gmpq_get_d(const eacsl_mpq_t q)
__attribute__((FC_BUILTIN));
/*@ requires \valid_read(z);
@ assigns \result \from *z; */
-extern unsigned long __gmpz_get_ui(const mpz_t z)
+extern unsigned long __gmpz_get_ui(const eacsl_mpz_t z)
__attribute__((FC_BUILTIN));
#endif
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
index 5492782fdd0..1ca2b8df284 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
@@ -432,7 +432,7 @@ static void bt_clean () {
/* DEBUG */
/*********************/
#ifdef E_ACSL_DEBUG
-static void bt_print_block(bt_block * ptr) {
+static void eacsl_bt_print_block(bt_block * ptr) {
if (ptr != NULL) {
DLOG("%a; %lu Bytes; %slitteral; [init] : %d ",
(char*)ptr->ptr, ptr->size,
@@ -453,7 +453,7 @@ static void bt_print_node(bt_node * ptr, int depth) {
for(i = 0; i < depth; i++)
DLOG(" ");
if(ptr->is_leaf)
- bt_print_block(ptr->leaf);
+ eacsl_bt_print_block(ptr->leaf);
else {
DLOG("%p -- %p\n", (void*)ptr->mask, (void*)ptr->addr);
bt_print_node(ptr->left, depth+1);
@@ -461,7 +461,7 @@ static void bt_print_node(bt_node * ptr, int depth) {
}
}
-static void bt_print_tree() {
+static void eacsl_bt_print_tree() {
DLOG("------------DEBUG\n");
bt_print_node(bt_root, 0);
DLOG("-----------------\n");
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
index ed2c18bc0c4..8ea10c63c71 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
@@ -89,7 +89,7 @@ static void bt_clean_block(bt_block *b);
#ifdef E_ACSL_DEBUG
/*! \brief Print information about a given block */
-static void bt_print_block(bt_block *b);
+static void eacsl_bt_print_block(bt_block *b);
/*! \brief Recursively print the contents of the bittree starting from a
* given node */
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
index 70b77c7a4a6..b48e6e1866f 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
@@ -39,11 +39,11 @@
/* Public API {{{ */
/* Debug */
#ifdef E_ACSL_DEBUG
-# define bt_print_block export_alias(bt_print_block)
-# define bt_print_tree export_alias(bt_print_tree)
-# define block_info export_alias(block_info)
-# define store_block_debug export_alias(store_block_debug)
-# define delete_block_debug export_alias(delete_block_debug)
+# define eacsl_bt_print_block export_alias(bt_print_block)
+# define eacsl_bt_print_tree export_alias(bt_print_tree)
+# define eacsl_block_info export_alias(block_info)
+# define eacsl_store_block_debug export_alias(store_block_debug)
+# define eacsl_delete_block_debug export_alias(delete_block_debug)
#endif
/* }}} */
@@ -85,7 +85,7 @@ static struct current_location {
/**************************/
/* mark the size bytes of ptr as initialized */
-void initialize (void * ptr, size_t size) {
+void eacsl_initialize (void * ptr, size_t size) {
bt_block * tmp;
if(!ptr)
return;
@@ -135,7 +135,7 @@ void initialize (void * ptr, size_t size) {
}
/* mark all bytes of ptr as initialized */
-void full_init (void * ptr) {
+void eacsl_full_init (void * ptr) {
bt_block * tmp;
if (ptr == NULL)
return;
@@ -152,7 +152,7 @@ void full_init (void * ptr) {
}
/* mark a block as read-only */
-void mark_readonly(void * ptr) {
+void eacsl_mark_readonly(void * ptr) {
bt_block * tmp;
if (ptr == NULL)
return;
@@ -167,7 +167,7 @@ void mark_readonly(void * ptr) {
/* PREDICATES {{{ */
/**************************/
-int freeable(void* ptr) {
+int eacsl_freeable(void* ptr) {
bt_block * tmp;
if(ptr == NULL)
return 0;
@@ -178,7 +178,7 @@ int freeable(void* ptr) {
}
/* return whether the size bytes of ptr are initialized */
-int initialized(void * ptr, size_t size) {
+int eacsl_initialized(void * ptr, size_t size) {
unsigned i;
bt_block * tmp = bt_find(ptr);
if(tmp == NULL)
@@ -191,7 +191,7 @@ int initialized(void * ptr, size_t size) {
if(tmp->init_bytes == tmp->size)
return 1;
- /* see implementation of function `initialize` for details */
+ /* see implementation of function `eacsl_initialize` for details */
for(i = 0; i < size; i++) {
size_t offset = (uintptr_t)ptr - tmp->ptr + i;
int byte = offset/8;
@@ -203,7 +203,7 @@ int initialized(void * ptr, size_t size) {
}
/** \brief \return the length (in bytes) of the block containing ptr */
-size_t block_length(void* ptr) {
+size_t eacsl_block_length(void* ptr) {
bt_block * blk = bt_find(ptr);
/* Hard failure when un-allocated memory is used */
private_assert(blk != NULL, "\\block_length of unallocated memory", NULL);
@@ -227,7 +227,7 @@ static bt_block* lookup_allocated(void* ptr, size_t size, void *ptr_base) {
}
/* return whether the size bytes of ptr are readable/writable */
-int valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
+int eacsl_valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
bt_block * blk = lookup_allocated(ptr, size, ptr_base);
return
size == 0
@@ -240,7 +240,7 @@ int valid(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
}
/* return whether the size bytes of ptr are readable */
-int valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
+int eacsl_valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
bt_block * blk = lookup_allocated(ptr, size, ptr_base);
return
size == 0
@@ -253,7 +253,7 @@ int valid_read(void* ptr, size_t size, void *ptr_base, void *addrof_base) {
}
/* return the base address of the block containing ptr */
-void* base_addr(void* ptr) {
+void* eacsl_base_addr(void* ptr) {
bt_block * tmp = bt_find(ptr);
private_assert(tmp != NULL, "\\base_addr of unallocated memory", NULL);
return (void*)tmp->ptr;
@@ -274,7 +274,7 @@ size_t offset(void* ptr) {
/* STACK ALLOCATION {{{ */
/* store the block of size bytes starting at ptr, the new block is returned.
* Warning: the return type is implicitly (bt_block*). */
-void* store_block(void *ptr, size_t size) {
+void* eacsl_store_block(void *ptr, size_t size) {
#ifdef E_ACSL_DEBUG
if (ptr == NULL)
private_abort("Attempt to record NULL block");
@@ -284,16 +284,16 @@ void* store_block(void *ptr, size_t size) {
if (exitsing_block) {
private_abort("\nRecording %a [%lu] at %s:%d failed."
" Overlapping block %a [%lu] found at %s:%d\n",
- ptr, size, cloc.file, cloc.line, base_addr(check),
- block_length(check), exitsing_block->file, exitsing_block->line);
+ ptr, size, cloc.file, cloc.line, eacsl_base_addr(check),
+ eacsl_block_length(check), exitsing_block->file, exitsing_block->line);
}
check += size - 1;
exitsing_block = bt_find(check);
if (exitsing_block) {
private_abort("\nRecording %a [%lu] at %d failed."
" Overlapping block %a [%lu] found at %s:%d\n",
- ptr, size, cloc.file, cloc.line, base_addr(check),
- block_length(check), exitsing_block->file, exitsing_block->line);
+ ptr, size, cloc.file, cloc.line, eacsl_base_addr(check),
+ eacsl_block_length(check), exitsing_block->file, exitsing_block->line);
}
}
#endif
@@ -326,7 +326,7 @@ void* store_block(void *ptr, size_t size) {
static void *store_freeable_block(void *ptr, size_t size, int init_bytes) {
bt_block *blk = NULL;
if (ptr) {
- blk = store_block(ptr, size);
+ blk = eacsl_store_block(ptr, size);
blk->is_freeable = 1;
update_heap_allocation(size);
if (init_bytes)
@@ -336,7 +336,7 @@ static void *store_freeable_block(void *ptr, size_t size, int init_bytes) {
}
/* remove the block starting at ptr */
-void delete_block(void *ptr) {
+void eacsl_delete_block(void *ptr) {
#ifdef E_ACSL_DEBUG
/* Make sure the recorded block is not NULL */
if (!ptr)
@@ -360,7 +360,7 @@ void delete_block(void *ptr) {
}
}
-void* store_block_duplicate(void* ptr, size_t size) {
+void* eacsl_store_block_duplicate(void* ptr, size_t size) {
bt_block * tmp = NULL;
if (ptr != NULL) {
bt_block * tmp = bt_lookup(ptr);
@@ -370,9 +370,9 @@ void* store_block_duplicate(void* ptr, size_t size) {
if (tmp->size != size)
private_abort("Attempt to store duplicate block of different length");
#endif
- delete_block(ptr);
+ eacsl_delete_block(ptr);
}
- store_block(ptr, size);
+ eacsl_store_block(ptr, size);
}
return tmp;
}
@@ -528,7 +528,7 @@ void free(void *ptr) {
/******************************/
/* erase the content of the abstract structure */
-void memory_clean() {
+void eacsl_memory_clean() {
bt_clean();
report_heap_leaks();
}
@@ -539,44 +539,44 @@ extern char **environ;
/* add `argv` to the memory model */
static void argv_alloca(int *argc_ref, char *** argv_ref) {
/* Track a top-level containers */
- store_block((void*)argc_ref, sizeof(int));
- store_block((void*)argv_ref, sizeof(char**));
+ eacsl_store_block((void*)argc_ref, sizeof(int));
+ eacsl_store_block((void*)argv_ref, sizeof(char**));
int argc = *argc_ref;
char** argv = *argv_ref;
/* Track argv */
size_t argvlen = (argc + 1)*sizeof(char*);
- store_block(argv, argvlen);
- initialize(argv, (argc + 1)*sizeof(char*));
+ eacsl_store_block(argv, argvlen);
+ eacsl_initialize(argv, (argc + 1)*sizeof(char*));
while (*argv) {
size_t arglen = strlen(*argv) + 1;
- store_block(*argv, arglen);
- initialize(*argv, arglen);
+ eacsl_store_block(*argv, arglen);
+ eacsl_initialize(*argv, arglen);
argv++;
}
#ifdef E_ACSL_TEMPORAL /* Fill temporal shadow */
int i;
argv = *argv_ref;
- temporal_store_nblock(argv_ref, *argv_ref);
+ eacsl_temporal_store_nblock(argv_ref, *argv_ref);
for (i = 0; i < argc; i++)
- temporal_store_nblock(argv + i, *(argv+i));
+ eacsl_temporal_store_nblock(argv + i, *(argv+i));
#endif
while (*environ) {
size_t envlen = strlen(*environ) + 1;
- store_block(*environ, envlen);
- initialize(*environ, envlen);
+ eacsl_store_block(*environ, envlen);
+ eacsl_initialize(*environ, envlen);
environ++;
}
}
-void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
+void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
describe_run();
/* Mspace sizes here are not that relevant as there is no shadowing and
mspaces will grow automatically */
- make_memory_spaces(MB_SZ(64), MB_SZ(64));
+ eacsl_make_memory_spaces(MB_SZ(64), MB_SZ(64));
arch_assert(ptr_size);
initialize_report_file(argc_ref, argv_ref);
/* Tracking program arguments */
@@ -589,9 +589,9 @@ void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
memory_location * loc = get_safe_location(i);
void *addr = (void*)loc->address;
uintptr_t len = loc->length;
- store_block(addr, len);
+ eacsl_store_block(addr, len);
if (loc->is_initialized)
- initialize(addr, len);
+ eacsl_initialize(addr, len);
}
init_infinity_values();
}
@@ -613,9 +613,9 @@ void memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
* The above macros with rewrite of instances of __e_acsl_store_block generating
* origin information of tracked memory blocks.
*/
-void* store_block_debug(char *file, int line, void* ptr, size_t size) {
+void* eacsl_store_block_debug(char *file, int line, void* ptr, size_t size) {
update_cloc(file, line);
- bt_block * res = store_block(ptr, size);
+ bt_block * res = eacsl_store_block(ptr, size);
if (res) {
res->line = line;
res->file = file;
@@ -623,7 +623,7 @@ void* store_block_debug(char *file, int line, void* ptr, size_t size) {
return res;
}
-void delete_block_debug(char *file, int line, void* ptr) {
+void eacsl_delete_block_debug(char *file, int line, void* ptr) {
update_cloc(file, line);
bt_block * tmp = bt_lookup(ptr);
if (!tmp) {
@@ -631,15 +631,15 @@ void delete_block_debug(char *file, int line, void* ptr) {
"Block with base address %a not found in the memory model at %s:%d",
ptr, file, line);
}
- delete_block(ptr);
+ eacsl_delete_block(ptr);
}
/* Debug print of block information */
-void block_info(char *p) {
+void eacsl_block_info(char *p) {
bt_block * res = bt_find(p);
if (res) {
DLOG(" << %a >> %a [%lu] => %lu \n",
- p, base_addr(p), offset(p), block_length(p));
+ p, eacsl_base_addr(p), eacsl_offset(p), eacsl_block_length(p));
} else {
DLOG(" << %a >> not allocated\n", p);
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c
index 12d3a4c02bc..a6d0c2a9d01 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c
@@ -42,7 +42,7 @@ uintptr_t temporal_referent_shadow(void *ptr) {
"referent timestamp on unallocated memory address %a", (uintptr_t)ptr);
private_assert(blk->temporal_shadow != NULL,
"no temporal shadow of block with base address", (uintptr_t)blk->ptr);
- return (uintptr_t)blk->temporal_shadow + offset(ptr);
+ return (uintptr_t)blk->temporal_shadow + eacsl_offset(ptr);
}
uint32_t referent_timestamp(void *ptr) {
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c
index 1737cc9b970..9425108e88b 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.c
@@ -24,10 +24,10 @@
#include "e_acsl_heap.h"
-size_t get_heap_allocation_size(void) {
+size_t eacsl_get_heap_allocation_size(void) {
return get_heap_internal_allocation_size();
}
-size_t get_heap_allocated_blocks(void) {
+size_t eacsl_get_heap_allocated_blocks(void) {
return get_heap_internal_allocated_blocks();
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h
index b3e521c2046..d622c489166 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_heap.h
@@ -31,22 +31,22 @@
#include <stddef.h>
#include "../internals/e_acsl_alias.h"
-#define heap_allocation_size export_alias(heap_allocation_size)
-#define heap_allocated_blocks export_alias(heap_allocated_blocks)
-#define get_heap_allocation_size export_alias(get_heap_allocation_size)
-#define get_heap_allocated_blocks export_alias(get_heap_allocated_blocks)
+#define eacsl_heap_allocation_size export_alias(heap_allocation_size)
+#define eacsl_heap_allocated_blocks export_alias(heap_allocated_blocks)
+#define eacsl_get_heap_allocation_size export_alias(get_heap_allocation_size)
+#define eacsl_get_heap_allocated_blocks export_alias(get_heap_allocated_blocks)
/*! \brief A variable holding the number of bytes in heap application allocation. */
-extern size_t heap_allocation_size;
+extern size_t eacsl_heap_allocation_size;
/*! \brief A variable holding the number of blocks in heap application allocation. */
-extern size_t heap_allocated_blocks;
+extern size_t eacsl_heap_allocated_blocks;
/*! Return the number of bytes in heap application allocation. */
-size_t get_heap_allocation_size()
+size_t eacsl_get_heap_allocation_size()
__attribute__((FC_BUILTIN));
/*! Return the number of blocks in heap application allocation. */
-size_t get_heap_allocated_blocks()
+size_t eacsl_get_heap_allocated_blocks()
__attribute__((FC_BUILTIN));
#endif // E_ACSL_HEAP
\ No newline at end of file
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
index cde04ae3cca..0e413258b36 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.c
@@ -56,7 +56,7 @@ int separated2(void * ptr1, size_t size1, void * ptr2, size_t size2) {
return sep;
}
-int separated(size_t count, ...) {
+int eacsl_separated(size_t count, ...) {
void * ptrs[count];
size_t sizes[count];
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
index 783532dd94c..f55417402c0 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/e_acsl_observation_model.h
@@ -41,28 +41,28 @@
/************************************************************************/
/* Memory state initialization */
-#define memory_init export_alias(memory_init)
-#define memory_clean export_alias(memory_clean)
+#define eacsl_memory_init export_alias(memory_init)
+#define eacsl_memory_clean export_alias(memory_clean)
/* Tracking */
-#define store_block export_alias(store_block)
-#define store_block_duplicate export_alias(store_block_duplicate)
-#define delete_block export_alias(delete_block)
+#define eacsl_store_block export_alias(store_block)
+#define eacsl_store_block_duplicate export_alias(store_block_duplicate)
+#define eacsl_delete_block export_alias(delete_block)
/* Predicates */
-#define offset export_alias(offset)
-#define base_addr export_alias(base_addr)
-#define 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)
-#define separated export_alias(separated)
+#define eacsl_offset export_alias(offset)
+#define eacsl_base_addr export_alias(base_addr)
+#define eacsl_block_length export_alias(block_length)
+#define eacsl_valid_read export_alias(valid_read)
+#define eacsl_valid export_alias(valid)
+#define eacsl_initialized export_alias(initialized)
+#define eacsl_freeable export_alias(freeable)
+#define eacsl_separated export_alias(separated)
/* Block initialization */
-#define mark_readonly export_alias(mark_readonly)
-#define initialize export_alias(initialize)
-#define full_init export_alias(full_init)
+#define eacsl_mark_readonly export_alias(mark_readonly)
+#define eacsl_initialize export_alias(initialize)
+#define eacsl_full_init export_alias(full_init)
/* }}} */
@@ -149,12 +149,12 @@ int posix_memalign(void **memptr, size_t alignment, size_t size)
/*! \brief Initialize memory tracking state.
* Called before any other statement in \p main */
/*@ assigns \nothing; */
-void memory_init(int *argc_ref, char ***argv, size_t ptr_size)
+void eacsl_memory_init(int *argc_ref, char ***argv, size_t ptr_size)
__attribute__((FC_BUILTIN));
/*! \brief Clean-up memory tracking state before a program's termination. */
/*@ assigns \nothing; */
-void memory_clean(void)
+void eacsl_memory_clean(void)
__attribute__((FC_BUILTIN));
/*! \brief Store stack or globally-allocated memory block
@@ -164,10 +164,10 @@ void memory_clean(void)
* \param size size of the tracked block in bytes */
/*@ ensures \result == ptr;
@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size; */
-void * store_block(void * ptr, size_t size)
+void * eacsl_store_block(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
-/*! \brief Same as `store_block`, but first check
+/*! \brief Same as `eacsl_store_block`, but first check
* checks whether a block with a base address given by `ptr` exists in the
* tracked allocation and remove it before storing a new block.
*
@@ -175,30 +175,30 @@ void * store_block(void * ptr, size_t size)
* \param size size of the tracked block in bytes */
/*@ ensures \result == ptr;
@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size; */
-void * store_block_duplicate(void * ptr, size_t size)
+void * eacsl_store_block_duplicate(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/*! \brief Remove a memory block which base address is \p ptr from tracking. */
/*@ assigns \nothing; */
-void delete_block(void * ptr)
+void eacsl_delete_block(void * ptr)
__attribute__((FC_BUILTIN));
/*! \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)
+void eacsl_initialize(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/*! \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)
+void eacsl_full_init(void * ptr)
__attribute__((FC_BUILTIN));
/*! \brief Mark a memory block which start address is given by \p ptr as
* read-only. */
/*@ assigns \nothing; */
-void mark_readonly(void * ptr)
+void eacsl_mark_readonly(void * ptr)
__attribute__((FC_BUILTIN));
/* }}} */
@@ -212,7 +212,7 @@ void mark_readonly(void * ptr)
* 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)
+int eacsl_freeable(void * ptr)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\valid predicate of E-ACSL.
@@ -257,12 +257,12 @@ int freeable(void * ptr)
@ complete behaviors;
@ disjoint behaviors;
@ */
-int valid(void * ptr, size_t size, void *base, void *addrof_base)
+int eacsl_valid(void * ptr, size_t size, void *base, void *addrof_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\valid_read predicate of E-ACSL.
*
- * Same as ::valid except the checked memory locations are only
+ * Same as ::eacsl_valid except the checked memory locations are only
* required to be allocated. */
/*@ assigns \result \from *(((char*)ptr)+(0..size-1)), ptr, size;
@ behavior valid:
@@ -283,7 +283,7 @@ int valid(void * ptr, size_t size, void *base, void *addrof_base)
@ complete behaviors;
@ disjoint behaviors;
@ */
-int valid_read(void * ptr, size_t size, void *base, void *addrof_base)
+int eacsl_valid_read(void * ptr, size_t size, void *base, void *addrof_base)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\base_addr predicate of E-ACSL.
@@ -291,7 +291,7 @@ int valid_read(void * ptr, size_t size, void *base, void *addrof_base)
* by \p ptr */
/*@ ensures \result == \base_addr(ptr);
@ assigns \result \from ptr; */
-void * base_addr(void * ptr)
+void * eacsl_base_addr(void * ptr)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\block_length predicate of E-ACSL.
@@ -299,7 +299,7 @@ void * base_addr(void * ptr)
* address given by \p ptr */
/*@ ensures \result == \block_length(ptr);
@ assigns \result \from ptr; */
-size_t block_length(void * ptr)
+size_t eacsl_block_length(void * ptr)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\offset predicate of E-ACSL.
@@ -307,7 +307,7 @@ size_t block_length(void * ptr)
* it belongs to */
/*@ ensures \result == \offset(ptr);
@ assigns \result \from ptr; */
-size_t offset(void * ptr)
+size_t eacsl_offset(void * ptr)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\initialized predicate of E-ACSL.
@@ -323,7 +323,7 @@ size_t offset(void * ptr)
@ complete behaviors;
@ disjoint behaviors;
@ */
-int initialized(void * ptr, size_t size)
+int eacsl_initialized(void * ptr, size_t size)
__attribute__((FC_BUILTIN));
/*! \brief Implementation of the \b \\separated predicate of E-ACSL.
@@ -344,7 +344,7 @@ int initialized(void * ptr, size_t size)
*/
/*@ assigns \result \from indirect:count;
@ ensures \result == 0 || \result == 1; */
-int separated(size_t count, ...)
+int eacsl_separated(size_t count, ...)
__attribute__((FC_BUILTIN));
/* }}} */
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c
index 39a5efb21a3..b4e6ae48a57 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_heap_tracking.c
@@ -57,8 +57,8 @@ void update_heap_allocation(long size) {
void report_heap_leaks() {
#if defined(E_ACSL_VERBOSE) || defined(E_ACSL_DEBUG)
- size_t size = get_heap_allocation_size();
- size_t blocks = get_heap_allocated_blocks();
+ size_t size = eacsl_get_heap_allocation_size();
+ size_t blocks = eacsl_get_heap_allocated_blocks();
if (size) {
rtl_printf(" *** WARNING: Leaked %lu bytes of heap memory in %ld block%s\n",
size, blocks, (blocks == 1) ? "" : "s");
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
index 88c378a96fb..cb7ce649dea 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
@@ -41,7 +41,7 @@
#include "../internals/e_acsl_timestamp_retrieval.h"
#include "../e_acsl_observation_model.h"
-void * store_block(void *ptr, size_t size) {
+void * eacsl_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. */
@@ -49,22 +49,22 @@ void * store_block(void *ptr, size_t size) {
return ptr;
}
-void delete_block(void *ptr) {
+void eacsl_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);
}
-void * store_block_duplicate(void *ptr, size_t size) {
+void * eacsl_store_block_duplicate(void *ptr, size_t size) {
if (allocated((uintptr_t)ptr, size, (uintptr_t)ptr))
- delete_block(ptr);
+ eacsl_delete_block(ptr);
shadow_alloca(ptr, size);
return ptr;
}
/*! \brief Initialize a chunk of memory given by its start address (`addr`)
* and byte length (`n`). */
-void initialize(void *ptr, size_t n) {
+void eacsl_initialize(void *ptr, size_t n) {
TRY_SEGMENT(
(uintptr_t)ptr,
initialize_heap_region((uintptr_t)ptr, n),
@@ -72,11 +72,11 @@ void initialize(void *ptr, size_t n) {
)
}
-void full_init(void *ptr) {
- initialize(ptr, _block_length(ptr));
+void eacsl_full_init(void *ptr) {
+ eacsl_initialize(ptr, _block_length(ptr));
}
-void mark_readonly(void *ptr) {
+void eacsl_mark_readonly(void *ptr) {
mark_readonly_region((uintptr_t)ptr, _block_length(ptr));
}
@@ -84,7 +84,7 @@ void mark_readonly(void *ptr) {
/* E-ACSL annotations {{{ */
/* ********************** */
-int valid(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
+int eacsl_valid(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
return
size == 0
||
@@ -96,7 +96,7 @@ int valid(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) {
+int eacsl_valid_read(void *ptr, size_t size, void *ptr_base, void *addrof_base) {
return
size == 0
||
@@ -110,7 +110,7 @@ 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. */
-void * base_addr(void *ptr) {
+void * eacsl_base_addr(void *ptr) {
TRY_SEGMENT(ptr,
return (void*)heap_info((uintptr_t)ptr, 'B'),
return (void*)static_info((uintptr_t)ptr, 'B'));
@@ -120,21 +120,21 @@ void * 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. */
-size_t block_length(void *ptr) {
+size_t eacsl_block_length(void *ptr) {
TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'L'),
return static_info((uintptr_t)ptr, 'L'))
return 0;
}
-size_t offset(void *ptr) {
+size_t eacsl_offset(void *ptr) {
TRY_SEGMENT(ptr,
return heap_info((uintptr_t)ptr, 'O'),
return static_info((uintptr_t)ptr, 'O'));
return 0;
}
-int initialized(void *ptr, size_t size) {
+int eacsl_initialized(void *ptr, size_t size) {
uintptr_t addr = (uintptr_t)ptr;
TRY_SEGMENT_WEAK(addr,
return heap_initialized(addr, size),
@@ -185,9 +185,9 @@ static void argv_alloca(int *argc_ref, char *** argv_ref) {
/* Fill temporal shadow */
int i;
argv = *argv_ref;
- temporal_store_nblock(argv_ref, *argv_ref);
+ eacsl_temporal_store_nblock(argv_ref, *argv_ref);
for (i = 0; i < argc; i++)
- temporal_store_nblock(argv + i, *(argv+i));
+ eacsl_temporal_store_nblock(argv + i, *(argv+i));
#endif
while (*environ) {
@@ -213,7 +213,7 @@ void mspaces_init() {
static char already_run = 0;
if (! already_run) {
describe_run();
- make_memory_spaces(64*MB, get_heap_size());
+ eacsl_make_memory_spaces(64*MB, get_heap_size());
/* Allocate and log shadow memory layout of the execution.
Case of the heap, globals and tls. */
init_shadow_layout_heap_global_tls();
@@ -221,7 +221,7 @@ void mspaces_init() {
}
}
-void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
+void eacsl_memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
/* [already_run] avoids reentrancy issue (see Gitlab issue #83),
e.g. in presence of a recursive call to 'main' */
static char already_run = 0;
@@ -255,14 +255,14 @@ void memory_init(int *argc_ref, char *** argv_ref, size_t ptr_size) {
uintptr_t len = loc->length;
shadow_alloca(addr, len);
if (loc->is_initialized)
- initialize(addr, len);
+ eacsl_initialize(addr, len);
}
init_infinity_values();
already_run = 1;
}
}
-void memory_clean(void) {
+void eacsl_memory_clean(void) {
clean_shadow_layout();
report_heap_leaks();
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
index 69192b7b3ce..4a15179f774 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
@@ -534,7 +534,7 @@ static void set_heap_segment(void *ptr, size_t size, size_t alloc_size,
/* Make sure that heap memspace has not been moved. This is likely if
a really large chunk has been requested to be allocated. */
private_assert(mem_spaces.heap_mspace_least ==
- (uintptr_t)mspace_least_addr(mem_spaces.heap_mspace),
+ (uintptr_t)eacsl_mspace_least_addr(mem_spaces.heap_mspace),
"Exceeded heap allocation limit of %luMB -- heap memory space moved. \n",
E_ACSL_HEAP_SIZE);
@@ -643,7 +643,7 @@ void *shadow_copy(const void *ptr, size_t size, int init) {
* block.
*
* NOTE: ::unset_heap_segment assumes that `ptr` is a base address of an
- * allocated heap memory block, i.e., `freeable(ptr)` evaluates to true.
+ * allocated heap memory block, i.e., `eacsl_freeable(ptr)` evaluates to true.
*
* \param ptr - base address of the memory block to be removed from tracking
* \param init - if evaluated to a non-zero value then initialization shadow
@@ -684,7 +684,7 @@ void free(void *ptr) {
}
if (ptr != NULL) { /* NULL is a valid behaviour */
- if (freeable(ptr)) {
+ if (eacsl_freeable(ptr)) {
unset_heap_segment(ptr, 1, "free");
public_free(ptr);
} else {
@@ -705,7 +705,7 @@ void* realloc(void *ptr, size_t size) {
else if (ptr != NULL && size == 0) {
free(ptr);
} else {
- if (freeable(ptr)) { /* ... and can be used as an input to `free` */
+ if (eacsl_freeable(ptr)) { /* ... and can be used as an input to `free` */
size_t alloc_size = ALLOC_SIZE(size);
res = public_realloc(ptr, alloc_size);
DVALIDATE_ALIGNMENT(res);
@@ -823,7 +823,7 @@ int heap_allocated(uintptr_t addr, size_t size, uintptr_t base_ptr) {
return 0;
}
-int freeable(void *ptr) { /* + */
+int eacsl_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))
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
index 828938c53a6..e5eae6834bd 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
@@ -364,7 +364,8 @@ void initialize_static_region(uintptr_t addr, long size);
/*! \brief Mark n bytes starting from the address given by `ptr` as initialized.
* NOTE: This function has many similarities with ::initialize_static_region
* The functionality, however is preferred to be kept separate
- * because the ::mark_readonly should operate only on the global shadow. */
+ * because the ::eacsl_mark_readonly should operate only on the global shadow.
+ */
void mark_readonly_region (uintptr_t addr, long size);
/* }}} */
@@ -400,7 +401,7 @@ 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. */
-int freeable(void *ptr);
+int eacsl_freeable(void *ptr);
/*! \brief Querying information about a specific heap memory address.
* This function is similar to ::static_info except it returns data
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
index 7d627c53486..e070180edfc 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
@@ -118,8 +118,8 @@ void set_shadow_segment(memory_segment *seg, memory_segment *parent,
seg->name = name;
seg->shadow_ratio = ratio;
seg->size = parent->size/seg->shadow_ratio;
- seg->mspace = create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
- seg->start = (uintptr_t)mspace_malloc(seg->mspace,1);
+ seg->mspace = eacsl_create_mspace(seg->size + SHADOW_SEGMENT_PADDING, 0);
+ seg->start = (uintptr_t)eacsl_mspace_malloc(seg->mspace,1);
seg->end = seg->start + seg->size;
seg->shadow_offset = parent->start - seg->start;
}
@@ -212,9 +212,9 @@ void clean_shadow_layout() {
int i;
for (i = 0; i < sizeof(mem_partitions)/sizeof(memory_partition*); i++) {
if (mem_partitions[i]->primary.mspace)
- destroy_mspace(mem_partitions[i]->primary.mspace);
+ eacsl_destroy_mspace(mem_partitions[i]->primary.mspace);
if (mem_partitions[i]->secondary.mspace)
- destroy_mspace(mem_partitions[i]->secondary.mspace);
+ eacsl_destroy_mspace(mem_partitions[i]->secondary.mspace);
}
}
}
--
GitLab