diff --git a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c
index 14c827d425f2b8afa03ebf6202e0d6d83be15c2e..56b394e1620e940d7e18097aa4cf96e0a9044188 100644
--- a/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c
+++ b/src/plugins/e-acsl/share/e-acsl/instrumentation_model/e_acsl_contract.c
@@ -77,7 +77,7 @@ struct contract_t {
contract_t *contract_init(size_t size) {
// Allocate memory for the structure
contract_t *c = malloc(sizeof(contract_t));
- DVASSERT(c != NULL, "Unable to allocate %d bytes of memory for contract_t",
+ DVASSERT(c != NULL, "Unable to allocate %d bytes of memory for contract_t\n",
sizeof(contract_t));
// Compute the number of char needed to store `size` behaviors, assuming
@@ -89,7 +89,7 @@ contract_t *contract_init(size_t size) {
c->assumes = calloc(c->char_count, sizeof(char));
DVASSERT(c->assumes != NULL,
"Unable to allocate %d cells of %d bytes of memory for "
- "contract_t::assumes",
+ "contract_t::assumes\n",
c->char_count, sizeof(char));
} else {
c->assumes = NULL;
@@ -110,7 +110,7 @@ void contract_clean(contract_t *c) {
void contract_set_behavior_assumes(contract_t *c, size_t i, int assumes) {
size_t char_idx = find_char_index(i);
DVASSERT(char_idx < c->char_count,
- "Out of bound char index %d (char_count: %d)", char_idx,
+ "Out of bound char index %d (char_count: %d)\n", char_idx,
c->char_count);
size_t bit_idx = find_bit_index(i);
assumes = normalize_to_boolean(assumes);
@@ -121,7 +121,7 @@ void contract_set_behavior_assumes(contract_t *c, size_t i, int assumes) {
int contract_get_behavior_assumes(const contract_t *c, size_t i) {
size_t char_idx = find_char_index(i);
DVASSERT(char_idx < c->char_count,
- "Out of bound char index %d (char_count: %d)", char_idx,
+ "Out of bound char index %d (char_count: %d)\n", char_idx,
c->char_count);
size_t bit_idx = find_bit_index(i);
int result = c->assumes[char_idx] & (1 << bit_idx);
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 12fdd8f1d76e474d1995570f79b99ca17228ea56..054e38c1ffb9aa952ccffa8bbf3a2209456a1f77 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
@@ -90,7 +90,7 @@ void eacsl_temporal_pull_parameter(void *ptr, unsigned int param, size_t size) {
eacsl_temporal_memcpy(ptr, tpar->ptr, size);
break;
default:
- private_assert(0, "Unreachable", NULL);
+ private_abort("Unreachable\n");
}
}
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h
index 82c85d10bc79d07e4ca2b157dee97a3da3176a1f..5eafc9bb1e73468a7821651a256175c2453f990e 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_debug.h
@@ -71,7 +71,9 @@ int dlog_fd;
# define DASSERT(_e) private_assert(_e, TOSTRING(_e), NULL)
/*! \brief Debug-time assertion based on vassert (see e_acsl_assert.h) */
-# define DVASSERT(_expr, _fmt, ...) private_assert(_expr, _fmt, __VA_ARGS__)
+# define DVASSERT(_expr, _fmt_and_args...) private_assert(_expr, _fmt_and_args)
+
+# define DVABORT(_fmt_and_args...) private_abort(_fmt_and_args)
/*! \brief Initialize debug report file:
* - open file descriptor
@@ -96,6 +98,7 @@ int debug_stop_number;
# define DVLOG(...)
# define DASSERT(_e)
# define DVASSERT(_expr, _fmt, ...)
+# define DVABORT(_fmt, ...)
#endif // E_ACSL_DEBUG
// }}}
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 9bd6e36758aadc97cec9a39b753fdf9933957506..b03debf7c70f32c4510d237c8dc82e0ea039f5a0 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
@@ -181,7 +181,7 @@ static bt_node *bt_get_leaf_from_block(bt_block *ptr) {
== (ptr->ptr & curr->left->mask))
curr = curr->left;
else
- private_assert(0, "Unreachable", NULL);
+ private_abort("Unreachable\n");
}
DASSERT(curr->is_leaf);
DASSERT(curr->leaf == ptr);
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 ae63e7c187b55d822374ba74a7223681b32bffb6..4082e4f8d9c1178dd9c4865a39750e97b0cbcb8f 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
@@ -212,7 +212,7 @@ int eacsl_initialized(void *ptr, size_t size) {
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);
+ private_assert(blk != NULL, "\\block_length of unallocated memory\n", NULL);
return blk->size;
}
@@ -258,14 +258,14 @@ int eacsl_valid_read(void *ptr, size_t size, void *ptr_base,
/* return the base address of the block containing ptr */
void *eacsl_base_addr(void *ptr) {
bt_block *tmp = bt_find(ptr);
- private_assert(tmp != NULL, "\\base_addr of unallocated memory", NULL);
+ private_assert(tmp != NULL, "\\base_addr of unallocated memory\n", NULL);
return (void *)tmp->ptr;
}
/* return the offset of `ptr` within its block */
size_t eacsl_offset(void *ptr) {
bt_block *tmp = bt_find(ptr);
- private_assert(tmp != NULL, "\\offset of unallocated memory", NULL);
+ private_assert(tmp != NULL, "\\offset of unallocated memory\n", NULL);
return ((uintptr_t)ptr - tmp->ptr);
}
/* }}} */
@@ -345,14 +345,14 @@ void eacsl_delete_block(void *ptr) {
#ifdef E_ACSL_DEBUG
/* Make sure the recorded block is not NULL */
if (!ptr)
- private_abort("Attempt to delete NULL block");
+ private_abort("Attempt to delete NULL block\n");
#endif
if (ptr != NULL) {
bt_block *tmp = bt_lookup(ptr);
#ifdef E_ACSL_DEBUG
/* Make sure the removed block exists in the tracked allocation */
if (!tmp)
- private_abort("Attempt to delete untracked block");
+ private_abort("Attempt to delete untracked block\n");
#endif
if (tmp) {
bt_clean_block_init(tmp);
@@ -373,7 +373,7 @@ void *eacsl_store_block_duplicate(void *ptr, size_t size) {
#ifdef E_ACSL_DEBUG
/* Make sure that duplicate block, if so is of the same length */
if (tmp->size != size)
- private_abort("Attempt to store duplicate block of different length");
+ private_abort("Attempt to store duplicate block of different length\n");
#endif
eacsl_delete_block(ptr);
}
@@ -637,7 +637,7 @@ void eacsl_delete_block_debug(char *file, int line, void *ptr) {
bt_block *tmp = bt_lookup(ptr);
if (!tmp) {
private_abort(
- "Block with base address %a not found in the memory model at %s:%d",
+ "Block with base address %a not found in the memory model at %s:%d\n",
ptr, file, line);
}
eacsl_delete_block(ptr);
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c
index 11a4323d8e89ffcdafef626524609203bb120e4b..c24279a10687a50073d1a34194aa5c2908df2583 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c
@@ -41,7 +41,7 @@ int allocated(uintptr_t addr, long size, uintptr_t base) {
int readonly(void *ptr) {
bt_block *blk = bt_find(ptr);
- private_assert(blk != NULL, "Readonly on unallocated memory", NULL);
+ private_assert(blk != NULL, "Readonly on unallocated memory\n", NULL);
return blk->is_readonly;
}
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 f8678b898fc9f6e9c290fdd54391951c6b22de82..d9c58eced84396efa755f94fc6009795252103ff 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
@@ -39,10 +39,10 @@ uint32_t origin_timestamp(void *ptr) {
uintptr_t temporal_referent_shadow(void *ptr) {
bt_block *blk = bt_find(ptr);
private_assert(blk != NULL,
- "referent timestamp on unallocated memory address %a",
+ "referent timestamp on unallocated memory address %a\n",
(uintptr_t)ptr);
private_assert(blk->temporal_shadow != NULL,
- "no temporal shadow of block with base address",
+ "no temporal shadow of block with base address\n",
(uintptr_t)blk->ptr);
return (uintptr_t)blk->temporal_shadow + eacsl_offset(ptr);
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h
index cc6ad8f4f6ed57ddc08c3df46500d61c8ecba57e..6f8bc48093d855354ae4503b48d85e5f95f8abd9 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_omodel_debug.h
@@ -32,7 +32,7 @@
/* Assert that a memory block [_addr, _addr + _size] is nullified */
# define DVALIDATE_NULLIFIED(_addr, _size) \
DVASSERT(zeroed_out((void *)_addr, _size), \
- "Block [%a, %a+%lu] not nullified", _addr, _addr, _size)
+ "Block [%a, %a+%lu] not nullified\n", _addr, _addr, _size)
/* Assert that memory block [_addr, _addr + _size] is allocated */
# define DVALIDATE_ALLOCATED(_addr, _size, _base) \
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 264d0e555f7d3fc817723aba8a4708a5f632c759..20fae255f71e303f2379d555d6a5a1f126577f83 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
@@ -222,7 +222,7 @@ void validate_shadow_layout() {
uintptr_t *dest = segments[j];
const char *dest_name = segment_names[j];
DVASSERT(src[1] < dest[0] || src[0] > dest[1],
- "Segment %s [%a, %a] overlaps with segment %s [%a, %a]",
+ "Segment %s [%a, %a] overlaps with segment %s [%a, %a]\n",
src_name, src[0], src[1], dest_name, dest[0], dest[1]);
}
}
@@ -413,7 +413,7 @@ uintptr_t static_info(uintptr_t addr, char type) {
case 'L': /* Length */
return sec_shadow[0];
default:
- DASSERT(0 && "Unknown static query type");
+ DVABORT("Unknown static query type\n");
}
} else {
switch (type) {
@@ -424,7 +424,7 @@ uintptr_t static_info(uintptr_t addr, char type) {
case 'L': /* Length */
return short_lengths[code];
default:
- DASSERT(0 && "Unknown static query type");
+ DVABORT("Unknown static query type\n");
}
}
}
@@ -767,7 +767,8 @@ void *realloc(void *ptr, size_t size) {
DVASSERT(
keep_bytes <= alloc_size / 8 && keep_bytes < old_alloc_size / 8,
"Attempt to access out of bound init shadow. Accessing %lu bytes, \
- old init shadow size: %lu bytes, new init shadow size: %lu bytes.",
+ old init shadow size: %lu bytes, new init shadow size: %lu \
+ bytes.\n",
keep_bytes, old_alloc_size / 8, alloc_size / 8);
memcpy(new_init_shadow, old_init_shadow, keep_bytes);
memset(old_init_shadow, 0, old_alloc_size / 8);
@@ -784,7 +785,7 @@ void *realloc(void *ptr, size_t size) {
DVASSERT(
idx < alloc_size / 8,
"Attempt to access out of bound init shadow. Accessing index %lu \
- with init shadow of size %lu bytes.",
+ with init shadow of size %lu bytes.\n",
idx, alloc_size / 8);
unsigned char mask = 0;
setbits64(rem_keep_bits, mask);
@@ -805,7 +806,7 @@ void *realloc(void *ptr, size_t size) {
DVASSERT(
(idx + count) <= alloc_size / 8,
"Attempt to access out of bound init shadow. Accessing %lu bytes \
- from index %lu with init shadow of size %lu bytes.",
+ from index %lu with init shadow of size %lu bytes.\n",
count, idx, alloc_size / 8);
memset(new_init_shadow + idx, 0, count);
}
@@ -850,7 +851,7 @@ int posix_memalign(void **memptr, size_t alignment, size_t size) {
/* Make sure that the first argument to posix memalign is indeed allocated */
private_assert(
allocated((uintptr_t)memptr, sizeof(void *), (uintptr_t)memptr),
- "\\invalid memptr in posix_memalign", NULL);
+ "\\invalid memptr in posix_memalign\n", NULL);
int res = public_posix_memalign(memptr, alignment, size);
if (!res) {
@@ -930,7 +931,7 @@ uintptr_t heap_info(uintptr_t addr, char type) {
* between the input address and the base address of the block. */
return addr - *aligned_shadow;
default:
- DASSERT(0 && "Unknown heap query type");
+ DVABORT("Unknown heap query type\n");
}
return 0;
}
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 26e06ad028752e94482227c9bd9cadf595f3dbc1..94214735f8d02a00e6ab1d86e50ab019ad634d65 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
@@ -112,20 +112,20 @@
#ifdef E_ACSL_DEBUG
# define DVALIDATE_ALIGNMENT(_addr) \
DVASSERT(((uintptr_t)_addr) % HEAP_SEGMENT == 0, \
- "Heap base address %a is unaligned", _addr)
+ "Heap base address %a is unaligned\n", _addr)
# define DVALIDATE_MEMORY_PRE_MAIN_INIT \
DVASSERT(mem_layout.is_initialized_pre_main != 0, \
- "Un-initialized pre-main shadow layout", NULL)
+ "Un-initialized pre-main shadow layout\n", NULL)
# define DVALIDATE_MEMORY_MAIN_INIT \
DVASSERT(mem_layout.is_initialized_main != 0, \
- "Un-initialized main shadow layout", NULL)
+ "Un-initialized main shadow layout\n", NULL)
# define DVALIDATE_MEMORY_INIT \
DVASSERT(mem_layout.is_initialized_pre_main != 0 \
&& mem_layout.is_initialized_main != 0, \
- "Un-initialized shadow layout", NULL)
+ "Un-initialized shadow layout\n", NULL)
/* Debug function making sure that the order of program segments is as expected
* and that the program and the shadow segments used do not overlap. */
@@ -138,9 +138,9 @@ void validate_shadow_layout();
/* Assert that boundaries of a block [_addr, _addr+_size] are within a segment
* given by `_s`. `_s` is either HEAP, STACK, TLS, GLOBAL or STATIC. */
# define DVALIDATE_IS_ON(_addr, _size, _s) \
- DVASSERT(IS_ON_##_s(_addr), "Address %a not on %s", _addr, #_s); \
- DVASSERT(IS_ON_##_s(_addr + _size), "Address %a not on %s", _addr + _size, \
- #_s)
+ DVASSERT(IS_ON_##_s(_addr), "Address %a not on %s\n", _addr, #_s); \
+ DVASSERT(IS_ON_##_s(_addr + _size), "Address %a not on %s\n", \
+ _addr + _size, #_s)
/* Assert that [_addr, _addr+_size] are within heap segment */
# define DVALIDATE_IS_ON_HEAP(_addr, _size) DVALIDATE_IS_ON(_addr, _size, HEAP)
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 e37c4ad740aa884609476b7fcb18b40006045860..9b910aaa18097903a66cdcd1844a72159be31db0 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
@@ -70,7 +70,7 @@ size_t increase_stack_limit(const size_t size) {
size_t get_stack_size() {
struct rlimit rlim;
private_assert(!getrlimit(RLIMIT_STACK, &rlim),
- "Cannot detect program's stack size", NULL);
+ "Cannot detect program's stack size\n", NULL);
return rlim.rlim_cur;
}