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 9c4df1533bf7feccab969de992f3c7692d8a77a2..b574f1ebb23ff90ef20b247d80dc53950ba7cac1 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 a0e3962c59b2053f8935433bd8700817af90aa19..8a0fc1325ad2739c205d5f68f3c75da00e5f9f53 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 7bd89827d09cfe2f1dfb1057c0b28c1c32d06abc..b55cb5a92eafcf2f00321298635858249ab4b402 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 9826a53ef7efbcc35395480a2eb83765489302ab..058ed9b3e78ad3db813372a8cae8c82bda2284c6 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0e725129643c7b30e93ea6195c25aba9922e6972..e636757d80cf08bc6ce76558588b6d19d49165e6 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0e725129643c7b30e93ea6195c25aba9922e6972..95c70361d689b4b4e6930818e275b4b729e56723 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 6af29643dcce11eb46a179d0074b4071c5fda849..3d748d198fa047070be6e22c80b86c6689f40055 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 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 562cc4e026c35f45fdeb94e9e2c0b3aa32a65bf2..b847786468f62551a3b2b1ac91111f49e883c423 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 c48b3e093e24048261d1b2db5c1b19ca0a608591..8d5a4b9a8eaaf6940e28365b5f7e6e709801a649 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 ff2e8be836240ac5e912b987a75f6279d755f697..f4166ccf69aeb1db1305d8dfeade9f84fabb1369 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 e8f001a3a72234a6f6a1a7073b8ce02c82d9cd1f..6cd778f70977b16bc85b2c0bb16af2103e78f68f 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 88c1cf9712022c1c32ccf47259fe968c4f633f5b..5130ef693dfea9d778f0dc8b4713c5dc360165f0 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 215ede69a5ac728d2b0a61f805a1711ed12f1d45..ede8f8b481c202fae55e63c1b220191aa774ce01 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 0afcc96640d51099799db3fc1e9b96033fbb43a2..e0f605d3ab0de91f4b0aa2cdaec73d41486df3d4 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 d98643937bbd1161685ee1a6b7e265d41f53e0c1..f5a7f077f94dc05a6f5a58513db7d87fc30933be 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 d0637544973e1bac493f0bc6e51b672fe7863aba..fc0e99b84953c08242632d30f2be91e0baba8dac 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 1f5066ee368a1ddccbb1c7773329bae6ab84d13c..016779b79af71d409e27a61d458af4249df331ed 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 e6edd0e607f64408c6859d400df6d61aeb4f5c06..fa46d21a401e9ca8dbe0509f68c55ef6eb87f5e0 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 5d82c469b0fca0fea19e9c8867e9f6d1d05a8d60..c9afc1ad4ccb053c19aa6ad104dc4807a91cb8ae 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 2469f352b4105cbdafccc9422054e0724ad84100..634c6875cbea95e70faf24e1fac9f1d448517ca7 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 01afaf3dbcc4216c7b0c5d3d85ef91fb51e63a5d..0a819870904c6ddac5311a0d875df1d19ad27f02 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 78f96e9145f8a1189dab9aad45a56ea0b1da1fd4..542afcfa3701af31353d28b4635d2a0b631ec988 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 9ae3b5d0a280fb86e55ce5f5f18fc32bc2022c58..531c2053098ef90b313bd5616830c3b3f4792b49 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 d023e0fb4971bc3bba5d01a973b341698a94751b..250632f587345a6956b1c5ce31b6624792f2acd9 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 e72e879cf605c315e6b69d6579dc479e4e6648f2..dd3526dc565ea0211752d0b2e649065e070ab578 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 7f39075385affd69ef3175b72ce9090142ca9b59..05a506120b1b6a69f425500bf441ba3fcc553e26 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 e86b18769b24a62bffe04fe97709831badddbda4..a390cadc7c632ab6c59fde8881a2695e0749ef4d 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