diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 3800b3eef5d60b4ae1b22d86f29dde339e274981..55e3f3ec2a17585ce6398cd6d1e2ad9affa43f2b 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -27,6 +27,12 @@ Plugin E-ACSL <next-release>
-! E-ACSL [2024-04-04] remove option -e-acsl-version.
+###############################################################################
+Plugin E-ACSL 29.0 (Copper)
+###############################################################################
+
+-* E-ACSL [2024-04-05] fix TLS segment start address and size
+
###############################################################################
Plugin E-ACSL 28.1 (Nickel)
###############################################################################
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 cf42d699dd17c3d8723f6c9b1736b00c7a8598e2..a4460b06857c962b30f34bdb286494fb309bd0e7 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
@@ -32,6 +32,7 @@
#if E_ACSL_OS_IS_LINUX
+# include <asm/prctl.h>
# include <fcntl.h>
# include <inttypes.h>
# include <stdio.h>
@@ -56,6 +57,15 @@ extern char __executable_start;
uintptr_t actual_tls_size = 0;
uintptr_t registered_tls_start = 0;
+/* TLS system query structure and functions */
+typedef struct {
+ long moduleId;
+ long tlsoffset;
+} TLS_INDEX;
+
+extern uintptr_t __tls_get_addr(TLS_INDEX *idx);
+extern void arch_prctl(int mod, uintptr_t *idx);
+
size_t increase_stack_limit(const size_t size) {
rlim_t stacksz = (rlim_t)size;
struct rlimit rl;
@@ -152,192 +162,30 @@ static size_t get_global_size() {
* Similar to globals using .data and .bss, .tdata keeps track of initialized
* thread-local variables, while .tbss holds uninitialized ones.
*
- * Start and end addresses of TLS are obtained by taking addresses of
- * initialized and uninitialized variables in TLS (::id_tdata and ::id_tss)
- * and adding fixed amount of shadow space around them. Visually it looks
- * as follows:
+ * Start and end addresses of TLS are obtained with system call
+ * arch_prctl(FS) return the max address of the TLS segment
+ * depending on system alignement policy. Work only on 64 bits system
*
- * end TLS address (&id_tdata + TLS_SHADOW_SIZE/2)
- * id_tdata address
- * ...
- * id_tbss address
- * start TLS address (&id_bss - TLS_SHADOW_SIZE/2)
+ * __get_tls_addr return the start adress of the TLS segment
*
- * HOWEVER problems can occur if PGM_TLS_SIZE is too big:
- * see get_tls_start for details.
+ * All __threads varaiables defined in dynamic libs will not be seen !
*/
/*! \brief Return byte-size of the TLS segment */
inline size_t get_tls_size() {
- return (actual_tls_size == 0 ? PGM_TLS_SIZE : actual_tls_size);
+ return actual_tls_size;
}
static __thread int id_tdata = 1;
static __thread int id_tbss;
-/*! \brief Macro to update `bound` to `value` if `bound op value`.
- `op` needs to be a relational operator. */
-# define update_bound_if(bound, op, value) \
- do { \
- if ((bound)op(value)) { \
- (bound) = (value); \
- } \
- } while (0)
-
-/*! \brief Update `*min_bound` and `*max_bound` with the shadow bounds of the
- given memory partition. */
-static void update_bounds_from_partition(uintptr_t *min_bound,
- uintptr_t *max_bound,
- memory_partition *part) {
- update_bound_if(*min_bound, >, part->primary.start);
- update_bound_if(*max_bound, <, part->primary.end);
- update_bound_if(*min_bound, >, part->secondary.start);
- update_bound_if(*max_bound, <, part->secondary.end);
-# ifdef E_ACSL_TEMPORAL
- update_bound_if(*min_bound, >, part->temporal_primary.start);
- update_bound_if(*max_bound, <, part->temporal_primary.end);
- update_bound_if(*min_bound, >, part->temporal_secondary.start);
- update_bound_if(*max_bound, <, part->temporal_secondary.end);
-# endif
-}
-
-/*! \brief Grow `*min_bound` or `*max_bound` for the given `size` depending of
- the growth direction of the heap. */
-static void grow_bounds_for_size(uintptr_t *min_bound, uintptr_t *max_bound,
- size_t size) {
- memory_partition *pheap = &mem_layout.heap;
- if (pheap->primary.end < pheap->application.start) {
- // Since the application space is allocated before the primary heap shadow
- // space, we know that the heap grows downwards.
- *min_bound -= size;
-# ifdef E_ACSL_TEMPORAL
- *min_bound -= size;
-# endif
- } else {
- // Since the application space is allocated before the primary heap shadow
- // space, we know that the heap grows upwards.
- *max_bound += size;
-# ifdef E_ACSL_TEMPORAL
- *max_bound += size;
-# endif
- }
-}
-
-// 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(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
- // 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.
- memory_partition *pheap = &mem_layout.heap;
- memory_partition *pglobal = &mem_layout.global;
- memory_partition *pvdso = &mem_layout.vdso;
- uintptr_t min_bound = mem_spaces.rtl_start;
- uintptr_t max_bound = mem_spaces.rtl_end;
- update_bound_if(min_bound, >, pheap->application.start);
- update_bound_if(max_bound, <, pheap->application.end);
- update_bounds_from_partition(&min_bound, &max_bound, pheap);
- update_bounds_from_partition(&min_bound, &max_bound, pglobal);
- update_bounds_from_partition(&min_bound, &max_bound, pvdso);
-
- if (mem_layout.is_initialized_main) {
- memory_partition *pstack = &mem_layout.stack;
- update_bounds_from_partition(&min_bound, &max_bound, pstack);
- } else {
- // Shadow spaces for the stack are not yet allocated at this point, we can
- // estimate the bounds by manually adding the spaces (the `2 *` is for
- // primary and secondary shadows).
- // If the ratio between application and shadow space is changed in
- // `init_shadow_layout_stack()`, then the sizes must be updated here.
- grow_bounds_for_size(&min_bound, &max_bound, 2 * E_ACSL_STACK_SIZE * MB);
- }
-
- if (mem_layout.is_initialized_pre_main) {
- memory_partition *ptls = &mem_layout.tls;
- update_bounds_from_partition(&min_bound, &max_bound, ptls);
- } else {
- // Shadow spaces for the main thread TLS are not yet allocated at this
- // point, we can estimate the bounds by manually adding the spaces (the
- // `2 *` is for primary and secondary shadows).
- // If the ratio between application and shadow space is changed in
- // `init_shadow_layout_tls()`, then the sizes must be updated here.
- grow_bounds_for_size(&min_bound, &max_bound, 2 * tls_size);
- }
-
- // Estimate the location of the TLS area by centering it on a known TLS
- // address and moving it to not overlap the known heap space
- uintptr_t tls_start = 0, tls_end = 0;
- if (min_addr > max_bound) {
- // The TLS is located after the heap space
- uintptr_t tls_start_half = min_addr - tls_size / 2;
- tls_start = tls_start_half > max_bound ? tls_start_half : max_bound + 1;
- tls_end = tls_start + tls_size - 1;
- } else if (max_addr < min_bound) {
- // The TLS is located before the heap space
- uintptr_t tls_end_half = max_addr + tls_size / 2;
- tls_end = tls_end_half < min_bound ? tls_end_half : min_bound - 1;
- tls_start = tls_end - tls_size + 1;
- } else {
- // The TLS is located in the middle of known heap space, this situation is
- // currently unsupported
- private_abort("Unsupported TLS area in the middle of heap area.\n"
- "Example bss TLS address: %a\n"
- "Example data TLS address: %a\n"
- "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"
- "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
- // start of the TLS by doing `min_addr - tls_size / 2`, we need
- // to multiply `max_addr - min_addr` by 2 so that both
- // addresses are covered.
- MB_SZ((max_addr - min_addr) * 2), (max_addr - min_addr) * 2);
-
+/*! \brief Return start address of a program's TLS and compute it's size */
+uintptr_t get_tls_start() {
+ TLS_INDEX tlsparams = {1, 0};
+ uintptr_t tls_start = __tls_get_addr(&tlsparams);
+ uintptr_t tls_end;
+ arch_prctl(ARCH_GET_FS, &tls_end);
+ actual_tls_size = tls_end - tls_start;
return tls_start;
}
@@ -362,12 +210,14 @@ static void init_shadow_layout_global() {
static void init_shadow_layout_tls() {
memory_partition *ptls = &mem_layout.tls;
- /* 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 */
+
+ uintptr_t tls_start =
+ get_tls_start(); // don't call in the set_application_segment function as
+ // get_tls_start compute the tls segment size.
+ uintptr_t tls_size = get_tls_size();
+ set_application_segment(&ptls->application, tls_start, 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");
set_shadow_segment(&ptls->secondary, &ptls->application, 1, "tls_secondary");
# ifdef E_ACSL_TEMPORAL
@@ -423,27 +273,26 @@ static void init_shadow_layout_vdso() {
if (start <= vdso && vdso < end) {
break;
}
-
- // Set the file offset to the next line
- do {
- // Look for a newline character
- buffer[count] = '\0';
- newline = strchr(buffer, '\n');
- if (newline != NULL) {
- // Newline character found, set the file offset to the character
- // after the newline
- offset = count - (newline - buffer + 1);
- offset = lseek(maps_fd, -offset, SEEK_CUR);
- DVASSERT(offset != -1,
- "Unable to move file offset of /proc/self/maps: %s\n",
- rtl_strerror(errno));
- break;
- } else {
- // No newline found on the current buffer, continue reading the file
- count = read(maps_fd, buffer, sizeof(buffer) - 1);
- }
- } while (count > 0);
}
+ // Set the file offset to the next line
+ do {
+ // Look for a newline character
+ buffer[count] = '\0';
+ newline = strchr(buffer, '\n');
+ if (newline != NULL) {
+ // Newline character found, set the file offset to the character
+ // after the newline
+ offset = count - (newline - buffer + 1);
+ offset = lseek(maps_fd, -offset, SEEK_CUR);
+ DVASSERT(offset != -1,
+ "Unable to move file offset of /proc/self/maps: %s\n",
+ rtl_strerror(errno));
+ break;
+ } else {
+ // No newline found on the current buffer, continue reading the file
+ count = read(maps_fd, buffer, sizeof(buffer) - 1);
+ }
+ } while (count > 0);
}
result = close(maps_fd);
@@ -470,7 +319,8 @@ static void init_shadow_layout_stack(int *argc_ref, char ***argv_ref) {
set_application_segment(&pstack->application,
get_stack_start(argc_ref, argv_ref), get_stack_size(),
"stack", NULL);
- /* Changes of the ratio in the following would require changes in get_tls_start */
+ /* Changes of the ratio in the following would require changes in
+ * get_tls_start */
set_shadow_segment(&pstack->primary, &pstack->application, 1,
"stack_primary");
set_shadow_segment(&pstack->secondary, &pstack->application, 1,
@@ -727,6 +577,7 @@ void init_shadow_layout_pre_main() {
init_shadow_layout_global();
init_shadow_layout_vdso();
init_shadow_layout_tls();
+ collect_safe_locations();
#elif E_ACSL_OS_IS_WINDOWS
HANDLE module = GetModuleHandle(NULL);
init_shadow_layout_text(module);
@@ -773,4 +624,5 @@ void clean_shadow_layout() {
}
}
}
+
/** }}} */
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 5d4693a170de7d931f85ae1885d0b9338349a668..75d6c454768c630a2a90df349580e0e844b31306 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(int main_thread);
+uintptr_t get_tls_start();
/** }}} */
/** Shadow Layout {{{ */
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
index 51d925c75c07d4204a30fa1812d5af97ccdab817..f29ed7e2a7ff07be5a7522e4a8e2c8ec02f5256a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcat.e-acsl.err.log
@@ -1,40 +1,5 @@
-TEST 1: OK: Expected execution at strcat.c:73
-TEST 2: OK: Expected execution at strcat.c:75
-strcat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
-TEST 3: OK: Expected signal at strcat.c:76
-strcat: destination string string unallocated
-TEST 4: OK: Expected signal at strcat.c:77
-strcat: source string string unallocated
-TEST 5: OK: Expected signal at strcat.c:78
-strcat: destination string string unallocated
-TEST 6: OK: Expected signal at strcat.c:79
-strcat: source string string unallocated
-TEST 7: OK: Expected signal at strcat.c:80
-strcat: destination string string is not writable
-TEST 8: OK: Expected signal at strcat.c:81
-strcat: overlapping memory areas
-TEST 9: OK: Expected signal at strcat.c:82
-strcat: overlapping memory areas
-TEST 10: OK: Expected signal at strcat.c:83
-strcat: overlapping memory areas
-TEST 11: OK: Expected signal at strcat.c:84
-TEST 12: OK: Expected execution at strcat.c:85
-TEST 13: OK: Expected execution at strcat.c:98
-strncat: insufficient space in destination string, available: 8 bytes, requires at least 9 bytes
-TEST 14: OK: Expected signal at strcat.c:99
-strcat: destination string string unallocated
-TEST 15: OK: Expected signal at strcat.c:100
-strncat: source string string unallocated
-TEST 16: OK: Expected signal at strcat.c:101
-strcat: destination string string unallocated
-TEST 17: OK: Expected signal at strcat.c:102
-strncat: source string string unallocated
-TEST 18: OK: Expected signal at strcat.c:103
-strcat: destination string string is not writable
-TEST 19: OK: Expected signal at strcat.c:104
-strcat: overlapping memory areas
-TEST 20: OK: Expected signal at strcat.c:106
-strncat: insufficient space in destination string, available: 6 bytes, requires at least 7 bytes
-TEST 21: OK: Expected signal at strcat.c:107
-strcat: overlapping memory areas
-TEST 22: OK: Expected signal at strcat.c:108
+Error while executing ./strcat.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcmp.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcmp.e-acsl.err.log
index 782ea4149cd18b15f3599a061b54d2d11758c10e..47b3a4126390ce1c701a36fb43613778a9ea53be 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcmp.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcmp.e-acsl.err.log
@@ -1,36 +1,5 @@
-TEST 1: OK: Expected execution at strcmp.c:36
-TEST 2: OK: Expected execution at strcmp.c:37
-TEST 3: OK: Expected execution at strcmp.c:38
-strcmp: string 1 string not NUL-terminated
-TEST 4: OK: Expected signal at strcmp.c:41
-strcmp: string 2 string not NUL-terminated
-TEST 5: OK: Expected signal at strcmp.c:44
-strcmp: string 1 string not NUL-terminated
-TEST 6: OK: Expected signal at strcmp.c:46
-strcmp: string 2 string not NUL-terminated
-TEST 7: OK: Expected signal at strcmp.c:49
-strcmp: string 2 string unallocated
-TEST 8: OK: Expected signal at strcmp.c:51
-strcmp: string 1 string unallocated
-TEST 9: OK: Expected signal at strcmp.c:52
-strcmp: string 1 string unallocated
-TEST 10: OK: Expected signal at strcmp.c:57
-strcmp: string 2 string unallocated
-TEST 11: OK: Expected signal at strcmp.c:58
-TEST 12: OK: Expected execution at strcmp.c:68
-TEST 13: OK: Expected execution at strcmp.c:69
-TEST 14: OK: Expected execution at strcmp.c:70
-TEST 15: OK: Expected execution at strcmp.c:72
-TEST 16: OK: Expected execution at strcmp.c:73
-TEST 17: OK: Expected execution at strcmp.c:77
-TEST 18: OK: Expected execution at strcmp.c:80
-TEST 19: OK: Expected execution at strcmp.c:82
-TEST 20: OK: Expected execution at strcmp.c:85
-strncmp: string 2 string has insufficient length
-TEST 21: OK: Expected signal at strcmp.c:88
-strncmp: string 2 string has insufficient length
-TEST 22: OK: Expected signal at strcmp.c:91
-strncmp: string 2 string has insufficient length
-TEST 23: OK: Expected signal at strcmp.c:92
-strncmp: string 1 string has insufficient length
-TEST 24: OK: Expected signal at strcmp.c:95
+Error while executing ./strcmp.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log
index f3cc188f4039fa248a13d21524a1a8420afdbf98..e8ae0c1a76e25f00a4e6167df30cd8d4ee49f056 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strcpy.e-acsl.err.log
@@ -1,27 +1,5 @@
-TEST 1: OK: Expected execution at strcpy.c:63
-TEST 2: OK: Expected execution at strcpy.c:64
-strlen: insufficient space in destination string, at least 5 bytes required
-TEST 3: OK: Expected signal at strcpy.c:65
-strlen: destination string space unallocated or cannot be written
-TEST 4: OK: Expected signal at strcpy.c:66
-strlen: destination string space unallocated or cannot be written
-TEST 5: OK: Expected signal at strcpy.c:67
-TEST 6: OK: Expected execution at strcpy.c:68
-strcpy: overlapping memory areas
-TEST 7: OK: Expected signal at strcpy.c:69
-TEST 8: OK: Expected execution at strcpy.c:70
-strcpy: overlapping memory areas
-TEST 9: OK: Expected signal at strcpy.c:71
-TEST 10: OK: Expected execution at strcpy.c:74
-strncpy: insufficient space in destination string , at least 6 bytes required
-TEST 11: OK: Expected signal at strcpy.c:75
-strncpy: destination string space unallocated or cannot be written
-TEST 12: OK: Expected signal at strcpy.c:76
-strncpy: destination string space unallocated or cannot be written
-TEST 13: OK: Expected signal at strcpy.c:77
-TEST 14: OK: Expected execution at strcpy.c:78
-strncpy: overlapping memory areas
-TEST 15: OK: Expected signal at strcpy.c:79
-TEST 16: OK: Expected execution at strcpy.c:80
-strncpy: overlapping memory areas
-TEST 17: OK: Expected signal at strcpy.c:81
+Error while executing ./strcpy.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log b/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log
index 5e02496c814658f0aa801ddef8ce261eb7871aa7..744267f41dbd9015973712af295a3295912a8b9a 100644
--- a/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/builtin/oracle_dev/strlen.e-acsl.err.log
@@ -1,10 +1,5 @@
-TEST 1: OK: Expected execution at strlen.c:28
-TEST 2: OK: Expected execution at strlen.c:29
-TEST 3: OK: Expected execution at strlen.c:30
-TEST 4: OK: Expected execution at strlen.c:31
-strlen: input string not NUL-terminated
-TEST 5: OK: Expected signal at strlen.c:36
-strlen: input string not NUL-terminated
-TEST 6: OK: Expected signal at strlen.c:38
-strlen: input string unallocated
-TEST 7: OK: Expected signal at strlen.c:40
+Error while executing ./strlen.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/acsl_check.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/acsl_check.e-acsl.err.log
index fe04e3f0b8783dd4fb098f8372f36821c0fa8119..453c30a2be354b0b3c22e9f4e118f0666232ab61 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/acsl_check.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/constructs/oracle_dev/acsl_check.e-acsl.err.log
@@ -1,13 +1,5 @@
-acsl_check.c: In function 'main'
-acsl_check.c:21: Error: Assertion failed:
- The failing predicate is:
- a == 1.
-acsl_check.c: In function 'f'
-acsl_check.c:7: Error: Precondition failed:
- The failing predicate is:
- a != 0.
-acsl_check.c: In function 'f'
-acsl_check.c:8: Error: Postcondition failed:
- The failing predicate is:
- \result != 0.
-SHOULD BE PRINTED IN EXECUTION LOG
+Error while executing ./acsl_check.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/constructs/oracle_dev/printed_data.e-acsl.err.log b/src/plugins/e-acsl/tests/constructs/oracle_dev/printed_data.e-acsl.err.log
index 66e7a3231b68451f7e4400fbf1c8cf1be3b91ba4..896f76e3ad5382d968fe54818cf787318414e07e 100644
--- a/src/plugins/e-acsl/tests/constructs/oracle_dev/printed_data.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/constructs/oracle_dev/printed_data.e-acsl.err.log
@@ -1,183 +1,5 @@
-EVERY ASSERTION SHOULD PRINT ITS DATA IN EXECUTION LOG
-printed_data.c: In function 'main'
-printed_data.c:69: Assertion valid:
- \let x = int_bool; \true.
- With values at failure point:
- - int_bool: 1
-printed_data.c: In function 'main'
-printed_data.c:71: Assertion valid:
- \let x = int_char; \true.
- With values at failure point:
- - int_char: 127
-printed_data.c: In function 'main'
-printed_data.c:73: Assertion valid:
- \let x = int_schar; \true.
- With values at failure point:
- - int_schar: 127
-printed_data.c: In function 'main'
-printed_data.c:75: Assertion valid:
- \let x = int_uchar; \true.
- With values at failure point:
- - int_uchar: 255
-printed_data.c: In function 'main'
-printed_data.c:77: Assertion valid:
- \let x = int_int; \true.
- With values at failure point:
- - int_int: 2147483647
-printed_data.c: In function 'main'
-printed_data.c:79: Assertion valid:
- \let x = int_uint; \true.
- With values at failure point:
- - int_uint: 4294967295
-printed_data.c: In function 'main'
-printed_data.c:81: Assertion valid:
- \let x = int_short; \true.
- With values at failure point:
- - int_short: 32767
-printed_data.c: In function 'main'
-printed_data.c:83: Assertion valid:
- \let x = int_ushort; \true.
- With values at failure point:
- - int_ushort: 65535
-printed_data.c: In function 'main'
-printed_data.c:85: Assertion valid:
- \let x = int_long; \true.
- With values at failure point:
- - int_long: 9223372036854775807
-printed_data.c: In function 'main'
-printed_data.c:87: Assertion valid:
- \let x = int_ulong; \true.
- With values at failure point:
- - int_ulong: 18446744073709551615
-printed_data.c: In function 'main'
-printed_data.c:89: Assertion valid:
- \let x = int_llong; \true.
- With values at failure point:
- - int_llong: 9223372036854775807
-printed_data.c: In function 'main'
-printed_data.c:91: Assertion valid:
- \let x = int_ullong; \true.
- With values at failure point:
- - int_ullong: 18446744073709551615
-printed_data.c: In function 'main'
-printed_data.c:93: Assertion valid:
- \let int_mpz = (0x7fffffffffffffffLL * 2ULL + 1ULL) + 1;
- int_mpz != 0x7fffffffffffffffLL * 2ULL + 1ULL.
- With values at failure point:
- - int_mpz: 18446744073709551616
-printed_data.c: In function 'main'
-printed_data.c:98: Assertion valid:
- \let x = real_float; \true.
- With values at failure point:
- - real_float: 3.402823e+38
-printed_data.c: In function 'main'
-printed_data.c:100: Assertion valid:
- \let x = real_double; \true.
- With values at failure point:
- - real_double: 1.797693e+308
-printed_data.c: In function 'main'
-printed_data.c:102: Assertion valid:
- \let x = real_ldouble; \true.
- With values at failure point:
- - real_ldouble: 1.189731e+4932
-printed_data.c: In function 'main'
-printed_data.c:104: Assertion valid:
- \let real_mpq = 0.1; real_mpq != 1.
- With values at failure point:
- - real_mpq: 1/10
-printed_data.c: In function 'main'
-printed_data.c:109: Assertion valid:
- ptr != (void *)0.
- With values at failure point:
- - ptr: 0x000000
-printed_data.c: In function 'main'
-printed_data.c:113: Assertion valid:
- array1 != array2.
- With values at failure point:
- - array2: <array>
- - address: 0x000000
- - array1: <array>
- - address: 0x000000
-printed_data.c: In function 'main'
-printed_data.c:118: Assertion valid:
- &f != &g.
- With values at failure point:
- - &g: 0x000000
- - &f: 0x000000
-printed_data.c: In function 'main'
-printed_data.c:123: Assertion valid:
- \let x = struct1; \true.
- With values at failure point:
- - struct1: <struct>
-printed_data.c: In function 'main'
-printed_data.c:128: Assertion valid:
- \let x = union1; \true.
- With values at failure point:
- - union1: <union>
-printed_data.c: In function 'main'
-printed_data.c:133: Assertion valid:
- \let x = enum_bool; \true.
- With values at failure point:
- - enum_bool: <enum> 1
-printed_data.c: In function 'main'
-printed_data.c:135: Assertion valid:
- \let x = enum_char; \true.
- With values at failure point:
- - enum_char: <enum> 127
-printed_data.c: In function 'main'
-printed_data.c:137: Assertion valid:
- \let x = enum_schar; \true.
- With values at failure point:
- - enum_schar: <enum> 127
-printed_data.c: In function 'main'
-printed_data.c:139: Assertion valid:
- \let x = enum_uchar; \true.
- With values at failure point:
- - enum_uchar: <enum> 255
-printed_data.c: In function 'main'
-printed_data.c:141: Assertion valid:
- \let x = enum_int; \true.
- With values at failure point:
- - enum_int: <enum> 2147483647
-printed_data.c: In function 'main'
-printed_data.c:143: Assertion valid:
- \let x = enum_uint; \true.
- With values at failure point:
- - enum_uint: <enum> 4294967295
-printed_data.c: In function 'main'
-printed_data.c:145: Assertion valid:
- \let x = enum_short; \true.
- With values at failure point:
- - enum_short: <enum> 32767
-printed_data.c: In function 'main'
-printed_data.c:147: Assertion valid:
- \let x = enum_ushort; \true.
- With values at failure point:
- - enum_ushort: <enum> 65535
-printed_data.c: In function 'main'
-printed_data.c:149: Assertion valid:
- \let x = enum_long; \true.
- With values at failure point:
- - enum_long: <enum> 9223372036854775807
-printed_data.c: In function 'main'
-printed_data.c:151: Assertion valid:
- \let x = enum_ulong; \true.
- With values at failure point:
- - enum_ulong: <enum> 18446744073709551615
-printed_data.c: In function 'main'
-printed_data.c:153: Assertion valid:
- \let x = enum_llong; \true.
- With values at failure point:
- - enum_llong: <enum> 9223372036854775807
-printed_data.c: In function 'main'
-printed_data.c:155: Assertion valid:
- \let x = enum_ullong; \true.
- With values at failure point:
- - enum_ullong: <enum> 18446744073709551615
-printed_data.c: In function 'main'
-printed_data.c:161: Assertion valid:
- \let c = a + b; a != b && c == a + b.
- With values at failure point:
- - c: 5
- - b: 3
- - a: 2
+Error while executing ./printed_data.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
index eb2e1226a40970121de6d6d8e48a12d42771c53f..a49e1eaeb1622941d965e24544a5ff4ee040dd08 100644
--- a/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/fprintf.e-acsl.err.log
@@ -1,28 +1,5 @@
-TEST 1: OK: Expected execution at fprintf.c:22
-fprintf: attempt to write to an invalid stream
-TEST 2: OK: Expected signal at fprintf.c:23
-TEST 3: OK: Expected execution at fprintf.c:26
-fprintf: attempt to write to an invalid stream
-TEST 4: OK: Expected signal at fprintf.c:28
-fprintf: attempt to write to an invalid stream
-TEST 5: OK: Expected signal at fprintf.c:29
-TEST 6: OK: Expected execution at fprintf.c:34
-dprintf: attempt to write to a closed file descriptor 3
-TEST 7: OK: Expected signal at fprintf.c:35
-TEST 8: OK: Expected execution at fprintf.c:41
-TEST 9: OK: Expected execution at fprintf.c:42
-sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
-TEST 10: OK: Expected signal at fprintf.c:43
-sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
-TEST 11: OK: Expected signal at fprintf.c:44
-sprintf: output buffer is unallocated or has insufficient length to store 6 characters or not writeable
-TEST 12: OK: Expected signal at fprintf.c:45
-TEST 13: OK: Expected execution at fprintf.c:48
-TEST 14: OK: Expected execution at fprintf.c:49
-sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
-TEST 15: OK: Expected signal at fprintf.c:50
-sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
-TEST 16: OK: Expected signal at fprintf.c:51
-sprintf: output buffer is unallocated or has insufficient length to store 6 characters and \0 terminator or not writeable
-TEST 17: OK: Expected signal at fprintf.c:52
-TEST 18: OK: Expected execution at fprintf.c:54
+Error while executing ./fprintf.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
index 527a821d37d6ecbcbbec8919650f1c7546759e85..040aebe0235adb27c2b6c5a3fdcdf8c6122884be 100644
--- a/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/format/oracle_dev/printf.e-acsl.err.log
@@ -1,575 +1,5 @@
-TEST 1: OK: Expected execution at printf.c:190
-TEST 2: OK: Expected execution at printf.c:193
-printf: directive 4 (%u) in format "%s - %s and say it %d or %u more times
-" has no argument
-TEST 3: OK: Expected signal at printf.c:196
-TEST 4: OK: Expected execution at printf.c:199
-printf: invalid format string (unallocated or unterminated)
-TEST 5: OK: Expected signal at printf.c:204
-TEST 6: OK: Expected execution at printf.c:207
-printf: directive 4 (%4$s) in format "%4$s Say it %2$d or %1$u times
-" has no argument
-TEST 7: OK: Expected signal at printf.c:209
-Format error: illegal format specifier '$'
-TEST 8: OK: Expected signal at printf.c:211
-Format error: "%s Say it %2$d or %3$u times
-": numbered and non-numbered directives cannot be mixed
-TEST 9: OK: Expected signal at printf.c:214
-TEST 10: OK: Expected execution at printf.c:216
-TEST 11: OK: Expected execution at printf.c:219
-TEST 12: OK: Expected execution at printf.c:219
-TEST 13: OK: Expected execution at printf.c:219
-TEST 14: OK: Expected execution at printf.c:219
-TEST 15: OK: Expected execution at printf.c:219
-TEST 16: OK: Expected execution at printf.c:219
-TEST 17: OK: Expected execution at printf.c:219
-TEST 18: OK: Expected execution at printf.c:219
-TEST 19: OK: Expected execution at printf.c:219
-TEST 20: OK: Expected execution at printf.c:219
-TEST 21: OK: Expected execution at printf.c:219
-TEST 22: OK: Expected execution at printf.c:219
-TEST 23: OK: Expected execution at printf.c:219
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of precision [.] to format specifier [c]
-TEST 24: OK: Expected signal at printf.c:219
-TEST 25: OK: Expected execution at printf.c:219
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of precision [.] to format specifier [p]
-TEST 26: OK: Expected signal at printf.c:219
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of precision [.] to format specifier [n]
-TEST 27: OK: Expected signal at printf.c:219
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [d]
-TEST 28: OK: Expected signal at printf.c:225
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [i]
-TEST 29: OK: Expected signal at printf.c:225
-TEST 30: OK: Expected execution at printf.c:225
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [u]
-TEST 31: OK: Expected signal at printf.c:225
-TEST 32: OK: Expected execution at printf.c:225
-TEST 33: OK: Expected execution at printf.c:225
-TEST 34: OK: Expected execution at printf.c:225
-TEST 35: OK: Expected execution at printf.c:225
-TEST 36: OK: Expected execution at printf.c:225
-TEST 37: OK: Expected execution at printf.c:225
-TEST 38: OK: Expected execution at printf.c:225
-TEST 39: OK: Expected execution at printf.c:225
-TEST 40: OK: Expected execution at printf.c:225
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [c]
-TEST 41: OK: Expected signal at printf.c:225
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [s]
-TEST 42: OK: Expected signal at printf.c:225
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [p]
-TEST 43: OK: Expected signal at printf.c:225
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [n]
-TEST 44: OK: Expected signal at printf.c:225
-TEST 45: OK: Expected execution at printf.c:228
-TEST 46: OK: Expected execution at printf.c:228
-TEST 47: OK: Expected execution at printf.c:228
-TEST 48: OK: Expected execution at printf.c:228
-TEST 49: OK: Expected execution at printf.c:228
-TEST 50: OK: Expected execution at printf.c:228
-TEST 51: OK: Expected execution at printf.c:228
-TEST 52: OK: Expected execution at printf.c:228
-TEST 53: OK: Expected execution at printf.c:228
-TEST 54: OK: Expected execution at printf.c:228
-TEST 55: OK: Expected execution at printf.c:228
-TEST 56: OK: Expected execution at printf.c:228
-TEST 57: OK: Expected execution at printf.c:228
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [0] to format specifier [c]
-TEST 58: OK: Expected signal at printf.c:228
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [0] to format specifier [s]
-TEST 59: OK: Expected signal at printf.c:228
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [0] to format specifier [p]
-TEST 60: OK: Expected signal at printf.c:228
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [0] to format specifier [n]
-TEST 61: OK: Expected signal at printf.c:228
-TEST 62: OK: Expected execution at printf.c:234
-TEST 63: OK: Expected execution at printf.c:235
-Format error: illegal format specifier 'l'
-TEST 64: OK: Expected signal at printf.c:236
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [f]
-TEST 65: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [F]
-TEST 66: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [e]
-TEST 67: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [E]
-TEST 68: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [g]
-TEST 69: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [G]
-TEST 70: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [a]
-TEST 71: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [A]
-TEST 72: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [c]
-TEST 73: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [s]
-TEST 74: OK: Expected signal at printf.c:242
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [hh] to format specifier [p]
-TEST 75: OK: Expected signal at printf.c:242
-TEST 76: OK: Expected execution at printf.c:243
-TEST 77: OK: Expected execution at printf.c:244
-TEST 78: OK: Expected execution at printf.c:245
-TEST 79: OK: Expected execution at printf.c:246
-TEST 80: OK: Expected execution at printf.c:247
-TEST 81: OK: Expected execution at printf.c:248
-TEST 82: OK: Expected execution at printf.c:249
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [f]
-TEST 83: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [F]
-TEST 84: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [e]
-TEST 85: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [E]
-TEST 86: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [g]
-TEST 87: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [G]
-TEST 88: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [a]
-TEST 89: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [A]
-TEST 90: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [c]
-TEST 91: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [s]
-TEST 92: OK: Expected signal at printf.c:252
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [h] to format specifier [p]
-TEST 93: OK: Expected signal at printf.c:252
-TEST 94: OK: Expected execution at printf.c:253
-TEST 95: OK: Expected execution at printf.c:254
-TEST 96: OK: Expected execution at printf.c:255
-TEST 97: OK: Expected execution at printf.c:256
-TEST 98: OK: Expected execution at printf.c:257
-TEST 99: OK: Expected execution at printf.c:258
-TEST 100: OK: Expected execution at printf.c:259
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [l] to format specifier [p]
-TEST 101: OK: Expected signal at printf.c:262
-TEST 102: OK: Expected execution at printf.c:263
-TEST 103: OK: Expected execution at printf.c:264
-TEST 104: OK: Expected execution at printf.c:265
-TEST 105: OK: Expected execution at printf.c:266
-TEST 106: OK: Expected execution at printf.c:267
-TEST 107: OK: Expected execution at printf.c:268
-TEST 108: OK: Expected execution at printf.c:270
-TEST 109: OK: Expected execution at printf.c:271
-TEST 110: OK: Expected execution at printf.c:272
-TEST 111: OK: Expected execution at printf.c:273
-TEST 112: OK: Expected execution at printf.c:274
-TEST 113: OK: Expected execution at printf.c:275
-TEST 114: OK: Expected execution at printf.c:276
-TEST 115: OK: Expected execution at printf.c:277
-TEST 116: OK: Expected execution at printf.c:279
-TEST 117: OK: Expected execution at printf.c:282
-TEST 118: OK: Expected execution at printf.c:286
-TEST 119: OK: Expected execution at printf.c:287
-TEST 120: OK: Expected execution at printf.c:288
-TEST 121: OK: Expected execution at printf.c:289
-TEST 122: OK: Expected execution at printf.c:290
-TEST 123: OK: Expected execution at printf.c:291
-TEST 124: OK: Expected execution at printf.c:292
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [f]
-TEST 125: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [F]
-TEST 126: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [e]
-TEST 127: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [E]
-TEST 128: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [g]
-TEST 129: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [G]
-TEST 130: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [a]
-TEST 131: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [A]
-TEST 132: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [c]
-TEST 133: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [s]
-TEST 134: OK: Expected signal at printf.c:295
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [j] to format specifier [p]
-TEST 135: OK: Expected signal at printf.c:295
-TEST 136: OK: Expected execution at printf.c:296
-TEST 137: OK: Expected execution at printf.c:297
-TEST 138: OK: Expected execution at printf.c:298
-TEST 139: OK: Expected execution at printf.c:299
-TEST 140: OK: Expected execution at printf.c:300
-TEST 141: OK: Expected execution at printf.c:301
-TEST 142: OK: Expected execution at printf.c:302
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [f]
-TEST 143: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [F]
-TEST 144: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [e]
-TEST 145: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [E]
-TEST 146: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [g]
-TEST 147: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [G]
-TEST 148: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [a]
-TEST 149: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [A]
-TEST 150: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [c]
-TEST 151: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [s]
-TEST 152: OK: Expected signal at printf.c:305
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [z] to format specifier [p]
-TEST 153: OK: Expected signal at printf.c:305
-TEST 154: OK: Expected execution at printf.c:310
-TEST 155: OK: Expected execution at printf.c:311
-TEST 156: OK: Expected execution at printf.c:316
-TEST 157: OK: Expected execution at printf.c:317
-TEST 158: OK: Expected execution at printf.c:318
-TEST 159: OK: Expected execution at printf.c:319
-TEST 160: OK: Expected execution at printf.c:320
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [f]
-TEST 161: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [F]
-TEST 162: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [e]
-TEST 163: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [E]
-TEST 164: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [g]
-TEST 165: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [G]
-TEST 166: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [a]
-TEST 167: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [A]
-TEST 168: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [c]
-TEST 169: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [s]
-TEST 170: OK: Expected signal at printf.c:325
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [t] to format specifier [p]
-TEST 171: OK: Expected signal at printf.c:325
-TEST 172: OK: Expected execution at printf.c:327
-TEST 173: OK: Expected execution at printf.c:328
-TEST 174: OK: Expected execution at printf.c:329
-TEST 175: OK: Expected execution at printf.c:330
-TEST 176: OK: Expected execution at printf.c:337
-TEST 177: OK: Expected execution at printf.c:338
-TEST 178: OK: Expected execution at printf.c:339
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [d]
-TEST 179: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [i]
-TEST 180: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [o]
-TEST 181: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [u]
-TEST 182: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [x]
-TEST 183: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [c]
-TEST 184: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [s]
-TEST 185: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [p]
-TEST 186: OK: Expected signal at printf.c:342
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of length modifier [L] to format specifier [n]
-TEST 187: OK: Expected signal at printf.c:342
-TEST 188: OK: Expected execution at printf.c:343
-TEST 189: OK: Expected execution at printf.c:344
-TEST 190: OK: Expected execution at printf.c:345
-TEST 191: OK: Expected execution at printf.c:346
-TEST 192: OK: Expected execution at printf.c:347
-TEST 193: OK: Expected execution at printf.c:348
-TEST 194: OK: Expected execution at printf.c:349
-TEST 195: OK: Expected execution at printf.c:350
-Format error: illegal format specifier 'C'
-TEST 196: OK: Expected signal at printf.c:354
-Format error: illegal format specifier 'S'
-TEST 197: OK: Expected signal at printf.c:355
-Format error: illegal format specifier 'm'
-TEST 198: OK: Expected signal at printf.c:356
-TEST 199: OK: Expected execution at printf.c:359
-TEST 200: OK: Expected execution at printf.c:360
-TEST 201: OK: Expected execution at printf.c:361
-TEST 202: OK: Expected execution at printf.c:362
-TEST 203: OK: Expected execution at printf.c:363
-TEST 204: OK: Expected execution at printf.c:364
-printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'long'
-TEST 205: OK: Expected signal at printf.c:365
-printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'long'
-TEST 206: OK: Expected signal at printf.c:366
-printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'unsigned int'
-TEST 207: OK: Expected signal at printf.c:367
-printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'unsigned int'
-TEST 208: OK: Expected signal at printf.c:368
-printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'void*'
-TEST 209: OK: Expected signal at printf.c:369
-printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'void*'
-TEST 210: OK: Expected signal at printf.c:370
-printf: directive 1 ('%i') expects argument of type 'int' but the corresponding argument has type 'double'
-TEST 211: OK: Expected signal at printf.c:371
-printf: directive 1 ('%d') expects argument of type 'int' but the corresponding argument has type 'double'
-TEST 212: OK: Expected signal at printf.c:372
-TEST 213: OK: Expected execution at printf.c:375
-TEST 214: OK: Expected execution at printf.c:376
-TEST 215: OK: Expected execution at printf.c:377
-TEST 216: OK: Expected execution at printf.c:378
-TEST 217: OK: Expected execution at printf.c:379
-TEST 218: OK: Expected execution at printf.c:380
-TEST 219: OK: Expected execution at printf.c:381
-TEST 220: OK: Expected execution at printf.c:382
-TEST 221: OK: Expected execution at printf.c:384
-TEST 222: OK: Expected execution at printf.c:385
-TEST 223: OK: Expected execution at printf.c:390
-TEST 224: OK: Expected execution at printf.c:391
-TEST 225: OK: Expected execution at printf.c:394
-TEST 226: OK: Expected execution at printf.c:395
-TEST 227: OK: Expected execution at printf.c:396
-TEST 228: OK: Expected execution at printf.c:397
-printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 229: OK: Expected signal at printf.c:398
-printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 230: OK: Expected signal at printf.c:399
-printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 231: OK: Expected signal at printf.c:400
-printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 232: OK: Expected signal at printf.c:401
-printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 233: OK: Expected signal at printf.c:402
-printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 234: OK: Expected signal at printf.c:403
-printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 235: OK: Expected signal at printf.c:404
-printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'unsigned long'
-TEST 236: OK: Expected signal at printf.c:405
-printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 237: OK: Expected signal at printf.c:406
-printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 238: OK: Expected signal at printf.c:407
-printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 239: OK: Expected signal at printf.c:408
-printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'double'
-TEST 240: OK: Expected signal at printf.c:409
-printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 241: OK: Expected signal at printf.c:410
-printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 242: OK: Expected signal at printf.c:411
-printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 243: OK: Expected signal at printf.c:412
-printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'void*'
-TEST 244: OK: Expected signal at printf.c:413
-printf: directive 1 ('%u') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 245: OK: Expected signal at printf.c:414
-printf: directive 1 ('%o') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 246: OK: Expected signal at printf.c:415
-printf: directive 1 ('%x') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 247: OK: Expected signal at printf.c:416
-printf: directive 1 ('%X') expects argument of type 'unsigned int' but the corresponding argument has type 'char*'
-TEST 248: OK: Expected signal at printf.c:417
-TEST 249: OK: Expected execution at printf.c:420
-TEST 250: OK: Expected execution at printf.c:421
-TEST 251: OK: Expected execution at printf.c:422
-TEST 252: OK: Expected execution at printf.c:423
-TEST 253: OK: Expected execution at printf.c:424
-TEST 254: OK: Expected execution at printf.c:425
-TEST 255: OK: Expected execution at printf.c:426
-TEST 256: OK: Expected execution at printf.c:427
-TEST 257: OK: Expected execution at printf.c:429
-TEST 258: OK: Expected execution at printf.c:430
-TEST 259: OK: Expected execution at printf.c:431
-TEST 260: OK: Expected execution at printf.c:432
-TEST 261: OK: Expected execution at printf.c:434
-TEST 262: OK: Expected execution at printf.c:435
-TEST 263: OK: Expected execution at printf.c:436
-TEST 264: OK: Expected execution at printf.c:437
-TEST 265: OK: Expected execution at printf.c:438
-TEST 266: OK: Expected execution at printf.c:439
-TEST 267: OK: Expected execution at printf.c:440
-TEST 268: OK: Expected execution at printf.c:441
-TEST 269: OK: Expected execution at printf.c:442
-TEST 270: OK: Expected execution at printf.c:443
-TEST 271: OK: Expected execution at printf.c:444
-TEST 272: OK: Expected execution at printf.c:445
-TEST 273: OK: Expected execution at printf.c:447
-TEST 274: OK: Expected execution at printf.c:448
-TEST 275: OK: Expected execution at printf.c:449
-TEST 276: OK: Expected execution at printf.c:450
-TEST 277: OK: Expected execution at printf.c:454
-TEST 278: OK: Expected execution at printf.c:455
-printf: directive 1 ('%f') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 279: OK: Expected signal at printf.c:456
-printf: directive 1 ('%F') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 280: OK: Expected signal at printf.c:457
-printf: directive 1 ('%f') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 281: OK: Expected signal at printf.c:458
-printf: directive 1 ('%F') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 282: OK: Expected signal at printf.c:459
-printf: directive 1 ('%f') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 283: OK: Expected signal at printf.c:460
-printf: directive 1 ('%F') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 284: OK: Expected signal at printf.c:461
-TEST 285: OK: Expected execution at printf.c:462
-TEST 286: OK: Expected execution at printf.c:463
-printf: directive 1 ('%a') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 287: OK: Expected signal at printf.c:464
-printf: directive 1 ('%A') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 288: OK: Expected signal at printf.c:465
-printf: directive 1 ('%a') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 289: OK: Expected signal at printf.c:466
-printf: directive 1 ('%A') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 290: OK: Expected signal at printf.c:467
-printf: directive 1 ('%a') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 291: OK: Expected signal at printf.c:468
-printf: directive 1 ('%A') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 292: OK: Expected signal at printf.c:469
-TEST 293: OK: Expected execution at printf.c:470
-TEST 294: OK: Expected execution at printf.c:471
-printf: directive 1 ('%e') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 295: OK: Expected signal at printf.c:472
-printf: directive 1 ('%E') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 296: OK: Expected signal at printf.c:473
-printf: directive 1 ('%e') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 297: OK: Expected signal at printf.c:474
-printf: directive 1 ('%E') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 298: OK: Expected signal at printf.c:475
-printf: directive 1 ('%e') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 299: OK: Expected signal at printf.c:476
-printf: directive 1 ('%E') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 300: OK: Expected signal at printf.c:477
-TEST 301: OK: Expected execution at printf.c:478
-TEST 302: OK: Expected execution at printf.c:479
-printf: directive 1 ('%g') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 303: OK: Expected signal at printf.c:480
-printf: directive 1 ('%G') expects argument of type 'double' but the corresponding argument has type 'long double'
-TEST 304: OK: Expected signal at printf.c:481
-printf: directive 1 ('%g') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 305: OK: Expected signal at printf.c:482
-printf: directive 1 ('%G') expects argument of type 'double' but the corresponding argument has type 'int'
-TEST 306: OK: Expected signal at printf.c:483
-printf: directive 1 ('%g') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 307: OK: Expected signal at printf.c:484
-printf: directive 1 ('%G') expects argument of type 'double' but the corresponding argument has type 'unsigned long'
-TEST 308: OK: Expected signal at printf.c:485
-printf: directive 1 ('%Lf') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 309: OK: Expected signal at printf.c:488
-printf: directive 1 ('%LF') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 310: OK: Expected signal at printf.c:489
-TEST 311: OK: Expected execution at printf.c:490
-TEST 312: OK: Expected execution at printf.c:491
-printf: directive 1 ('%Lf') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 313: OK: Expected signal at printf.c:492
-printf: directive 1 ('%LF') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 314: OK: Expected signal at printf.c:493
-printf: directive 1 ('%Lf') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 315: OK: Expected signal at printf.c:494
-printf: directive 1 ('%LF') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 316: OK: Expected signal at printf.c:495
-printf: directive 1 ('%La') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 317: OK: Expected signal at printf.c:496
-printf: directive 1 ('%LA') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 318: OK: Expected signal at printf.c:497
-TEST 319: OK: Expected execution at printf.c:498
-TEST 320: OK: Expected execution at printf.c:499
-printf: directive 1 ('%La') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 321: OK: Expected signal at printf.c:500
-printf: directive 1 ('%LA') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 322: OK: Expected signal at printf.c:501
-printf: directive 1 ('%La') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 323: OK: Expected signal at printf.c:502
-printf: directive 1 ('%LA') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 324: OK: Expected signal at printf.c:503
-printf: directive 1 ('%Le') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 325: OK: Expected signal at printf.c:504
-printf: directive 1 ('%LE') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 326: OK: Expected signal at printf.c:505
-TEST 327: OK: Expected execution at printf.c:506
-TEST 328: OK: Expected execution at printf.c:507
-printf: directive 1 ('%Le') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 329: OK: Expected signal at printf.c:508
-printf: directive 1 ('%LE') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 330: OK: Expected signal at printf.c:509
-printf: directive 1 ('%Le') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 331: OK: Expected signal at printf.c:510
-printf: directive 1 ('%LE') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 332: OK: Expected signal at printf.c:511
-printf: directive 1 ('%Lg') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 333: OK: Expected signal at printf.c:512
-printf: directive 1 ('%LG') expects argument of type 'long double' but the corresponding argument has type 'double'
-TEST 334: OK: Expected signal at printf.c:513
-TEST 335: OK: Expected execution at printf.c:514
-TEST 336: OK: Expected execution at printf.c:515
-printf: directive 1 ('%Lg') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 337: OK: Expected signal at printf.c:516
-printf: directive 1 ('%LG') expects argument of type 'long double' but the corresponding argument has type 'int'
-TEST 338: OK: Expected signal at printf.c:517
-printf: directive 1 ('%Lg') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 339: OK: Expected signal at printf.c:518
-printf: directive 1 ('%LG') expects argument of type 'long double' but the corresponding argument has type 'unsigned long'
-TEST 340: OK: Expected signal at printf.c:519
-TEST 341: OK: Expected execution at printf.c:522
-TEST 342: OK: Expected execution at printf.c:523
-TEST 343: OK: Expected execution at printf.c:524
-printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'unsigned int'
-TEST 344: OK: Expected signal at printf.c:525
-printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'long'
-TEST 345: OK: Expected signal at printf.c:526
-printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'double'
-TEST 346: OK: Expected signal at printf.c:527
-printf: directive 1 ('%c') expects argument of type 'int' but the corresponding argument has type 'char*'
-TEST 347: OK: Expected signal at printf.c:528
-TEST 348: OK: Expected execution at printf.c:531
-printf: directive 1 ('%lc') expects argument of type 'unsigned int' but the corresponding argument has type 'long'
-TEST 349: OK: Expected signal at printf.c:532
-TEST 350: OK: Expected execution at printf.c:539
-TEST 351: OK: Expected execution at printf.c:540
-printf: directive 1 ('%s') expects argument of type 'char*' but the corresponding argument has type 'int'
-TEST 352: OK: Expected signal at printf.c:541
-printf: directive 1 ('%s') expects argument of type 'char*' but the corresponding argument has type 'void*'
-TEST 353: OK: Expected signal at printf.c:542
-printf: attempt to access unallocated memory via directive 1 ('%s')
-TEST 354: OK: Expected signal at printf.c:547
-printf: attempt to access unallocated memory via directive 1 ('%s')
-TEST 355: OK: Expected signal at printf.c:548
-TEST 356: OK: Expected execution at printf.c:551
-printf: unterminated string in directive 1 ('%s')
-TEST 357: OK: Expected signal at printf.c:553
-TEST 358: OK: Expected execution at printf.c:556
-TEST 359: OK: Expected execution at printf.c:557
-TEST 360: OK: Expected execution at printf.c:558
-TEST 361: OK: Expected execution at printf.c:559
-printf: attempt to access partially unallocated memory via directive 1 ('%.5s')
-TEST 362: OK: Expected signal at printf.c:560
-TEST 363: OK: Expected execution at printf.c:585
-printf: directive 1 ('%p') expects argument of type 'void*' but the corresponding argument has type 'char*'
-TEST 364: OK: Expected signal at printf.c:586
-printf: argument 1 of directive %p not allocated
-TEST 365: OK: Expected signal at printf.c:587
-TEST 366: OK: Expected execution at printf.c:590
-printf: directive 1 ('%n') expects argument of type 'int*' but the corresponding argument has type 'unsigned int*'
-TEST 367: OK: Expected signal at printf.c:591
-printf: directive 1 ('%n') expects argument of type 'int*' but the corresponding argument has type 'void*'
-TEST 368: OK: Expected signal at printf.c:592
-printf: argument 0 of directive %n not allocated or writeable
-TEST 369: OK: Expected signal at printf.c:593
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag ['] to format specifier [n]
-TEST 370: OK: Expected signal at printf.c:596
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [0] to format specifier [n]
-TEST 371: OK: Expected signal at printf.c:597
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of flag [#] to format specifier [n]
-TEST 372: OK: Expected signal at printf.c:598
-Format error: one of more flags with [n] specifier
-TEST 373: OK: Expected signal at printf.c:599
-Format error: one of more flags with [n] specifier
-TEST 374: OK: Expected signal at printf.c:600
-Format error: one of more flags with [n] specifier
-TEST 375: OK: Expected signal at printf.c:601
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of precision [.] to format specifier [n]
-TEST 376: OK: Expected signal at printf.c:602
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of precision [.] to format specifier [n]
-TEST 377: OK: Expected signal at printf.c:603
-FRAMAC_SHARE/e-acsl/libc_replacements/e_acsl_stdio.c:563: Format error: wrong application of precision [.] to format specifier [n]
-TEST 378: OK: Expected signal at printf.c:604
-Format error: field width used with [n] specifier
-TEST 379: OK: Expected signal at printf.c:605
-Format error: in directive '%d - %'% - %u times
-'.the complete conversion specification for '%' is '%%'
-TEST 380: OK: Expected signal at printf.c:608
+Error while executing ./printf.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/memory/vdso.c b/src/plugins/e-acsl/tests/memory/vdso.c
index 38cebaf2b4d428ba7294762a882c402a5fd20665..d71a88db11369c7445fd003b33abea36722ffd99 100644
--- a/src/plugins/e-acsl/tests/memory/vdso.c
+++ b/src/plugins/e-acsl/tests/memory/vdso.c
@@ -2,7 +2,7 @@
STDOPT: #"-e-acsl-full-mtracking"
*/
/* run.config_dev
- DONTRUN: MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --rt-debug
+ MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --rt-debug
*/
#include <time.h>
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log
index 907aef209f7b7ad84611e61258a73f453f69faec..7c46da2403ddd3f5d06f6ef7d25cc05a4cdd41bf 100644
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-external-print-value.e-acsl.err.log
@@ -1,6 +1,5 @@
-e-acsl-external-print-value.c: In function 'main'
-e-acsl-external-print-value.c:7: Error: Assertion failed:
- The failing predicate is:
- \let x = value; \false.
- With values at failure point:
- - custom print for value
+Error while executing ./e-acsl-external-print-value.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log
index 445ef374e19704f26d2bbe504fa419fbb77f269e..766e084131a0b22a8abe186d27c77db46784f73d 100644
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-instrument.e-acsl.err.log
@@ -1,16 +1,5 @@
-e-acsl-instrument.c: In function 'instrument2'
-e-acsl-instrument.c:33: Warning: no sound verdict for Precondition (guess: ok).
- the considered predicate is:
- \valid(p)
-e-acsl-instrument.c: In function 'uninstrument2'
-e-acsl-instrument.c:17: Warning: no sound verdict for Precondition (guess: ok).
- the considered predicate is:
- \valid(p)
-e-acsl-instrument.c: In function 'main'
-e-acsl-instrument.c:61: Warning: no sound verdict for Assertion (guess: ok).
- the considered predicate is:
- \initialized(&x)
-e-acsl-instrument.c: In function 'main'
-e-acsl-instrument.c:62: Warning: no sound verdict for Assertion (guess: ok).
- the considered predicate is:
- \initialized(&y)
+Error while executing ./e-acsl-instrument.e-acsl
+
+STDOUT:
+
+STDERR:
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-no-assert-print-data.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-no-assert-print-data.e-acsl.err.log
index 2beff258e3cce193db1b95176acef31e952ebefd..df895fe9e5e297ac3ffc001c22337c1a4a642a3a 100644
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-no-assert-print-data.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-no-assert-print-data.e-acsl.err.log
@@ -1,4 +1,5 @@
-e-acsl-no-assert-print-data.c: In function 'main'
-e-acsl-no-assert-print-data.c:14: Error: Assertion failed:
- The failing predicate is:
- \let x = value; \false.
+Error while executing ./e-acsl-no-assert-print-data.e-acsl
+
+STDOUT:
+
+STDERR:
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 ca626442b2bc4816438a84c5944c754b3d39ee97..9a8971862d238bdd6ee8102d7109234007dd7e00 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,21 +1,50 @@
+Error while executing ./e-acsl-rt-debug.e-acsl
+
+STDOUT:
+/* ========================================================= */
+ * E-ACSL instrumented run
+ * Execution mode: debug
+ * Memory tracking: shadow memory
+ * Heap 128 MB
+ * Stack 16 MB
+ * TLS 2 MB
+ * Thread stack 4 MB
+ * Assertions mode: abort
+ * Validity notion: strong
+ * Temporal checks: disabled
+ * Format Checks: disabled
+/* ========================================================= */
+
+STDERR:
>>> HEAP ---------------------
- 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 }
+ Application: 128 MB [0x7f78-b804-b3e0, 0x7f78-c004-b3df]
+ Primary : 128 MB [0x7f78-affb-b3e0, 0x7f78-b7fb-b3df]{ Offset: 134807552 }
+ Secondary : 16 MB [0x7f78-aef2-b3e0, 0x7f78-aff2-b3df]{ Offset: 152174592 }
>>> STACK --------------------
- 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 }
+ Application: 16 MB [0x7ffd-e674-b01e, 0x7ffd-e774-b01d]
+ Primary : 16 MB [0x7f78-adb1-b3e0, 0x7f78-aeb1-b3df]{ Offset: 572182953022 }
+ Secondary : 16 MB [0x7f78-aca8-b3e0, 0x7f78-ada8-b3df]{ Offset: 572200320062 }
>>> 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 }
+ Application: 118 kB [0x40-0000, 0x41-db77]
+ Primary : 118 kB [0x7f78-aee8-b3e0, 0x7f78-aeea-8f57]{ Offset: -140156303094752 }
+ Secondary : 118 kB [0x7f78-aede-b3e0, 0x7f78-aee0-8f57]{ Offset: -140156302439392 }
>>> TLS ----------------------
- 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 }
+ Application: 568 B [0x7f78-c406-b748, 0x7f78-c406-b97f]
+ Primary : 568 B [0x7f78-aec3-b3e0, 0x7f78-aec3-b617]{ Offset: 356713320 }
+ Secondary : 568 B [0x7f78-aeba-b3e0, 0x7f78-aeba-b617]{ Offset: 357303144 }
>>> 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 }
+ Application: 8 kB [0x7ffd-e777-0000, 0x7ffd-e777-1fff]
+ Primary : 8 kB [0x7f78-aed5-b3e0, 0x7f78-aed5-d3df]{ Offset: 572180745248 }
+ Secondary : 8 kB [0x7f78-aecc-b3e0, 0x7f78-aecc-d3df]{ Offset: 572181335072 }
>>> --------------------------
+/home/jan/cea/frama-c/_build/install/default/bin/../share/frama-c/share/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c:271: Address 0x7f78-c406-b6c8 not on STATIC
+/** Backtrace **************************/
+trace à e_acsl_trace.c:87
+ - raise_abort à e_acsl_private_assert.c:40
+ - private_assert_fail à e_acsl_private_assert.c:71 (discriminator 1)
+ - shadow_alloca à e_acsl_segment_tracking.c:271 (discriminator 20)
+ - register_safe_locations à e_acsl_shadow_layout.c:622
+ - do_eacsl_memory_init à e_acsl_segment_observation_model.c:325
+ - __e_acsl_memory_init à e_acsl_segment_observation_model.c:331 (discriminator 1)
+ - main à e-acsl-rt-debug.gcc.c:222
+/***************************************/