From b46fc091160f1847d20050d4d9217c85fdedf117 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 8 Jul 2022 09:26:07 +0200
Subject: [PATCH] [e-acsl] disable non-deterministic tests on segments -
 depending on system+executions, VDSO and TLS may overlap

---
 src/plugins/e-acsl/tests/concurrency/threads_debug.c | 4 ++--
 src/plugins/e-acsl/tests/memory/vdso.c               | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/plugins/e-acsl/tests/concurrency/threads_debug.c b/src/plugins/e-acsl/tests/concurrency/threads_debug.c
index 75bf51d6121..31d748444a6 100644
--- a/src/plugins/e-acsl/tests/concurrency/threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/threads_debug.c
@@ -1,10 +1,10 @@
-/* run.config, run.config_dev
+/* run.config_dev
   COMMENT: This test is identical to `parallel_thread.c` but with RTL debug code
   COMMENT: activated.
   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/[0-9]*\sMB/xxxMB/g | sed -e s/Leaked.*bytes/Leakedxxxbytes/g
+  DONTRUN:
 */
 
 // Include existing test
diff --git a/src/plugins/e-acsl/tests/memory/vdso.c b/src/plugins/e-acsl/tests/memory/vdso.c
index d71a88db113..38cebaf2b4d 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
-  MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --rt-debug
+  DONTRUN: MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --rt-debug
 */
 
 #include <time.h>
-- 
GitLab