diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 1976998a6fea11f1c4c50142815bc3213f1882c8..63e965d0c9d53b2bb6bcda0f0a4c5905aa1b9843 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -25,6 +25,14 @@
Plugin E-ACSL <next-release>
############################
+- E-ACSL [2021-11-03] Improve runtime debug logs: the %a modifier now
+ outputs in hexadecimal, the debug logs now all end in new lines,
+ the trace now outputs to stderr.
+-* E-ACSL [2021-11-03] Fix default stack size: E_ACSL_STACK_SIZE
+ is now correctly used by the runtime, the default values
+ have been adjusted to what was effectively used.
+-* E-ACSL [2021-11-03] Now the same Frama-C options are used when parsing
+ the user sources and the E-ACSL's RTL.
- E-ACSL [2021-10-20] Add option -e-acsl-assert-print-data
(--assert-print-data in e-acsl-gcc.sh) to print data
contributing to a failed assertion along with the error message.
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index cab1f3ede72d4cfd8635ba6c0089894e5dbc2060..8547ac9d2e1d37fcc2b8c66c7fd6dc1131c99821 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -349,8 +349,8 @@ OPTION_VALIDATE_FORMAT_STRINGS= # Runtime format string validation
OPTION_LIBC_REPLACEMENTS= # Replace libc functions with RTL definitions
OPTION_RTE_SELECT= # Generate assertions for these functions only
OPTION_THEN= # Adds -then in front of -e-acsl in FC command.
-OPTION_STACK_SIZE=32 # Size of a heap shadow space (in MB)
-OPTION_HEAP_SIZE=128 # Size of a stack shadow space (in MB)
+OPTION_STACK_SIZE= # Size of a heap shadow space (in MB)
+OPTION_HEAP_SIZE= # Size of a stack shadow space (in MB)
OPTION_KEEP_GOING= # Report failing assertions but do not abort execution
OPTION_EXTERNAL_ASSERT="" # Use custom definition of assert function
OPTION_ASSERT_PRINT_DATA= # Print data contributing to a failed runtime assertion
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/internals/e_acsl_rtl_io.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
index 8b6d2d4e9d6497ea63154f2069c94402e87956b4..6bcc5370058d07296866fdfe13497c6b01317525 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_rtl_io.c
@@ -72,11 +72,15 @@ static void addr2a(uintptr_t addr, char *bf) {
*bf++ = '0';
*bf++ = 'x';
+ int base = 16;
+ int group = 4;
+ char sep = '-';
+
unsigned int digits = 1;
int n = 0;
unsigned long int d = 1;
- while (addr / d >= 10) {
- d *= 10;
+ while (addr / d >= base) {
+ d *= base;
digits++;
}
@@ -85,13 +89,13 @@ static void addr2a(uintptr_t addr, char *bf) {
ctr++;
int dgt = addr / d;
addr %= d;
- d /= 10;
+ d /= base;
if (n || dgt > 0 || d == 0) {
*bf++ = dgt + (dgt < 10 ? '0' : 'a' - 10);
++n;
}
- if (--digits % 5 == 0 && d != 0)
- *bf++ = '-';
+ if (--digits % group == 0 && d != 0)
+ *bf++ = sep;
}
*bf = 0;
}
@@ -100,7 +104,7 @@ static void addr2a(uintptr_t addr, char *bf) {
static void ptr2a(void *p, char *bf) {
*bf++ = '0';
*bf++ = 'x';
- uli2a((intptr_t)p, 16, 0, bf);
+ uli2a((uintptr_t)p, 16, 0, bf);
}
/* Signed long integer to string conversion (%ld) */
diff --git a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
index 2d0bff075be92ed60c3c7070c7bca7ab2f95701b..81f7901c8c6e66e4af814ee0791e377c6851ffe2 100644
--- a/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
+++ b/src/plugins/e-acsl/share/e-acsl/internals/e_acsl_trace.c
@@ -85,7 +85,7 @@ void trace() {
char executable[PATH_MAX];
rtl_sprintf(executable, "/proc/%d/exe", getpid());
- STDOUT("/** Backtrace **************************/\n");
+ STDERR("/** Backtrace **************************/\n");
int counter = 0;
while (*bb) {
char *addr = (char *)private_malloc(21);
@@ -99,18 +99,18 @@ void trace() {
if (outs) {
outs[strlen(outs) - 1] = '\0';
if (strlen(outs) && endswith(outs, "??:0") && endswith(outs, "??:?")) {
- STDOUT("%s%s\n", prefix, outs);
+ STDERR("%s%s\n", prefix, outs);
}
} else {
char *errs = (char *)ipr->stderrs;
if (errs) {
- STDOUT("%s\n", errs);
+ STDERR("%s\n", errs);
}
}
}
bb++;
counter++;
}
- STDOUT("/***************************************/\n");
+ STDERR("/***************************************/\n");
#endif /* E_ACSL_OS_IS_LINUX */
}
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_observation_model.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
index b67b9b3fe6f28a15dc797310715a6ac13241fdcb..cbb04be951eab07b4ddecdf7fa96be0a4aa41b7b 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
@@ -224,7 +224,7 @@ void eacsl_memory_init(int *argc_ref, char ***argv_ref, size_t ptr_size) {
/* Initialize report file with debug logs (only in debug mode). */
initialize_report_file(argc_ref, argv_ref);
/* Lift stack limit to account for extra stack memory overhead. */
- increase_stack_limit(get_stack_size() * 2);
+ increase_stack_limit(E_ACSL_STACK_SIZE * MB);
/* Allocate and log shadow memory layout of the execution. Case of the
segments available after main. */
init_shadow_layout_main(argc_ref, argv_ref);
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;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
index 93de48c4ad3b99bcc137ca40ccaa3c76fb620bb4..f64825206dd86c8579ab4bb78b8ff16eb91e6996 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
@@ -36,12 +36,12 @@
/* Default size of a program's heap tracked via shadow memory */
#ifndef E_ACSL_HEAP_SIZE
-# define E_ACSL_HEAP_SIZE 512
+# define E_ACSL_HEAP_SIZE 128
#endif
/* Default size of a program's stack tracked via shadow memory */
#ifndef E_ACSL_STACK_SIZE
-# define E_ACSL_STACK_SIZE 64
+# define E_ACSL_STACK_SIZE 16
#endif
/* MAP_ANONYMOUS is a mmap flag indicating that the contents of allocated blocks
diff --git a/src/plugins/e-acsl/src/main.ml b/src/plugins/e-acsl/src/main.ml
index 8439a6b2b725c35b843318e35ada2accb345a919..179208761e50a057c0383b80ad0c7079c6fcaa61 100644
--- a/src/plugins/e-acsl/src/main.ml
+++ b/src/plugins/e-acsl/src/main.ml
@@ -40,19 +40,7 @@ let generate_code =
(fun name ->
Options.feedback "beginning translation.";
Temporal.enable (Options.Temporal_validity.get ());
- if Plugin.is_present "variadic" then begin
- let opt_name = "-variadic-translation" in
- if Dynamic.Parameter.Bool.get opt_name () &&
- Options.Validate_format_strings.get () then begin
- if Ast.is_computed () then
- Options.abort
- "The variadic translation is incompatible with E-ACSL option \
- '%s'.@ Please use option '-variadic-no-translation'."
- Options.Validate_format_strings.option_name
- Options.warning "deactivating variadic translation";
- Dynamic.Parameter.Bool.off opt_name ();
- end
- end;
+ Options.setup ();
(* slightly more efficient to copy the project before computing the AST
if it is not yet computed *)
let rtl_prj_name = Options.Project_name.get () ^ " RTL" in
diff --git a/src/plugins/e-acsl/src/options.ml b/src/plugins/e-acsl/src/options.ml
index e4f6bdddd94e5c6ad94c656f6e85e0dea9120e16..cc172a073cca608159d727b83e34df66c02e3a13 100644
--- a/src/plugins/e-acsl/src/options.ml
+++ b/src/plugins/e-acsl/src/options.ml
@@ -177,6 +177,35 @@ let dkey_prepare = register_category "preparation"
let dkey_translation = register_category "translation"
let dkey_typing = register_category "typing"
+let setup ?(rtl=false) () =
+ (* Variadic translation *)
+ if Plugin.is_present "variadic" then begin
+ let opt_name = "-variadic-translation" in
+ if Dynamic.Parameter.Bool.get opt_name () then begin
+ if rtl then
+ (* If we are translating the RTL project, then we need to deactivate the
+ variadic translation. Indeed since we are translating the RTL in
+ isolation, we do not now if the variadic functions are used by the
+ user project and we cannot monomorphise them accordingly. *)
+ Dynamic.Parameter.Bool.off opt_name ()
+ else if Validate_format_strings.get () then begin
+ if Ast.is_computed () then
+ abort
+ "The variadic translation is incompatible with E-ACSL option \
+ '%s'.@ Please use option '-variadic-no-translation'."
+ Validate_format_strings.option_name;
+ warning ~once:true "deactivating variadic translation";
+ Dynamic.Parameter.Bool.off opt_name ();
+ end
+ end
+ end;
+ (* Additionnal kernel options while parsing the RTL project. *)
+ if rtl then begin
+ Kernel.Keep_unused_specified_functions.off ();
+ Kernel.CppExtraArgs.add
+ (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
+ end
+
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/e-acsl/src/options.mli b/src/plugins/e-acsl/src/options.mli
index eda2b4a31e1271bd08c5cdf9d9ee8c72323e6bde..ec3f385c089743a1901f0a52b355cd22ea42c6e1 100644
--- a/src/plugins/e-acsl/src/options.mli
+++ b/src/plugins/e-acsl/src/options.mli
@@ -46,6 +46,11 @@ val dkey_prepare: category
val dkey_translation: category
val dkey_typing: category
+val setup: ?rtl:bool -> unit -> unit
+(** Verify and initialize the options of the current project according to the
+ options set by the user.
+ If [rtl] is true, then the project being modified is the RTL project. *)
+
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 2666f70349900e1e38437991b775f84f36ae1f90..c48aa7a7e8f48c066a20b77dde02d94992f99dea 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/src/plugins/e-acsl/src/project_initializer/rtl.ml
@@ -31,11 +31,7 @@ let create_rtl_ast prj =
prj
(fun () ->
(* compute the RTL AST in the standard E-ACSL setting *)
- if Plugin.is_present "variadic" then
- Dynamic.Parameter.Bool.off "-variadic-translation" ();
- Kernel.Keep_unused_specified_functions.off ();
- Kernel.CppExtraArgs.add
- (Format.asprintf " -DE_ACSL_MACHDEP=%s" (Kernel.Machdep.get ()));
+ Options.setup ~rtl:true ();
Kernel.Files.set [ rtl_file () ];
Ast.get ())
()
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
index 50e2bd836c0f0066ac43d023809c3bf213578de2..1f58f5e6b965c2af807ca2ea7605fd1343253dba 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
@@ -5,7 +5,7 @@
/* run.config_dev
MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose --full-mtracking
COMMENT: Filter the addresses of the output so that the test is deterministic.
- MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|0x[0-9-]*|0x00000-00000-00000|g" | @SEDCMD@ -e "s|Offset: [0-9-]*|Offset: xxxx|g"
+ MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|0x[0-9a-f-]*|0x0000-0000-0000|g" | @SEDCMD@ -e "s|Offset: [0-9-]*|Offset: xxxx|g"
*/
int main() {
return 0;
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
index 3ae40d5d7872ad1db6e7c6d073868023c2ab74b7..30d0abab894eea95a8bf6781909e678cf384f022 100644
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
@@ -1,17 +1,17 @@
>>> HEAP ---------------------
- Application: 128 MB [0x00000-00000-00000, 0x00000-00000-00000]
- Primary : 128 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
- Secondary : 16 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
+ Application: 128 MB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : 128 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
>>> STACK --------------------
- Application: 16 MB [0x00000-00000-00000, 0x00000-00000-00000]
- Primary : 16 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
- Secondary : 16 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
+ Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
>>> GLOBAL -------------------
- Application: 0 MB [0x00000-00000-00000, 0x00000-00000-00000]
- Primary : 0 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
- Secondary : 0 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
+ Application: 0 MB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Secondary : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
>>> TLS ----------------------
- Application: 64 MB [0x00000-00000-00000, 0x00000-00000-00000]
- Primary : 64 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
- Secondary : 64 MB [0x00000-00000-00000, 0x00000-00000-00000]{ Offset: xxxx }
+ Application: 64 MB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Secondary : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
>>> --------------------------