From 2004fbc172e49f7f6e4898e4adc34e35346d65e4 Mon Sep 17 00:00:00 2001 From: Thibaut Benjamin <thibaut.benjamin@gmail.com> Date: Tue, 5 Apr 2022 15:47:23 +0200 Subject: [PATCH] [e-acsl] first review --- .../internals/e_acsl_safe_locations.c | 3 +- .../segment_model/e_acsl_shadow_layout.c | 11 +- .../segment_model/e_acsl_shadow_layout.h | 2 +- .../oracle_dev/threads_debug.e-acsl.err.log | 258 +++++++++--------- .../e-acsl/tests/concurrency/threads_debug.c | 2 +- .../oracle_dev/e-acsl-rt-debug.e-acsl.err.log | 18 +- 6 files changed, 151 insertions(+), 143 deletions(-) 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 a8c8f41d96f..6e0d5403e95 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 @@ -58,8 +58,7 @@ uintptr_t get_safe_locations_start() { } uintptr_t get_safe_locations_end() { - memory_location *first_location = get_safe_location(0); - uintptr_t max = first_location->address; + 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) 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 2b58af42b3b..3578bc01584 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 @@ -223,6 +223,16 @@ 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; @@ -247,7 +257,6 @@ uintptr_t get_tls_start(int 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 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 0dc8ade8124..5a7bf7272c4 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 22ba0d967c8..1f0d3a94375 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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: 19 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 19 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 19 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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 e5cf53be95a..75bf51d6121 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 | sed -e s/[0-9]*\sMB/xxMB/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/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 dba7d415d87..ca626442b2b 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: 3 MB [0x0000-0000-0000, 0x0000-0000-0000] - Primary : 3 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx } - Secondary : 3 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 } -- GitLab