From 416b510d0ba456287db8b73be8983f7acabe55d0 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Fri, 10 Apr 2020 18:28:14 +0200
Subject: [PATCH] [eacsl:tests] Reactivate `temporal` tests
---
.../e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c | 4 ++--
.../e-acsl/tests/temporal/oracle_ci/gen_t_scope.c | 14 +++++++-------
.../tests/temporal/oracle_ci/t_getenv.res.oracle | 12 ++++++------
.../tests/temporal/oracle_ci/t_scope.res.oracle | 6 +++---
.../oracle_dev/t_addr-by-val.e-acsl.err.log | 0
.../temporal/oracle_dev/t_args.e-acsl.err.log | 0
.../temporal/oracle_dev/t_array.e-acsl.err.log | 0
.../temporal/oracle_dev/t_char.e-acsl.err.log | 0
.../temporal/oracle_dev/t_darray.e-acsl.err.log | 0
.../temporal/oracle_dev/t_dpointer.e-acsl.err.log | 0
.../temporal/oracle_dev/t_dpointer.res.oracle | 6 +-----
.../temporal/oracle_dev/t_fptr.e-acsl.err.log | 0
.../temporal/oracle_dev/t_fun_lib.e-acsl.err.log | 0
.../temporal/oracle_dev/t_fun_ptr.e-acsl.err.log | 0
.../temporal/oracle_dev/t_getenv.e-acsl.err.log | 0
.../oracle_dev/t_global_init.e-acsl.err.log | 0
.../temporal/oracle_dev/t_labels.e-acsl.err.log | 0
.../oracle_dev/t_lit_string.e-acsl.err.log | 0
.../oracle_dev/t_local_init.e-acsl.err.log | 0
.../oracle_dev/t_malloc-asan.e-acsl.err.log | 0
.../temporal/oracle_dev/t_malloc.e-acsl.err.log | 0
.../tests/temporal/oracle_dev/t_malloc.res.oracle | 6 +-----
.../temporal/oracle_dev/t_memcpy.e-acsl.err.log | 0
.../temporal/oracle_dev/t_scope.e-acsl.err.log | 0
.../tests/temporal/oracle_dev/t_scope.res.oracle | 7 +------
.../temporal/oracle_dev/t_struct.e-acsl.err.log | 0
.../temporal/oracle_dev/t_while.e-acsl.err.log | 0
src/plugins/e-acsl/tests/temporal/t_addr-by-val.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_args.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_array.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_char.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_darray.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_dpointer.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_fptr.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_fun_lib.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_fun_ptr.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_getenv.c | 3 ++-
src/plugins/e-acsl/tests/temporal/t_global_init.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_labels.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_lit_string.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_local_init.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_malloc-asan.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_malloc.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_scope.c | 3 ++-
src/plugins/e-acsl/tests/temporal/t_struct.c | 2 +-
src/plugins/e-acsl/tests/temporal/t_while.c | 2 +-
src/plugins/e-acsl/tests/temporal/test_config_dev | 3 +--
47 files changed, 43 insertions(+), 55 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.e-acsl.err.log
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.e-acsl.err.log
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
index 9c4df1533bf..b574f1ebb23 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
@@ -107,7 +107,7 @@ int main(int argc, char const **argv)
}
__e_acsl_assert(__gen_e_acsl_or,"Assertion","main",
"g1 == \\null || \\valid(g1)",
- "tests/temporal/t_getenv.c",13);
+ "tests/temporal/t_getenv.c",14);
}
/*@ assert g1 ≡ \null ∨ \valid(g1); */ ;
{
@@ -132,7 +132,7 @@ int main(int argc, char const **argv)
}
__e_acsl_assert(__gen_e_acsl_or_2,"Assertion","main",
"g2 == \\null || \\valid(g2)",
- "tests/temporal/t_getenv.c",14);
+ "tests/temporal/t_getenv.c",15);
}
/*@ assert g2 ≡ \null ∨ \valid(g2); */ ;
__retres = 0;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
index a0e3962c59b..8a0fc1325ad 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
@@ -39,7 +39,7 @@ int main(void)
}
else __gen_e_acsl_and = 0;
__e_acsl_assert(! __gen_e_acsl_and,"Assertion","main","!\\valid(p)",
- "tests/temporal/t_scope.c",15);
+ "tests/temporal/t_scope.c",16);
}
/*@ assert ¬\valid(p); */ ;
{
@@ -55,7 +55,7 @@ int main(void)
}
else __gen_e_acsl_and_2 = 0;
__e_acsl_assert(! __gen_e_acsl_and_2,"Assertion","main","!\\valid(q)",
- "tests/temporal/t_scope.c",16);
+ "tests/temporal/t_scope.c",17);
}
/*@ assert ¬\valid(q); */ ;
{
@@ -78,7 +78,7 @@ int main(void)
}
else __gen_e_acsl_and_3 = 0;
__e_acsl_assert(__gen_e_acsl_and_3,"Assertion","main","\\valid(p)",
- "tests/temporal/t_scope.c",21);
+ "tests/temporal/t_scope.c",22);
}
/*@ assert \valid(p); */ ;
__e_acsl_initialize((void *)p,sizeof(int));
@@ -96,7 +96,7 @@ int main(void)
}
else __gen_e_acsl_and_4 = 0;
__e_acsl_assert(! __gen_e_acsl_and_4,"Assertion","main","!\\valid(q)",
- "tests/temporal/t_scope.c",24);
+ "tests/temporal/t_scope.c",25);
}
/*@ assert ¬\valid(q); */ ;
{
@@ -104,7 +104,7 @@ int main(void)
__gen_e_acsl_valid_5 = __e_acsl_valid((void *)(& j),sizeof(int),
(void *)(& j),(void *)0);
__e_acsl_assert(__gen_e_acsl_valid_5,"Assertion","main","\\valid(&j)",
- "tests/temporal/t_scope.c",25);
+ "tests/temporal/t_scope.c",26);
}
/*@ assert \valid(&j); */ ;
__e_acsl_delete_block((void *)(& j));
@@ -132,7 +132,7 @@ int main(void)
}
else __gen_e_acsl_and_5 = 0;
__e_acsl_assert(! __gen_e_acsl_and_5,"Assertion","main","!\\valid(p)",
- "tests/temporal/t_scope.c",34);
+ "tests/temporal/t_scope.c",35);
}
/*@ assert ¬\valid(p); */ ;
__e_acsl_full_init((void *)(& q));
@@ -154,7 +154,7 @@ int main(void)
}
else __gen_e_acsl_and_6 = 0;
__e_acsl_assert(__gen_e_acsl_and_6,"Assertion","main","\\valid(p)",
- "tests/temporal/t_scope.c",37);
+ "tests/temporal/t_scope.c",38);
}
/*@ assert \valid(p); */ ;
len --;
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
index 7bd89827d09..b55cb5a92ea 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
@@ -15,13 +15,13 @@
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/stdlib.h:488: Warning:
function __gen_e_acsl_getenv: postcondition 'null_or_valid_result' got status unknown.
-[eva:alarm] tests/temporal/t_getenv.c:13: Warning:
- pointer comparison. assert \pointer_comparable((void *)g1, (void *)0);
-[eva:alarm] tests/temporal/t_getenv.c:13: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/temporal/t_getenv.c:13: Warning: assertion got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
- pointer comparison. assert \pointer_comparable((void *)g2, (void *)0);
+ pointer comparison. assert \pointer_comparable((void *)g1, (void *)0);
[eva:alarm] tests/temporal/t_getenv.c:14: Warning:
function __e_acsl_assert: precondition got status unknown.
[eva:alarm] tests/temporal/t_getenv.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
+ pointer comparison. assert \pointer_comparable((void *)g2, (void *)0);
+[eva:alarm] tests/temporal/t_getenv.c:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/temporal/t_getenv.c:15: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle
index 9826a53ef7e..058ed9b3e78 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle
@@ -1,9 +1,9 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:locals-escaping] tests/temporal/t_scope.c:10: Warning:
+[eva:locals-escaping] tests/temporal/t_scope.c:11: Warning:
locals {i} escaping the scope of a block of main through p
-[eva:locals-escaping] tests/temporal/t_scope.c:10: Warning:
+[eva:locals-escaping] tests/temporal/t_scope.c:11: Warning:
locals {i} escaping the scope of a block of main through q
-[eva:alarm] tests/temporal/t_scope.c:15: Warning:
+[eva:alarm] tests/temporal/t_scope.c:16: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_addr-by-val.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_args.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_array.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_char.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_darray.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
index 0e725129643..e636757d80c 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_dpointer.res.oracle
@@ -1,5 +1 @@
-[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
- Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
-[kernel] User Error: compilation of './tests/print.ml' failed
-[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing tests/temporal/t_dpointer.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fptr.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_lib.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_fun_ptr.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_getenv.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_global_init.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_labels.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_lit_string.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_local_init.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc-asan.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
index 0e725129643..95c70361d68 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_malloc.res.oracle
@@ -1,5 +1 @@
-[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
- Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
-[kernel] User Error: compilation of './tests/print.ml' failed
-[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing tests/temporal/t_malloc.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_memcpy.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
index 6af29643dcc..3d748d198fa 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_scope.res.oracle
@@ -1,6 +1 @@
-[kernel] User Error: cannot load plug-in 'frama-c-e_acsl': cannot load module
- Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./top/E_ACSL.cmxs: cannot open shared object file: No such file or directory\")")
-[kernel] User Error: cannot load plug-in 'print': cannot load module
- Details: error loading shared library: Dynlink.Error (Dynlink.Cannot_open_dll "Failure(\"./tests/print.cmxs: cannot open shared object file: No such file or directory\")")
-[kernel] User Error: Deferred error message was emitted during execution. See above messages for more information.
-[kernel] Frama-C aborted: invalid user input.
+[kernel] Parsing tests/temporal/t_scope.c (with preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_struct.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.e-acsl.err.log b/src/plugins/e-acsl/tests/temporal/oracle_dev/t_while.e-acsl.err.log
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
index 562cc4e026c..b847786468f 100644
--- a/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
+++ b/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Case when a pointer is taking address by value.
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_args.c b/src/plugins/e-acsl/tests/temporal/t_args.c
index c48b3e093e2..8d5a4b9a8ea 100644
--- a/src/plugins/e-acsl/tests/temporal/t_args.c
+++ b/src/plugins/e-acsl/tests/temporal/t_args.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check that command line parameters are properly tracked
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_array.c b/src/plugins/e-acsl/tests/temporal/t_array.c
index ff2e8be8362..f4166ccf69a 100644
--- a/src/plugins/e-acsl/tests/temporal/t_array.c
+++ b/src/plugins/e-acsl/tests/temporal/t_array.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check temporal timestamps of arrays
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_char.c b/src/plugins/e-acsl/tests/temporal/t_char.c
index e8f001a3a72..6cd778f7097 100644
--- a/src/plugins/e-acsl/tests/temporal/t_char.c
+++ b/src/plugins/e-acsl/tests/temporal/t_char.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check that when small blocks (such as char) are used the
COMMENT: instrumentation adds alignment sufficient for tracking
COMMENT: block origin number via shadowing
diff --git a/src/plugins/e-acsl/tests/temporal/t_darray.c b/src/plugins/e-acsl/tests/temporal/t_darray.c
index 88c1cf97120..5130ef693df 100644
--- a/src/plugins/e-acsl/tests/temporal/t_darray.c
+++ b/src/plugins/e-acsl/tests/temporal/t_darray.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Checking propagation of referent numbers in arrays
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_dpointer.c b/src/plugins/e-acsl/tests/temporal/t_dpointer.c
index 215ede69a5a..ede8f8b481c 100644
--- a/src/plugins/e-acsl/tests/temporal/t_dpointer.c
+++ b/src/plugins/e-acsl/tests/temporal/t_dpointer.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Simple case of double pointer dereference
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_fptr.c b/src/plugins/e-acsl/tests/temporal/t_fptr.c
index 0afcc96640d..e0f605d3ab0 100644
--- a/src/plugins/e-acsl/tests/temporal/t_fptr.c
+++ b/src/plugins/e-acsl/tests/temporal/t_fptr.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check simple case of calling functions via pointer derefernce
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/t_fun_lib.c
index d98643937bb..f5a7f077f94 100644
--- a/src/plugins/e-acsl/tests/temporal/t_fun_lib.c
+++ b/src/plugins/e-acsl/tests/temporal/t_fun_lib.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check handling library functions (without definitions)
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_fun_ptr.c b/src/plugins/e-acsl/tests/temporal/t_fun_ptr.c
index d0637544973..fc0e99b8495 100644
--- a/src/plugins/e-acsl/tests/temporal/t_fun_ptr.c
+++ b/src/plugins/e-acsl/tests/temporal/t_fun_ptr.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check handling function definitions with pointer parameters
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_getenv.c b/src/plugins/e-acsl/tests/temporal/t_getenv.c
index 1f5066ee368..016779b79af 100644
--- a/src/plugins/e-acsl/tests/temporal/t_getenv.c
+++ b/src/plugins/e-acsl/tests/temporal/t_getenv.c
@@ -1,6 +1,7 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check temporal validity of environment string (via getenv function)
*/
+
#include <stdlib.h>
#include <errno.h>
diff --git a/src/plugins/e-acsl/tests/temporal/t_global_init.c b/src/plugins/e-acsl/tests/temporal/t_global_init.c
index e6edd0e607f..fa46d21a401 100644
--- a/src/plugins/e-acsl/tests/temporal/t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/t_global_init.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check global compound variable initializers
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_labels.c b/src/plugins/e-acsl/tests/temporal/t_labels.c
index 5d82c469b0f..c9afc1ad4cc 100644
--- a/src/plugins/e-acsl/tests/temporal/t_labels.c
+++ b/src/plugins/e-acsl/tests/temporal/t_labels.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check that statements generated via temporal analysis are handled
COMMENT: properly, i.e., if a statement has a label attached then all
COMMENT: the generated statements are inserted after that label
diff --git a/src/plugins/e-acsl/tests/temporal/t_lit_string.c b/src/plugins/e-acsl/tests/temporal/t_lit_string.c
index 2469f352b41..634c6875cbe 100644
--- a/src/plugins/e-acsl/tests/temporal/t_lit_string.c
+++ b/src/plugins/e-acsl/tests/temporal/t_lit_string.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check handling of literal strings. Because literal strings are
COMMENT: replaced by variables we need to make sure that we take block
COMMENT: numbers and not referent numbers in assignments
diff --git a/src/plugins/e-acsl/tests/temporal/t_local_init.c b/src/plugins/e-acsl/tests/temporal/t_local_init.c
index 01afaf3dbcc..0a819870904 100644
--- a/src/plugins/e-acsl/tests/temporal/t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/t_local_init.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Check local compound variable initializers
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/t_malloc-asan.c
index 78f96e9145f..542afcfa370 100644
--- a/src/plugins/e-acsl/tests/temporal/t_malloc-asan.c
+++ b/src/plugins/e-acsl/tests/temporal/t_malloc-asan.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Temporal analysis with respect dynamic memory allocation.
COMMENT: malloc-free-malloc errors
COMMENT: This test is a modification aiming targeting AddressSanitizer and
diff --git a/src/plugins/e-acsl/tests/temporal/t_malloc.c b/src/plugins/e-acsl/tests/temporal/t_malloc.c
index 9ae3b5d0a28..531c2053098 100644
--- a/src/plugins/e-acsl/tests/temporal/t_malloc.c
+++ b/src/plugins/e-acsl/tests/temporal/t_malloc.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Temporal analysis with respect dynamic memory allocation.
COMMENT: malloc-free-malloc errors
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_scope.c b/src/plugins/e-acsl/tests/temporal/t_scope.c
index d023e0fb497..250632f5873 100644
--- a/src/plugins/e-acsl/tests/temporal/t_scope.c
+++ b/src/plugins/e-acsl/tests/temporal/t_scope.c
@@ -1,6 +1,7 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Temporal analysis with respect to scopes
*/
+
#include <stddef.h>
int main() {
diff --git a/src/plugins/e-acsl/tests/temporal/t_struct.c b/src/plugins/e-acsl/tests/temporal/t_struct.c
index e72e879cf60..dd3526dc565 100644
--- a/src/plugins/e-acsl/tests/temporal/t_struct.c
+++ b/src/plugins/e-acsl/tests/temporal/t_struct.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Several basic cases involving assignments of structs
*/
diff --git a/src/plugins/e-acsl/tests/temporal/t_while.c b/src/plugins/e-acsl/tests/temporal/t_while.c
index 7f39075385a..05a506120b1 100644
--- a/src/plugins/e-acsl/tests/temporal/t_while.c
+++ b/src/plugins/e-acsl/tests/temporal/t_while.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci, run.config_dev
COMMENT: Off-by-one error where a pointer is made point to an adjacent block
COMMENT: Note that this behaviour is not quaranteed by likely due to the
COMMENT: way compiler allocates stack blocks
diff --git a/src/plugins/e-acsl/tests/temporal/test_config_dev b/src/plugins/e-acsl/tests/temporal/test_config_dev
index e86b18769b2..a390cadc7c6 100644
--- a/src/plugins/e-acsl/tests/temporal/test_config_dev
+++ b/src/plugins/e-acsl/tests/temporal/test_config_dev
@@ -1,2 +1 @@
-DONTRUN:
-MACRO: ROOT_EACSL_GCC_OPTS_EXT --temporal
\ No newline at end of file
+MACRO: ROOT_EACSL_GCC_OPTS_EXT --temporal
--
GitLab