diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
index 4169419fdbf5030345e5414704ab2888925a738b..6e0d5403e95fe600ef421349c21dbfa62d829120 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.c
@@ -42,14 +42,43 @@ static __thread int safe_location_counter = 0;
safe_location_counter++; \
} while (0)
+struct segment_boundaries safe_locations_boundaries = {
+ .start = 0,
+ .end = 0,
+};
+
+uintptr_t get_safe_locations_start() {
+ uintptr_t min = get_safe_location(0)->address;
+ for (int i = 1; i < get_safe_locations_count(); i++) {
+ memory_location *location = get_safe_location(i);
+ if (min >= location->address)
+ min = location->address;
+ }
+ return min;
+}
+
+uintptr_t get_safe_locations_end() {
+ uintptr_t max = get_safe_location(0)->address;
+ for (int i = 1; i < get_safe_locations_count(); i++) {
+ memory_location *location = get_safe_location(i);
+ if (max <= location->address)
+ max = location->address;
+ }
+ return max;
+}
+
void collect_safe_locations() {
/* Tracking of errno and standard streams */
add_safe_location((uintptr_t)&errno, sizeof(int), 1, E_ACSL_OS_IS_LINUX);
add_safe_location((uintptr_t)stdout, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
add_safe_location((uintptr_t)stderr, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
add_safe_location((uintptr_t)stdin, sizeof(FILE), 1, E_ACSL_OS_IS_LINUX);
+ safe_locations_boundaries.start = get_safe_locations_start();
+ safe_locations_boundaries.end = get_safe_locations_end();
}
+/* collect_safe_locations(); */
+
size_t get_safe_locations_count() {
return safe_location_counter;
}
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
index 19c05fec0687b9af6b35c7628e81a2b2962cf20f..f77a3ca4c0f7890abe4da678cd129552219cc315 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/internals/e_acsl_safe_locations.h
@@ -50,6 +50,14 @@ struct memory_location {
};
typedef struct memory_location memory_location;
+struct segment_boundaries {
+ uintptr_t start;
+ uintptr_t end;
+};
+typedef struct segment_boundaries segment_boundaries;
+
+struct segment_boundaries safe_locations_boundaries;
+
/*! Initialize the array of safe locations */
void collect_safe_locations();
diff --git a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c
index 042eef56fbcf55f56be63002d2825d290ccc6570..3d92f1977f81bc31634a6c04888742941d62047f 100644
--- a/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c
+++ b/src/plugins/e-acsl/share/e-acsl/observation_model/segment_model/e_acsl_shadow_concurrency.c
@@ -183,7 +183,11 @@ static void fill_thread_layout_stack(memory_partition *pstack,
static void fill_thread_layout_tls(memory_partition *ptls) {
// Since the TLS is by design specific to each thread, we can reuse the
// method used to identify the TLS segment in the main thread
- set_application_segment(&ptls->application, get_tls_start(), get_tls_size(),
+ // We first need to collect the safe locations of the current thread,
+ // since we need to register them in case the program uses one of them
+ // inside the thread
+ collect_safe_locations();
+ set_application_segment(&ptls->application, get_tls_start(0), get_tls_size(),
"thread_tls", NULL);
set_shadow_segment(&ptls->primary, &ptls->application, 1,
"thread_tls_primary");
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 258cc25fde89442abd39671ac57a6d50ace6b9d0..15870873f1afe6e642d76b62ec3760a7d881f700 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
@@ -53,6 +53,9 @@ extern char end;
/*!\brief The first address of a program. */
extern char __executable_start;
+uintptr_t actual_tls_size = 0;
+uintptr_t registered_tls_start = 0;
+
size_t increase_stack_limit(const size_t size) {
rlim_t stacksz = (rlim_t)size;
struct rlimit rl;
@@ -166,7 +169,7 @@ static size_t get_global_size() {
/*! \brief Return byte-size of the TLS segment */
inline size_t get_tls_size() {
- return PGM_TLS_SIZE;
+ return (actual_tls_size == 0 ? PGM_TLS_SIZE : actual_tls_size);
}
static __thread int id_tdata = 1;
@@ -220,13 +223,40 @@ static void grow_bounds_for_size(uintptr_t *min_bound, uintptr_t *max_bound,
}
}
+// We do not exactly know the bounds of the TLS, we can only guess an
+// approximation. To do that, we take TLS's known addresses and add a buffer
+// around them. Since the TLS in Linux is positionned around the heap, we can
+// check if the approximation overlaps with heap space and adjust it
+// accordingly. The heap spaces allocated for E-ACSL are of course application
+// heap and rtl spaces, but also shadow memory spaces. We also add as a condition
+// that the [safe_locations] should be in the TLS, by construction. It might
+// happen that those addresses are separated by a more than half the size of
+// our initial guess. If this is the case, we have to increase the size of
+// our guess in order to fit both the TLS that we see and its shadow model.
+static void init_tls_size() {
+ uintptr_t data = (uintptr_t)&id_tdata, bss = (uintptr_t)&id_tbss;
+ uintptr_t min_safe_loc = safe_locations_boundaries.start;
+ uintptr_t max_safe_loc = safe_locations_boundaries.end;
+ uintptr_t min_addr = data < bss ? data : bss;
+ uintptr_t max_addr = data > bss ? data : bss;
+ min_addr = min_addr < min_safe_loc ? min_addr : min_safe_loc;
+ max_addr = max_addr > max_safe_loc ? max_addr : max_safe_loc;
+ uintptr_t size = (max_addr - min_addr + 1) * 2;
+ actual_tls_size = size > PGM_TLS_SIZE ? size : PGM_TLS_SIZE;
+}
+
/*! \brief Return start address of a program's TLS */
-uintptr_t get_tls_start() {
+uintptr_t get_tls_start(int main_thread) {
size_t tls_size = get_tls_size();
uintptr_t data = (uintptr_t)&id_tdata, bss = (uintptr_t)&id_tbss;
+ uintptr_t min_safe_loc = safe_locations_boundaries.start;
+ uintptr_t max_safe_loc = safe_locations_boundaries.end;
uintptr_t min_addr = data < bss ? data : bss;
uintptr_t max_addr = data > bss ? data : bss;
-
+ if (main_thread) {
+ min_addr = min_addr < min_safe_loc ? min_addr : min_safe_loc;
+ max_addr = max_addr > max_safe_loc ? max_addr : max_safe_loc;
+ }
// We do not exactly know the bounds of the TLS, we can only guess an
// approximation. To do that, we take TLS's known addresses and add a buffer
// around them. Since the TLS in Linux is positionned around the heap, we can
@@ -287,15 +317,19 @@ uintptr_t get_tls_start() {
private_abort("Unsupported TLS area in the middle of heap area.\n"
"Example bss TLS address: %a\n"
"Example data TLS address: %a\n"
- "Estimated bounds of heap area: [%a, %a]\n",
- bss, data, min_bound, max_bound);
+ "Range of safe locations data: [%a, %a]\n"
+ "Estimated bounds of heap area: [%a, %a]\n"
+ "Minimal TLS address: %a\n",
+ bss, data, min_safe_loc, max_safe_loc, min_bound, max_bound,
+ min_addr);
}
-
private_assert(tls_start <= min_addr && max_addr <= tls_end,
"Configured TLS size smaller than actual TLS size\n"
"Configured TLS size: %" PRIxPTR " MB\n"
"Minimum supported TLS size for this execution: %" PRIxPTR
- " MB (%" PRIxPTR " B)\n",
+ " MB (%" PRIxPTR " B)\n"
+ "Please ensure that the TLS size has been initialize with "
+ "[init_tls_size()]",
MB_SZ(tls_size),
// The minimum actual size is found by substracting the lesser
// known TLS address to the greater one. Since we estimate the
@@ -328,7 +362,10 @@ static void init_shadow_layout_global() {
static void init_shadow_layout_tls() {
memory_partition *ptls = &mem_layout.tls;
- set_application_segment(&ptls->application, get_tls_start(), get_tls_size(),
+ /* Collect the safe locations of the main thread */
+ collect_safe_locations();
+ init_tls_size();
+ set_application_segment(&ptls->application, get_tls_start(1), get_tls_size(),
"tls", NULL);
/* Changes of the ratio in the following would require changes in get_tls_start */
set_shadow_segment(&ptls->primary, &ptls->application, 1, "tls_primary");
@@ -709,7 +746,6 @@ void init_shadow_layout_main(int *argc_ref, char ***argv_ref) {
}
void register_safe_locations(int thread_only) {
- collect_safe_locations();
int count = get_safe_locations_count();
for (int i = 0; i < count; ++i) {
memory_location *loc = get_safe_location(i);
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 0dc8ade8124565c23a3218867afc3c9ca51c6d93..5a7bf7272c4637f4605e4266535b5b816b44c400 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
@@ -120,7 +120,7 @@ size_t get_heap_size();
size_t get_tls_size();
/*! \brief Return start address of a program's TLS */
-uintptr_t get_tls_start();
+uintptr_t get_tls_start(int main_thread);
/** }}} */
/** Shadow Layout {{{ */
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle_dev/threads_debug.e-acsl.err.log b/src/plugins/e-acsl/tests/concurrency/oracle_dev/threads_debug.e-acsl.err.log
index e338b6d403c5a5e10843cf71d93df93272621992..1f0d3a94375d8a4739ab04df8909eaec26127b7f 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle_dev/threads_debug.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/concurrency/oracle_dev/threads_debug.e-acsl.err.log
@@ -1,182 +1,182 @@
>>> HEAP ---------------------
- Application: 128 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 128 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> STACK --------------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> GLOBAL -------------------
Application: xxxkB [0x0000-0000-0000, 0x0000-0000-0000]
Primary : xxxkB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
Secondary : xxxkB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> TLS ----------------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> VDSO ---------------------
Application: xxxkB [0x0000-0000-0000, 0x0000-0000-0000]
Primary : xxxkB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
Secondary : xxxkB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> --------------------------
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread stack -------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> Thread TLS ---------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
*** WARNING: Leakedxxxbytes of heap memory in 2 blocks
diff --git a/src/plugins/e-acsl/tests/concurrency/threads_debug.c b/src/plugins/e-acsl/tests/concurrency/threads_debug.c
index 35837359d4f1de8addc0f62050b90be999d13137..75bf51d6121358b31fa55b3114b3d2b2ac5a6b12 100644
--- a/src/plugins/e-acsl/tests/concurrency/threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/threads_debug.c
@@ -4,7 +4,7 @@
MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose --concurrency
COMMENT: Filter the addresses of the output so that the test is deterministic.
- MACRO: ROOT_EACSL_EXEC_FILTER sed -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | sed -e s_Offset:\s[0-9-]*_Offset:xxxxx_g | sed -e s/[0-9]*\skB/xxxkB/g | sed -e s/Leaked.*bytes/Leakedxxxbytes/g
+ MACRO: ROOT_EACSL_EXEC_FILTER sed -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | sed -e s_Offset:\s[0-9-]*_Offset:xxxxx_g | sed -e s/[0-9]*\skB/xxxkB/g | sed -e s/[0-9]*\sMB/xxxMB/g | sed -e s/Leaked.*bytes/Leakedxxxbytes/g
*/
// Include existing test
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 ec28d64c54f39dc42bce34ca67dae6051c2a5300..3dad85476b7bc1cf6da89c7884342b9b7ba268e1 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 sed -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | sed -e s_Offset:\s[0-9-]*_Offset:xxxxx_g | sed -e s/[0-9]*\skB/xxxkB/g
+ MACRO: ROOT_EACSL_EXEC_FILTER sed -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | sed -e s_Offset:\s[0-9-]*_Offset:xxxxx_g | sed -e s/[0-9]*\skB/xxxkB/g | sed -e s/[0-9]*\sMB/xxMB/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 4606d5468186f5a26f438b45094a0c1919c95741..ca626442b2bc4816438a84c5944c754b3d39ee97 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,19 +1,19 @@
>>> HEAP ---------------------
- Application: 128 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 128 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> STACK --------------------
- Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> GLOBAL -------------------
Application: xxxkB [0x0000-0000-0000, 0x0000-0000-0000]
Primary : xxxkB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
Secondary : xxxkB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> TLS ----------------------
- Application: 2 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
- Secondary : 2 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Application: xxMB [0x0000-0000-0000, 0x0000-0000-0000]
+ Primary : xxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : xxMB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> VDSO ---------------------
Application: xxxkB [0x0000-0000-0000, 0x0000-0000-0000]
Primary : xxxkB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }