diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore index 5543dbdb43e12ae58f5c6ecfa2674b7ebf5243c4..571f4326b0671351d79f193657dbf8c1d0d23fff 100644 --- a/src/plugins/e-acsl/.gitignore +++ b/src/plugins/e-acsl/.gitignore @@ -57,6 +57,7 @@ /tests/test_config_ci /tests/test_config_dev /tests/*/result*/* +/tests/*/oracle_ci/* /tests/check/obj/* .frama-c tests/ptests_config diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index b2befe524f232d45cb7fed6b7e9e57a17be2337c..bc2d25e3edeec9aa496db2bb54df3355916a4fc0 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -184,17 +184,18 @@ PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml DEV?= ifeq ("$(DEV)","yes") EACSL_TEST_CONFIG:=dev -else - EACSL_TEST_CONFIG:=ci endif -# Prepend PTESTS_OPTS with the test config to use. If the user-provided -# PTESTS_OPTS variable contains another -config instruction, then it will be -# prioritized over the one selected by the Makefile. -E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: override PTESTS_OPTS:=-config $(EACSL_TEST_CONFIG) $(PTESTS_OPTS) + +ifdef EACSL_TEST_CONFIG + # Prepend PTESTS_OPTS with the test config to use. If the user-provided + # PTESTS_OPTS variable contains another -config instruction, then it will be + # prioritized over the one selected by the Makefile. + E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: override PTESTS_OPTS:=-config $(EACSL_TEST_CONFIG) $(PTESTS_OPTS) +endif TEST_DEPENDENCIES:= \ $(EACSL_PLUGIN_DIR)/tests/ptests_config \ - $(EACSL_PLUGIN_DIR)/tests/test_config_ci \ + $(EACSL_PLUGIN_DIR)/tests/test_config \ $(EACSL_PLUGIN_DIR)/tests/test_config_dev \ $(EACSL_PLUGIN_DIR)/tests/print.cmo @@ -209,8 +210,8 @@ plugins_ptests_config: $(TEST_DEPENDENCIES) E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: $(TEST_DEPENDENCIES) tests:: $(TEST_DEPENDENCIES) -$(EACSL_PLUGIN_DIR)/tests/test_config_ci: \ - $(EACSL_PLUGIN_DIR)/tests/test_config_ci.in \ +$(EACSL_PLUGIN_DIR)/tests/test_config: \ + $(EACSL_PLUGIN_DIR)/tests/test_config.in \ $(EACSL_PLUGIN_DIR)/Makefile $(PRINT_MAKING) $@ $(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@ @@ -227,7 +228,7 @@ clean:: done $(PRINT_RM) cleaning generated test files $(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o - $(RM) $(E_ACSL_DIR)/tests/test_config_ci \ + $(RM) $(E_ACSL_DIR)/tests/test_config \ $(E_ACSL_DIR)/tests/test_config_dev $(RM) $(foreach dir, $(PLUGIN_TESTS_DIRS), tests/$(dir)/result/*) @@ -323,16 +324,16 @@ EACSL_DOC_FILES = \ EACSL_TEST_FILES = \ tests/test_config_dev.in \ - tests/test_config_ci.in \ - tests/gmp-only/test_config_ci \ + tests/test_config.in \ + tests/gmp-only/test_config \ tests/gmp-only/test_config_dev \ - tests/full-mtracking/test_config_ci \ + tests/full-mtracking/test_config \ tests/full-mtracking/test_config_dev \ - tests/builtin/test_config_ci \ + tests/builtin/test_config \ tests/builtin/test_config_dev \ - tests/temporal/test_config_ci \ + tests/temporal/test_config \ tests/temporal/test_config_dev \ - tests/format/test_config_ci \ + tests/format/test_config \ tests/format/test_config_dev \ tests/print.ml @@ -340,9 +341,9 @@ EACSL_TEST_FILES = \ EACSL_DISTRIB_TESTS = \ $(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \ $(dir)/*.[ich] \ - $(dir)/test_config_ci \ + $(dir)/test_config \ $(dir)/test_config_dev \ - $(dir)/oracle_ci/* \ + $(dir)/oracle/* \ $(dir)/oracle_dev/* \ ) diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt index 82e0dc5a87c8525b82c160f0d198bed05dbead73..7f24e72705c0e02ecd7c80e03048f3fed66aaa35 100644 --- a/src/plugins/e-acsl/headers/header_spec.txt +++ b/src/plugins/e-acsl/headers/header_spec.txt @@ -150,15 +150,15 @@ src/project_initializer/rtl.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/project_initializer/prepare_ast.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL src/project_initializer/prepare_ast.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL tests/print.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL -tests/test_config_ci.in: .ignore +tests/test_config.in: .ignore tests/test_config_dev.in: .ignore -tests/builtin/test_config_ci: .ignore +tests/builtin/test_config: .ignore tests/builtin/test_config_dev: .ignore -tests/format/test_config_ci: .ignore +tests/format/test_config: .ignore tests/format/test_config_dev: .ignore -tests/full-mtracking/test_config_ci: .ignore +tests/full-mtracking/test_config: .ignore tests/full-mtracking/test_config_dev: .ignore -tests/gmp-only/test_config_ci: .ignore +tests/gmp-only/test_config: .ignore tests/gmp-only/test_config_dev: .ignore -tests/temporal/test_config_ci: .ignore +tests/temporal/test_config: .ignore tests/temporal/test_config_dev: .ignore diff --git a/src/plugins/e-acsl/tests/arith/array.i b/src/plugins/e-acsl/tests/arith/array.i index 4ef7b8e882fb2b7aa57e48eb425b5436fd70349b..eca3cdeea30ac0823b5d58ce32382e1639acd774 100644 --- a/src/plugins/e-acsl/tests/arith/array.i +++ b/src/plugins/e-acsl/tests/arith/array.i @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: arrays STDOPT: #"-eva-slevel 5" */ diff --git a/src/plugins/e-acsl/tests/arith/bitwise.c b/src/plugins/e-acsl/tests/arith/bitwise.c index 676150fb0315130ec0efd4a7e9c6d7ffa2588339..37e967a40b26ae9dbd89213a75e1be964e2c2761 100644 --- a/src/plugins/e-acsl/tests/arith/bitwise.c +++ b/src/plugins/e-acsl/tests/arith/bitwise.c @@ -1,8 +1,10 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Support of bitwise operations - MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -warn-right-shift-negative -warn-left-shift-negative STDOPT: #"-warn-right-shift-negative -warn-left-shift-negative" */ +/* run.config_dev + MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -warn-right-shift-negative -warn-left-shift-negative +*/ #include <limits.h> diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c index 89eb4a6a15c7c0f242611ebc534fea5aafa09d90..6542b6eaff0afe9a156199e54219679faa7a37bb 100644 --- a/src/plugins/e-acsl/tests/arith/functions_rec.c +++ b/src/plugins/e-acsl/tests/arith/functions_rec.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: recursive logic functions STDOPT: +"-eva-unroll-recursive-calls 100" */ diff --git a/src/plugins/e-acsl/tests/arith/longlong.i b/src/plugins/e-acsl/tests/arith/longlong.i index 9dc71da4e6dc44fc36bb79c1ed0dd5390cbf0137..851d7a13c56ae978d4a5b678f3c5e37379966231 100644 --- a/src/plugins/e-acsl/tests/arith/longlong.i +++ b/src/plugins/e-acsl/tests/arith/longlong.i @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: upgrading longlong to GMP STDOPT: +"-eva-unroll-recursive-calls 8" */ diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/array.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/array.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/at.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/at.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle similarity index 87% rename from src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle index e4a35555d5f519e3d00a6f0883a7713dc5b41e20..1d829537034b569747b7f2216f3b8e1c335b4c05 100644 --- a/src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle +++ b/src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle @@ -1,16 +1,12 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] tests/arith/bitwise.c:40: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] tests/arith/bitwise.c:40: Warning: - function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:42: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:42: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:44: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] tests/arith/bitwise.c:45: Warning: +[eva:alarm] tests/arith/bitwise.c:44: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:46: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. @@ -18,9 +14,9 @@ function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:48: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] tests/arith/bitwise.c:55: Warning: +[eva:alarm] tests/arith/bitwise.c:49: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] tests/arith/bitwise.c:55: Warning: +[eva:alarm] tests/arith/bitwise.c:50: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:57: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. @@ -28,7 +24,7 @@ function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:59: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. -[eva:alarm] tests/arith/bitwise.c:60: Warning: +[eva:alarm] tests/arith/bitwise.c:59: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:61: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. @@ -36,3 +32,7 @@ function __e_acsl_assert, behavior blocking: precondition got status unknown. [eva:alarm] tests/arith/bitwise.c:63: Warning: function __e_acsl_assert, behavior blocking: precondition got status unknown. +[eva:alarm] tests/arith/bitwise.c:64: Warning: + function __e_acsl_assert, behavior blocking: precondition got status unknown. +[eva:alarm] tests/arith/bitwise.c:65: Warning: + function __e_acsl_assert, behavior blocking: precondition got status unknown. diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/cast.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/cast.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/comparison.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/comparison.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/functions.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_arith.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle/gen_array.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_array.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_at.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c similarity index 95% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c index 45747581a4140cb65b4165cbaabb258e6b81faae..54340192b07b7754f52a4ea9b5bef4152f4659d7 100644 --- a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_bitwise.c +++ b/src/plugins/e-acsl/tests/arith/oracle/gen_bitwise.c @@ -5,27 +5,27 @@ void f_signed(int a, int b) { int c = a << 2; __e_acsl_assert(0 <= a,1,"RTE","f_signed","shift: 0 <= a", - "tests/arith/bitwise.c",12); + "tests/arith/bitwise.c",14); __e_acsl_assert((long)c == a << 2L,1,"Assertion","f_signed","c == a << 2", - "tests/arith/bitwise.c",12); + "tests/arith/bitwise.c",14); /*@ assert c ≡ a << 2; */ ; int d = b >> 2; __e_acsl_assert(0 <= b,1,"RTE","f_signed","shift: 0 <= b", - "tests/arith/bitwise.c",14); + "tests/arith/bitwise.c",16); __e_acsl_assert(d == b >> 2,1,"Assertion","f_signed","d == b >> 2", - "tests/arith/bitwise.c",14); + "tests/arith/bitwise.c",16); /*@ assert d ≡ b >> 2; */ ; int e = a | b; __e_acsl_assert((long)e == (a | (long)b),1,"Assertion","f_signed", - "e == (a | b)","tests/arith/bitwise.c",16); + "e == (a | b)","tests/arith/bitwise.c",18); /*@ assert e ≡ (a | b); */ ; int f = a & b; __e_acsl_assert((long)f == (a & (long)b),1,"Assertion","f_signed", - "f == (a & b)","tests/arith/bitwise.c",18); + "f == (a & b)","tests/arith/bitwise.c",20); /*@ assert f ≡ (a & b); */ ; int g = a ^ b; __e_acsl_assert((long)g == (a ^ (long)b),1,"Assertion","f_signed", - "g == (a ^ b)","tests/arith/bitwise.c",20); + "g == (a ^ b)","tests/arith/bitwise.c",22); /*@ assert g ≡ (a ^ b); */ ; return; } @@ -34,23 +34,23 @@ void f_unsigned(unsigned int a, unsigned int b) { unsigned int c = a << 2u; __e_acsl_assert((unsigned long)c == a << 2UL,1,"Assertion","f_unsigned", - "c == a << 2","tests/arith/bitwise.c",26); + "c == a << 2","tests/arith/bitwise.c",28); /*@ assert c ≡ a << 2; */ ; unsigned int d = b >> 2u; __e_acsl_assert(d == b >> 2U,1,"Assertion","f_unsigned","d == b >> 2", - "tests/arith/bitwise.c",28); + "tests/arith/bitwise.c",30); /*@ assert d ≡ b >> 2; */ ; unsigned int e = a | b; __e_acsl_assert(e == (a | b),1,"Assertion","f_unsigned","e == (a | b)", - "tests/arith/bitwise.c",30); + "tests/arith/bitwise.c",32); /*@ assert e ≡ (a | b); */ ; unsigned int f = a & b; __e_acsl_assert(f == (a & b),1,"Assertion","f_unsigned","f == (a & b)", - "tests/arith/bitwise.c",32); + "tests/arith/bitwise.c",34); /*@ assert f ≡ (a & b); */ ; unsigned int g = a ^ b; __e_acsl_assert(g == (a ^ b),1,"Assertion","f_unsigned","g == (a ^ b)", - "tests/arith/bitwise.c",34); + "tests/arith/bitwise.c",36); /*@ assert g ≡ (a ^ b); */ ; return; } @@ -78,7 +78,7 @@ void g_signed(int a, int b) */ __e_acsl_assert(__gen_e_acsl_b_shiftl_guard,1,"RTE","g_signed", "shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615", - "tests/arith/bitwise.c",40); + "tests/arith/bitwise.c",42); __gen_e_acsl_b_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b)); __gmpz_init_set_si(__gen_e_acsl_,0L); __gen_e_acsl_a_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a), @@ -86,14 +86,14 @@ void g_signed(int a, int b) __gmpz_init(__gen_e_acsl_shiftl); /*@ assert E_ACSL: a ≥ 0; */ __e_acsl_assert(__gen_e_acsl_a_shiftl_guard >= 0,1,"RTE","g_signed", - "a >= 0","tests/arith/bitwise.c",40); + "a >= 0","tests/arith/bitwise.c",42); __gmpz_mul_2exp(__gen_e_acsl_shiftl, (__e_acsl_mpz_struct const *)(__gen_e_acsl_a), __gen_e_acsl_b_shiftl_coerced); __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_c), (__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl)); __e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","g_signed", - "c == a << b","tests/arith/bitwise.c",40); + "c == a << b","tests/arith/bitwise.c",42); __gmpz_clear(__gen_e_acsl_c); __gmpz_clear(__gen_e_acsl_a); __gmpz_clear(__gen_e_acsl_b); @@ -122,7 +122,7 @@ void g_signed(int a, int b) */ __e_acsl_assert(__gen_e_acsl_b_shiftr_guard,1,"RTE","g_signed", "shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615", - "tests/arith/bitwise.c",42); + "tests/arith/bitwise.c",44); __gen_e_acsl_b_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b_2)); __gmpz_init_set_si(__gen_e_acsl__2,0L); __gen_e_acsl_a_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2), @@ -130,14 +130,14 @@ void g_signed(int a, int b) __gmpz_init(__gen_e_acsl_shiftr); /*@ assert E_ACSL: a ≥ 0; */ __e_acsl_assert(__gen_e_acsl_a_shiftr_guard >= 0,1,"RTE","g_signed", - "a >= 0","tests/arith/bitwise.c",42); + "a >= 0","tests/arith/bitwise.c",44); __gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr, (__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2), __gen_e_acsl_b_shiftr_coerced); __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_d), (__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr)); __e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","g_signed", - "d == a >> b","tests/arith/bitwise.c",42); + "d == a >> b","tests/arith/bitwise.c",44); __gmpz_clear(__gen_e_acsl_d); __gmpz_clear(__gen_e_acsl_a_2); __gmpz_clear(__gen_e_acsl_b_2); @@ -168,7 +168,7 @@ void g_signed(int a, int b) */ __e_acsl_assert(__gen_e_acsl_cst_shiftl_guard,1,"RTE","g_signed", "shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 1 <= 18446744073709551615", - "tests/arith/bitwise.c",44); + "tests/arith/bitwise.c",46); __gen_e_acsl_cst_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__4)); __gmpz_init_set_si(__gen_e_acsl__5,0L); __gen_e_acsl_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add), @@ -177,7 +177,7 @@ void g_signed(int a, int b) /*@ assert E_ACSL: 18446744073709551615ULL + 1 ≥ 0; */ __e_acsl_assert(__gen_e_acsl_shiftl_guard >= 0,1,"RTE","g_signed", "18446744073709551615ULL + 1 >= 0", - "tests/arith/bitwise.c",44); + "tests/arith/bitwise.c",46); __gmpz_mul_2exp(__gen_e_acsl_shiftl_2, (__e_acsl_mpz_struct const *)(__gen_e_acsl_add), __gen_e_acsl_cst_shiftl_coerced); @@ -185,7 +185,7 @@ void g_signed(int a, int b) (__e_acsl_mpz_struct const *)(__gen_e_acsl__5)); __e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","g_signed", "(18446744073709551615ULL + 1) << 1 != 0", - "tests/arith/bitwise.c",44); + "tests/arith/bitwise.c",46); __gmpz_clear(__gen_e_acsl__3); __gmpz_clear(__gen_e_acsl__4); __gmpz_clear(__gen_e_acsl_add); @@ -216,7 +216,7 @@ void g_signed(int a, int b) */ __e_acsl_assert(__gen_e_acsl_cst_shiftr_guard,1,"RTE","g_signed", "shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= 1 <= 18446744073709551615", - "tests/arith/bitwise.c",45); + "tests/arith/bitwise.c",47); __gen_e_acsl_cst_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__7)); __gmpz_init_set_si(__gen_e_acsl__8,0L); __gen_e_acsl_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2), @@ -225,14 +225,14 @@ void g_signed(int a, int b) /*@ assert E_ACSL: 18446744073709551615ULL + 1 ≥ 0; */ __e_acsl_assert(__gen_e_acsl_shiftr_guard >= 0,1,"RTE","g_signed", "18446744073709551615ULL + 1 >= 0", - "tests/arith/bitwise.c",45); + "tests/arith/bitwise.c",47); __gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr_2, (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2), __gen_e_acsl_cst_shiftr_coerced); __gen_e_acsl__9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr_2)); __e_acsl_assert(__gen_e_acsl__9 != 0UL,1,"Assertion","g_signed", "(18446744073709551615ULL + 1) >> 1 != 0", - "tests/arith/bitwise.c",45); + "tests/arith/bitwise.c",47); __gmpz_clear(__gen_e_acsl__6); __gmpz_clear(__gen_e_acsl__7); __gmpz_clear(__gen_e_acsl_add_2); @@ -258,7 +258,7 @@ void g_signed(int a, int b) */ __e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_2,1,"RTE","g_signed", "shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 65 <= 18446744073709551615", - "tests/arith/bitwise.c",46); + "tests/arith/bitwise.c",48); __gen_e_acsl_cst_shiftl_coerced_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__11)); __gmpz_init_set_si(__gen_e_acsl__12,0L); __gen_e_acsl_cst_shiftl_guard_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10), @@ -266,14 +266,14 @@ void g_signed(int a, int b) __gmpz_init(__gen_e_acsl_shiftl_3); /*@ assert E_ACSL: 1 ≥ 0; */ __e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_3 >= 0,1,"RTE","g_signed", - "1 >= 0","tests/arith/bitwise.c",46); + "1 >= 0","tests/arith/bitwise.c",48); __gmpz_mul_2exp(__gen_e_acsl_shiftl_3, (__e_acsl_mpz_struct const *)(__gen_e_acsl__10), __gen_e_acsl_cst_shiftl_coerced_2); __gen_e_acsl_ne_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl_3), (__e_acsl_mpz_struct const *)(__gen_e_acsl__12)); __e_acsl_assert(__gen_e_acsl_ne_2 != 0,1,"Assertion","g_signed", - "1 << 65 != 0","tests/arith/bitwise.c",46); + "1 << 65 != 0","tests/arith/bitwise.c",48); __gmpz_clear(__gen_e_acsl__10); __gmpz_clear(__gen_e_acsl__11); __gmpz_clear(__gen_e_acsl__12); @@ -309,7 +309,7 @@ void g_signed(int a, int b) (__e_acsl_mpz_struct const *)(__gen_e_acsl__16)); __e_acsl_assert(__gen_e_acsl_ne_3 != 0,1,"Assertion","g_signed", "((18446744073709551615ULL + 1) | ((-9223372036854775807LL - 1LL) - 1)) != 0", - "tests/arith/bitwise.c",47); + "tests/arith/bitwise.c",49); __gmpz_clear(__gen_e_acsl__13); __gmpz_clear(__gen_e_acsl__14); __gmpz_clear(__gen_e_acsl_add_3); @@ -355,7 +355,7 @@ void g_signed(int a, int b) (__e_acsl_mpz_struct const *)(__gen_e_acsl_bxor)); __e_acsl_assert(__gen_e_acsl_ne_4 != 0,1,"Assertion","g_signed", "((18446744073709551615ULL + 1) & ((-9223372036854775807LL - 1LL) - 1)) !=\n((18446744073709551615ULL + 1) ^ ((-9223372036854775807LL - 1LL) - 1))", - "tests/arith/bitwise.c",48); + "tests/arith/bitwise.c",50); __gmpz_clear(__gen_e_acsl__17); __gmpz_clear(__gen_e_acsl__18); __gmpz_clear(__gen_e_acsl_add_4); @@ -395,7 +395,7 @@ void g_unsigned(unsigned int a, unsigned int b) */ __e_acsl_assert(__gen_e_acsl_b_shiftl_guard,1,"RTE","g_unsigned", "shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615", - "tests/arith/bitwise.c",55); + "tests/arith/bitwise.c",57); __gen_e_acsl_b_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b)); __gmpz_init_set_si(__gen_e_acsl_,0L); __gen_e_acsl_a_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a), @@ -403,14 +403,14 @@ void g_unsigned(unsigned int a, unsigned int b) __gmpz_init(__gen_e_acsl_shiftl); /*@ assert E_ACSL: a ≥ 0; */ __e_acsl_assert(__gen_e_acsl_a_shiftl_guard >= 0,1,"RTE","g_unsigned", - "a >= 0","tests/arith/bitwise.c",55); + "a >= 0","tests/arith/bitwise.c",57); __gmpz_mul_2exp(__gen_e_acsl_shiftl, (__e_acsl_mpz_struct const *)(__gen_e_acsl_a), __gen_e_acsl_b_shiftl_coerced); __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_c), (__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl)); __e_acsl_assert(__gen_e_acsl_eq == 0,1,"Assertion","g_unsigned", - "c == a << b","tests/arith/bitwise.c",55); + "c == a << b","tests/arith/bitwise.c",57); __gmpz_clear(__gen_e_acsl_c); __gmpz_clear(__gen_e_acsl_a); __gmpz_clear(__gen_e_acsl_b); @@ -439,7 +439,7 @@ void g_unsigned(unsigned int a, unsigned int b) */ __e_acsl_assert(__gen_e_acsl_b_shiftr_guard,1,"RTE","g_unsigned", "shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= b <= 18446744073709551615", - "tests/arith/bitwise.c",57); + "tests/arith/bitwise.c",59); __gen_e_acsl_b_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_b_2)); __gmpz_init_set_si(__gen_e_acsl__2,0L); __gen_e_acsl_a_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2), @@ -447,14 +447,14 @@ void g_unsigned(unsigned int a, unsigned int b) __gmpz_init(__gen_e_acsl_shiftr); /*@ assert E_ACSL: a ≥ 0; */ __e_acsl_assert(__gen_e_acsl_a_shiftr_guard >= 0,1,"RTE","g_unsigned", - "a >= 0","tests/arith/bitwise.c",57); + "a >= 0","tests/arith/bitwise.c",59); __gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr, (__e_acsl_mpz_struct const *)(__gen_e_acsl_a_2), __gen_e_acsl_b_shiftr_coerced); __gen_e_acsl_eq_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_d), (__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr)); __e_acsl_assert(__gen_e_acsl_eq_2 == 0,1,"Assertion","g_unsigned", - "d == a >> b","tests/arith/bitwise.c",57); + "d == a >> b","tests/arith/bitwise.c",59); __gmpz_clear(__gen_e_acsl_d); __gmpz_clear(__gen_e_acsl_a_2); __gmpz_clear(__gen_e_acsl_b_2); @@ -485,7 +485,7 @@ void g_unsigned(unsigned int a, unsigned int b) */ __e_acsl_assert(__gen_e_acsl_cst_shiftl_guard,1,"RTE","g_unsigned", "shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 1u <= 18446744073709551615", - "tests/arith/bitwise.c",59); + "tests/arith/bitwise.c",61); __gen_e_acsl_cst_shiftl_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__4)); __gmpz_init_set_si(__gen_e_acsl__5,0L); __gen_e_acsl_shiftl_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add), @@ -494,7 +494,7 @@ void g_unsigned(unsigned int a, unsigned int b) /*@ assert E_ACSL: 18446744073709551615ULL + 1u ≥ 0; */ __e_acsl_assert(__gen_e_acsl_shiftl_guard >= 0,1,"RTE","g_unsigned", "18446744073709551615ULL + 1u >= 0", - "tests/arith/bitwise.c",59); + "tests/arith/bitwise.c",61); __gmpz_mul_2exp(__gen_e_acsl_shiftl_2, (__e_acsl_mpz_struct const *)(__gen_e_acsl_add), __gen_e_acsl_cst_shiftl_coerced); @@ -502,7 +502,7 @@ void g_unsigned(unsigned int a, unsigned int b) (__e_acsl_mpz_struct const *)(__gen_e_acsl__5)); __e_acsl_assert(__gen_e_acsl_ne != 0,1,"Assertion","g_unsigned", "(18446744073709551615ULL + 1u) << 1u != 0", - "tests/arith/bitwise.c",59); + "tests/arith/bitwise.c",61); __gmpz_clear(__gen_e_acsl__3); __gmpz_clear(__gen_e_acsl__4); __gmpz_clear(__gen_e_acsl_add); @@ -533,7 +533,7 @@ void g_unsigned(unsigned int a, unsigned int b) */ __e_acsl_assert(__gen_e_acsl_cst_shiftr_guard,1,"RTE","g_unsigned", "shiftr_rhs_fits_in_mp_bitcnt_t: 0 <= 1u <= 18446744073709551615", - "tests/arith/bitwise.c",60); + "tests/arith/bitwise.c",62); __gen_e_acsl_cst_shiftr_coerced = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__7)); __gmpz_init_set_si(__gen_e_acsl__8,0L); __gen_e_acsl_shiftr_guard = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2), @@ -542,14 +542,14 @@ void g_unsigned(unsigned int a, unsigned int b) /*@ assert E_ACSL: 18446744073709551615ULL + 1u ≥ 0; */ __e_acsl_assert(__gen_e_acsl_shiftr_guard >= 0,1,"RTE","g_unsigned", "18446744073709551615ULL + 1u >= 0", - "tests/arith/bitwise.c",60); + "tests/arith/bitwise.c",62); __gmpz_tdiv_q_2exp(__gen_e_acsl_shiftr_2, (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_2), __gen_e_acsl_cst_shiftr_coerced); __gen_e_acsl__9 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftr_2)); __e_acsl_assert(__gen_e_acsl__9 != 0UL,1,"Assertion","g_unsigned", "(18446744073709551615ULL + 1u) >> 1u != 0", - "tests/arith/bitwise.c",60); + "tests/arith/bitwise.c",62); __gmpz_clear(__gen_e_acsl__6); __gmpz_clear(__gen_e_acsl__7); __gmpz_clear(__gen_e_acsl_add_2); @@ -575,7 +575,7 @@ void g_unsigned(unsigned int a, unsigned int b) */ __e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_2,1,"RTE","g_unsigned", "shiftl_rhs_fits_in_mp_bitcnt_t: 0 <= 65u <= 18446744073709551615", - "tests/arith/bitwise.c",61); + "tests/arith/bitwise.c",63); __gen_e_acsl_cst_shiftl_coerced_2 = __gmpz_get_ui((__e_acsl_mpz_struct const *)(__gen_e_acsl__11)); __gmpz_init_set_si(__gen_e_acsl__12,0L); __gen_e_acsl_cst_shiftl_guard_3 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl__10), @@ -583,14 +583,14 @@ void g_unsigned(unsigned int a, unsigned int b) __gmpz_init(__gen_e_acsl_shiftl_3); /*@ assert E_ACSL: 1u ≥ 0; */ __e_acsl_assert(__gen_e_acsl_cst_shiftl_guard_3 >= 0,1,"RTE", - "g_unsigned","1u >= 0","tests/arith/bitwise.c",61); + "g_unsigned","1u >= 0","tests/arith/bitwise.c",63); __gmpz_mul_2exp(__gen_e_acsl_shiftl_3, (__e_acsl_mpz_struct const *)(__gen_e_acsl__10), __gen_e_acsl_cst_shiftl_coerced_2); __gen_e_acsl_ne_2 = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_shiftl_3), (__e_acsl_mpz_struct const *)(__gen_e_acsl__12)); __e_acsl_assert(__gen_e_acsl_ne_2 != 0,1,"Assertion","g_unsigned", - "1u << 65u != 0","tests/arith/bitwise.c",61); + "1u << 65u != 0","tests/arith/bitwise.c",63); __gmpz_clear(__gen_e_acsl__10); __gmpz_clear(__gen_e_acsl__11); __gmpz_clear(__gen_e_acsl__12); @@ -619,7 +619,7 @@ void g_unsigned(unsigned int a, unsigned int b) (__e_acsl_mpz_struct const *)(__gen_e_acsl__15)); __e_acsl_assert(__gen_e_acsl_ne_3 != 0,1,"Assertion","g_unsigned", "((18446744073709551615ULL + 1u) | 1u) != 0", - "tests/arith/bitwise.c",62); + "tests/arith/bitwise.c",64); __gmpz_clear(__gen_e_acsl__13); __gmpz_clear(__gen_e_acsl__14); __gmpz_clear(__gen_e_acsl_add_3); @@ -652,7 +652,7 @@ void g_unsigned(unsigned int a, unsigned int b) (__e_acsl_mpz_struct const *)(__gen_e_acsl_bxor)); __e_acsl_assert(__gen_e_acsl_ne_4 != 0,1,"Assertion","g_unsigned", "((18446744073709551615ULL + 1u) & 1u) !=\n((18446744073709551615ULL + 1u) ^ 1u)", - "tests/arith/bitwise.c",63); + "tests/arith/bitwise.c",65); __gmpz_clear(__gen_e_acsl__16); __gmpz_clear(__gen_e_acsl__17); __gmpz_clear(__gen_e_acsl_add_4); diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_cast.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_let.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle/gen_not.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_not.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/gen_sum.c b/src/plugins/e-acsl/tests/arith/oracle/gen_sum.c similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/gen_sum.c rename to src/plugins/e-acsl/tests/arith/oracle/gen_sum.c diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/integer_constant.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/integer_constant.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/let.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/let.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/let.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/not.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/not.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/not.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/not.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/oracle_ci/sum.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/arith/oracle_ci/sum.res.oracle rename to src/plugins/e-acsl/tests/arith/oracle/sum.res.oracle diff --git a/src/plugins/e-acsl/tests/arith/result_ci/.gitkeep b/src/plugins/e-acsl/tests/arith/result_ci/.gitkeep deleted file mode 100644 index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000 diff --git a/src/plugins/e-acsl/tests/bts/bts1395.i b/src/plugins/e-acsl/tests/bts/bts1395.i index 34b85b1ee8c73ac93cbf2eb25dde331690ad4ab0..01c399aa67785e1cd1887203c633f24b11a18842 100644 --- a/src/plugins/e-acsl/tests/bts/bts1395.i +++ b/src/plugins/e-acsl/tests/bts/bts1395.i @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: recursive function STDOPT: +"-eva-unroll-recursive-calls 5" */ diff --git a/src/plugins/e-acsl/tests/bts/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c index 9dbd83d269e0b636508a91221f8dfbb292c62a9f..9d299958c7e22790f9e6d218fc4343816a2bcebe 100644 --- a/src/plugins/e-acsl/tests/bts/bts1398.c +++ b/src/plugins/e-acsl/tests/bts/bts1398.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: variadic function call */ diff --git a/src/plugins/e-acsl/tests/bts/bts2386.c b/src/plugins/e-acsl/tests/bts/bts2386.c index 007b5c1523db429bdd25baee480d4ccb1fdfcd97..aec12329f6583c96b632e6f54f2d84ff6c5eeff3 100644 --- a/src/plugins/e-acsl/tests/bts/bts2386.c +++ b/src/plugins/e-acsl/tests/bts/bts2386.c @@ -1,4 +1,4 @@ -/* run.config, run.config_2 +/* run.config COMMENT: pointer substraction */ diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-139.c index d08b64bccfe85566d22503896fa2b3f8c381f67f..8222c0e3c22db38e45093403e4c508f67ef89ad9 100644 --- a/src/plugins/e-acsl/tests/bts/issue-eacsl-139.c +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-139.c @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: While unsupported, struct comparison should fail gracefully instead COMMENT: of crashing Frama-C (issue frama-c/e-acsl#139). */ diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c index dde2d2aed6d86286c36c65a36223e36f2132880d..536e7ccae8932498ab134cba45c989584dc1affc 100644 --- a/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-145.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: frama-c/e-acsl#145, test for validity of globals_init and globals_clean. STDOPT: +"-verbose 1 -eva-print" diff --git a/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c index 74b8476fdbf9b0c8e72eb96819d1157615fe6229..232f7d14e3320c6ba6608c233da2c5fdf04ad0ec 100644 --- a/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c +++ b/src/plugins/e-acsl/tests/bts/issue-eacsl-91.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: frama-c/e-acsl#91, test for misplaced delete_block of local variable in switch. STDOPT: #"-e-acsl-full-mtracking" diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1304.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1326.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1386_complex_flowgraph.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1386_complex_flowgraph.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1386_complex_flowgraph.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1386_complex_flowgraph.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1399.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1478.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1700.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1717.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1718.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1740.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts1837.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts2191.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts2231.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2305.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts2305.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2386.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts2386.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts2406.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/bts2406.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1386_complex_flowgraph.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1386_complex_flowgraph.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-105.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-105.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-139.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-139.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-139.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-145.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-145.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue-eacsl-91.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_issue-eacsl-91.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c rename to src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-105.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-105.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-105.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-139.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-139.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-139.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-139.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-145.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-145.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-91.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-91.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/issue-eacsl-91.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/issue-eacsl-91.res.oracle diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/issue69.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/bts/oracle_ci/issue69.res.oracle rename to src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/builtin_literal_string.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string.res.oracle rename to src/plugins/e-acsl/tests/builtin/oracle/builtin_literal_string.res.oracle diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string_local_init.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/builtin_literal_string_local_init.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/builtin_literal_string_local_init.res.oracle rename to src/plugins/e-acsl/tests/builtin/oracle/builtin_literal_string_local_init.res.oracle diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string.c similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string.c rename to src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string.c diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string_local_init.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string_local_init.c similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/gen_builtin_literal_string_local_init.c rename to src/plugins/e-acsl/tests/builtin/oracle/gen_builtin_literal_string_local_init.c diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c rename to src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c rename to src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c rename to src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c rename to src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle rename to src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle rename to src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle rename to src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle diff --git a/src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle rename to src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle diff --git a/src/plugins/e-acsl/tests/builtin/test_config_ci b/src/plugins/e-acsl/tests/builtin/test_config similarity index 100% rename from src/plugins/e-acsl/tests/builtin/test_config_ci rename to src/plugins/e-acsl/tests/builtin/test_config diff --git a/src/plugins/e-acsl/tests/constructs/decrease.i b/src/plugins/e-acsl/tests/constructs/decrease.i index 569bcb71d0f339ffec25afb1935e3da6e30b0053..4bb96675366a34026d543101466313a8add9cb9e 100644 --- a/src/plugins/e-acsl/tests/constructs/decrease.i +++ b/src/plugins/e-acsl/tests/constructs/decrease.i @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config STDOPT: +"-eva-unroll-recursive-calls 10 -eva-slevel 7" */ diff --git a/src/plugins/e-acsl/tests/constructs/invariant.i b/src/plugins/e-acsl/tests/constructs/invariant.i index 8bc1eeee091a422a69c6b9ad3d8f2454f1b6e7c8..6458296dc3d3cce7f5f97b3a143928d0e960516a 100644 --- a/src/plugins/e-acsl/tests/constructs/invariant.i +++ b/src/plugins/e-acsl/tests/constructs/invariant.i @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: invariant STDOPT: +"-eva-slevel 11" */ diff --git a/src/plugins/e-acsl/tests/constructs/loop.i b/src/plugins/e-acsl/tests/constructs/loop.i index bbab3b09f21b67d29a1dda970db34f0b93f9f35b..a2349e8dd1c0c989e636385246d1eb68281342a3 100644 --- a/src/plugins/e-acsl/tests/constructs/loop.i +++ b/src/plugins/e-acsl/tests/constructs/loop.i @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: loop invariants STDOPT: +"-eva-slevel 160" */ diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/acsl_check.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/acsl_check.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/acsl_check.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/acsl_check.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/decrease.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/decrease.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/decrease.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/false.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/false.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/false.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/false.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/function_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/function_contract.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/function_contract.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/function_contract.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_acsl_check.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_acsl_check.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_acsl_check.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_acsl_check.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_decrease.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_decrease.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_false.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_false.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_function_contract.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_ghost.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_invariant.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_labeled_stmt.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_lazy.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_loop.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_nested_code_annot.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_result.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_result.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_rte.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_rte.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_rte.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_stmt_contract.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_true.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_true.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c rename to src/plugins/e-acsl/tests/constructs/oracle/gen_typedef.c diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/ghost.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/ghost.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/ghost.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/ghost.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/invariant.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/invariant.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/invariant.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/invariant.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/labeled_stmt.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/labeled_stmt.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/labeled_stmt.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/lazy.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/lazy.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/lazy.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/lazy.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/loop.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/loop.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/loop.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/loop.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/nested_code_annot.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/nested_code_annot.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/nested_code_annot.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/result.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/result.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/result.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/result.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/rte.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/rte.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/rte.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/rte.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/stmt_contract.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/stmt_contract.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/true.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/true.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/true.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/true.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/oracle_ci/typedef.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle/typedef.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/constructs/oracle_ci/typedef.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle/typedef.res.oracle diff --git a/src/plugins/e-acsl/tests/constructs/rte.i b/src/plugins/e-acsl/tests/constructs/rte.i index f80f978c8f7e5b359989b0639da72935e11e9c07..8b4578d3b3f81bac3883f9486e5da3c199631b6a 100644 --- a/src/plugins/e-acsl/tests/constructs/rte.i +++ b/src/plugins/e-acsl/tests/constructs/rte.i @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config * COMMENT: Check that the RTE checks are generated for every part of a * behavior, and are generated at the right place. */ diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/examples/oracle_ci/functions_contiki.res.oracle rename to src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c similarity index 100% rename from src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c rename to src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c similarity index 100% rename from src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c rename to src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c diff --git a/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle rename to src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle diff --git a/src/plugins/e-acsl/tests/format/fprintf.c b/src/plugins/e-acsl/tests/format/fprintf.c index 562a89a4f6be9b0398ea3cf9857d2acffd570fe1..47b1fb5d4c3d113ab7247769f78ee5520a56549d 100644 --- a/src/plugins/e-acsl/tests/format/fprintf.c +++ b/src/plugins/e-acsl/tests/format/fprintf.c @@ -1,4 +1,4 @@ -/* run.config_ci,run.config_dev +/* run.config,run.config_dev COMMENT: Check behaviours of format functions */ diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle rename to src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c similarity index 100% rename from src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c rename to src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle/gen_printf.c similarity index 100% rename from src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c rename to src/plugins/e-acsl/tests/format/oracle/gen_printf.c diff --git a/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle rename to src/plugins/e-acsl/tests/format/oracle/printf.res.oracle diff --git a/src/plugins/e-acsl/tests/format/printf.c b/src/plugins/e-acsl/tests/format/printf.c index 9120259d2bc1a4629f7a8c2ae1962ca80b5b3d60..ec4a162e3da4e18f6b1408094fa6007e05c630e3 100644 --- a/src/plugins/e-acsl/tests/format/printf.c +++ b/src/plugins/e-acsl/tests/format/printf.c @@ -1,4 +1,4 @@ -/* run.config_ci,run.config_dev +/* run.config,run.config_dev COMMENT: Check detection of format-string vulnerabilities via printf MACRO: ROOT_EACSL_GCC_OPTS_EXT @ROOT_EACSL_GCC_OPTS_EXT@ -e "-Wno-maybe-uninitialized" */ diff --git a/src/plugins/e-acsl/tests/format/test_config_ci b/src/plugins/e-acsl/tests/format/test_config similarity index 100% rename from src/plugins/e-acsl/tests/format/test_config_ci rename to src/plugins/e-acsl/tests/format/test_config diff --git a/src/plugins/e-acsl/tests/full-mtracking/addrOf.i b/src/plugins/e-acsl/tests/full-mtracking/addrOf.i index 281703719852d97b3b865510c8ea8d67c049a045..c797facb0f9c1ea90d23dd783c7e380668314ce0 100644 --- a/src/plugins/e-acsl/tests/full-mtracking/addrOf.i +++ b/src/plugins/e-acsl/tests/full-mtracking/addrOf.i @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: addrOf */ diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/addrOf.res.oracle b/src/plugins/e-acsl/tests/full-mtracking/oracle/addrOf.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/full-mtracking/oracle_ci/addrOf.res.oracle rename to src/plugins/e-acsl/tests/full-mtracking/oracle/addrOf.res.oracle diff --git a/src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c similarity index 100% rename from src/plugins/e-acsl/tests/full-mtracking/oracle_ci/gen_addrOf.c rename to src/plugins/e-acsl/tests/full-mtracking/oracle/gen_addrOf.c diff --git a/src/plugins/e-acsl/tests/full-mtracking/test_config_ci b/src/plugins/e-acsl/tests/full-mtracking/test_config similarity index 100% rename from src/plugins/e-acsl/tests/full-mtracking/test_config_ci rename to src/plugins/e-acsl/tests/full-mtracking/test_config diff --git a/src/plugins/e-acsl/tests/full-mtracking/test_config_dev b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev index 7341131a532b15723e4ea283ad68908ff7ec3917..80a939ea02713f1e0fb539f6bfb567096a7e2510 100644 --- a/src/plugins/e-acsl/tests/full-mtracking/test_config_dev +++ b/src/plugins/e-acsl/tests/full-mtracking/test_config_dev @@ -1,2 +1 @@ MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking -STDOPT: diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle rename to src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle rename to src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c similarity index 100% rename from src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c rename to src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c similarity index 100% rename from src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c rename to src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config_ci b/src/plugins/e-acsl/tests/gmp-only/test_config similarity index 100% rename from src/plugins/e-acsl/tests/gmp-only/test_config_ci rename to src/plugins/e-acsl/tests/gmp-only/test_config diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config_dev b/src/plugins/e-acsl/tests/gmp-only/test_config_dev index 17fca0a799c66f8133edd943ed1f76a484263218..3a3fc2c7e601d0b97416e7f858e9ddeee944102f 100644 --- a/src/plugins/e-acsl/tests/gmp-only/test_config_dev +++ b/src/plugins/e-acsl/tests/gmp-only/test_config_dev @@ -1,2 +1 @@ MACRO: ROOT_EACSL_GCC_OPTS_EXT --gmp -STDOPT: diff --git a/src/plugins/e-acsl/tests/memory/array_overflow.c b/src/plugins/e-acsl/tests/memory/array_overflow.c index d002e455f4975a75dc9f7a58d8bdf28f1268796b..c57e379c6c5805d53da72f3dc31d396808d10703 100644 --- a/src/plugins/e-acsl/tests/memory/array_overflow.c +++ b/src/plugins/e-acsl/tests/memory/array_overflow.c @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Array overflow */ diff --git a/src/plugins/e-acsl/tests/memory/constructor.c b/src/plugins/e-acsl/tests/memory/constructor.c index 8530264c83f3dff89a26d3dc0beaa254942795a8..4cedd70a7852643a423c4a76c61882a6e8fd6daa 100644 --- a/src/plugins/e-acsl/tests/memory/constructor.c +++ b/src/plugins/e-acsl/tests/memory/constructor.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: bts #2405. Memory not initialized for code executed before main. */ diff --git a/src/plugins/e-acsl/tests/memory/ctype_macros.c b/src/plugins/e-acsl/tests/memory/ctype_macros.c index b4ba9cc170ec6cadc01cb6fc81276bc31e3def48..82a1caf2ffd9d923187cf02cc4678c40213f8c59 100644 --- a/src/plugins/e-acsl/tests/memory/ctype_macros.c +++ b/src/plugins/e-acsl/tests/memory/ctype_macros.c @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Tests for function-based implementation of ctype.h features */ diff --git a/src/plugins/e-acsl/tests/memory/decl_in_switch.c b/src/plugins/e-acsl/tests/memory/decl_in_switch.c index bd12fc2105e2952ba6f236fb18a8c25206dacc59..59ef8bedd5e95f746b6f9d0c31aa20a887e1353c 100644 --- a/src/plugins/e-acsl/tests/memory/decl_in_switch.c +++ b/src/plugins/e-acsl/tests/memory/decl_in_switch.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: Check that variables declared in the body of switch statements are correctly tracked. */ diff --git a/src/plugins/e-acsl/tests/memory/hidden_malloc.c b/src/plugins/e-acsl/tests/memory/hidden_malloc.c index 7d220a59517efd7bd62e13946568cae3d0b613fd..a33c036ea74cbcf53c637f434e6cb2af885841de 100644 --- a/src/plugins/e-acsl/tests/memory/hidden_malloc.c +++ b/src/plugins/e-acsl/tests/memory/hidden_malloc.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: Malloc executed by a library function */ diff --git a/src/plugins/e-acsl/tests/memory/local_goto.c b/src/plugins/e-acsl/tests/memory/local_goto.c index a5448bf07063eeaa318549d0c51931ddf7357998..2defb67029366fd074c7708a3103dc7431a9947e 100644 --- a/src/plugins/e-acsl/tests/memory/local_goto.c +++ b/src/plugins/e-acsl/tests/memory/local_goto.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: Check that deleting statements before goto jumps takes into COMMENT: account variable declarations given via local inits */ diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c index 8de0529d5b4ebe3a34852ca95b5cd4d28c4e9816..da9137f48c11421f055c798973e142946134bf75 100644 --- a/src/plugins/e-acsl/tests/memory/local_init.c +++ b/src/plugins/e-acsl/tests/memory/local_init.c @@ -1,6 +1,5 @@ -/* run.config_ci +/* run.config COMMENT: test of a local initializer which contains an annotation - LOG: gen_@PTEST_NAME@.c STDOPT: #"@MACHDEP@ -lib-entry -eva -then -no-lib-entry" */ diff --git a/src/plugins/e-acsl/tests/memory/memsize.c b/src/plugins/e-acsl/tests/memory/memsize.c index 2260a306878d6dfd4943d73ccbddc6436c2ec2f5..ca285b6115b01f0a911aa2e93c03d56e7cab749f 100644 --- a/src/plugins/e-acsl/tests/memory/memsize.c +++ b/src/plugins/e-acsl/tests/memory/memsize.c @@ -1,4 +1,4 @@ -/* run.config_ci +/* run.config COMMENT: Checking heap memory size STDOPT: +"-eva-no-builtins-auto" */ diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/addrOf.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/addrOf.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/alias.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/array_overflow.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/array_overflow.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/array_overflow.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/array_overflow.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/base_addr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/base_addr.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/block_length.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/block_length.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/block_valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/block_valid.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/bypassed_var.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/call.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/call.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/call.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/call.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/compound_initializers.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/early_exit.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/early_exit.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/errno.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/errno.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/freeable.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/freeable.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_alias.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_array_overflow.c b/src/plugins/e-acsl/tests/memory/oracle/gen_array_overflow.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_array_overflow.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_array_overflow.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c b/src/plugins/e-acsl/tests/memory/oracle/gen_call.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_call.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_errno.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_ghost_parameters.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_ghost_parameters.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_goto.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_init.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle/gen_null.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_null.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_offset.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c b/src/plugins/e-acsl/tests/memory/oracle/gen_separated.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_separated.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_separated.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c b/src/plugins/e-acsl/tests/memory/oracle/gen_struct_initialized.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_struct_initialized.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_struct_initialized.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_valid.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_vector.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c rename to src/plugins/e-acsl/tests/memory/oracle/gen_vla.c diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ghost_parameters.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/ghost_parameters.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/ghost_parameters.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/goto.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/init.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/init.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/init_function.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/initialized.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/literal_string.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/literal_string.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/local_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle similarity index 70% rename from src/plugins/e-acsl/tests/memory/oracle_ci/local_init.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle index e5104fb7e863db59eeb9c0c2a6e355a0e5b6a167..05cabd8f3024c932301660d16157e52707d6e787 100644 --- a/src/plugins/e-acsl/tests/memory/oracle_ci/local_init.res.oracle +++ b/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle @@ -1,4 +1,4 @@ -[eva:alarm] tests/memory/local_init.c:11: Warning: +[eva:alarm] tests/memory/local_init.c:10: Warning: out of bounds read. assert \valid_read(p); [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/local_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/local_var.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/null.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/null.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/null.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/null.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/offset.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/offset.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/other_constants.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/other_constants.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ptr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/ptr.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ptr_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/ptr_init.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/separated.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/separated.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/separated.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/sizeof.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/sizeof.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/stdout.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/struct_initialized.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/struct_initialized.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/struct_initialized.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/valid.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/valid_alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/valid_alias.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/valid_in_contract.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/vector.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle rename to src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle diff --git a/src/plugins/e-acsl/tests/memory/separated.c b/src/plugins/e-acsl/tests/memory/separated.c index 872cba8db9d97a4cd3e2cf835109049747077274..4df0b435e5c0936e4e5b1d02f95c48492de66b2e 100644 --- a/src/plugins/e-acsl/tests/memory/separated.c +++ b/src/plugins/e-acsl/tests/memory/separated.c @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: \separated */ diff --git a/src/plugins/e-acsl/tests/special/builtin.i b/src/plugins/e-acsl/tests/special/builtin.i index 3b7f9c7f4b99c25f238acc91271d0e222e6f1e18..fa933a4b19c280e39924ad73594bdb58270ca90e 100644 --- a/src/plugins/e-acsl/tests/special/builtin.i +++ b/src/plugins/e-acsl/tests/special/builtin.i @@ -1,6 +1,8 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: -e-acsl-builtins STDOPT: #"-e-acsl-builtins incr" +*/ +/* run.config_dev MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-builtins incr */ diff --git a/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c b/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c index efdd82a5ee0f2c74f1cc055f005cb40cce853a5d..cefea47b8a6f006a274669e79ef60cc94eddfa0e 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-bittree-model.c @@ -1,6 +1,8 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Compile RTL with bittree memory model STDOPT:#"-e-acsl-full-mtracking" + */ +/* run.config_dev MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model bittree */ int main() { diff --git a/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c b/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c index 3b5788f306a66a9598ba9e6c318fc94c8fde7aae..6454a92893b1c084a563d6d22cfc5326636a52e8 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config_dev COMMENT: Compile dlmalloc from sources with this file MACRO: ROOT_EACSL_GCC_OPTS_EXT --dlmalloc-from-sources */ diff --git a/src/plugins/e-acsl/tests/special/e-acsl-functions.c b/src/plugins/e-acsl/tests/special/e-acsl-functions.c index 5838bd1de677255f88cea71841ecb916e1cb6344..fa843b0f065c6489e44da9659211cd3e729f8acf 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-functions.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-functions.c @@ -1,6 +1,8 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: test option -e-acsl-functions STDOPT: #"-e-acsl-functions f" +*/ +/* run.config_dev MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-functions f */ diff --git a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c index 3e02977ecd65d1da1459b59dfa8cdca6227eb2cc..97b8c72a7791d5b1e13fe19ddf9d379b8328846b 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c @@ -1,6 +1,8 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: test option -e-acsl-instrument; cannot run Eva on this example STDOPT:#"-e-acsl-instrument='@all,-uninstrument1,-uninstrument2'" +*/ +/* run.config_dev MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -e-acsl-instrument @all,-uninstrument1,-uninstrument2 */ diff --git a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c index 8d050c12439f462c3148f4f3dcde4456249f974c..6964a4e84d91b7633603365c9122606873119ec0 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c @@ -1,6 +1,8 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Compile RTL with debug and debug verbose informations STDOPT:#"-e-acsl-debug 1" + */ +/* run.config_dev MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose */ int main() { diff --git a/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c index d9bf523c54916e4d2decf42fe5b3342b3415c9ba..70b91066513425041600670857fade2163792628 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-segment-model.c @@ -1,6 +1,8 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Compile RTL with segment memory model STDOPT:#"-e-acsl-full-mtracking" + */ +/* run.config_dev MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --memory-model segment */ int main() { diff --git a/src/plugins/e-acsl/tests/special/e-acsl-valid.c b/src/plugins/e-acsl/tests/special/e-acsl-valid.c index f84464d00758640dd8187876d1d0cd3bcefbcf50..44ad91d51e2abacbfa432bcae6866458f28bbcb8 100644 --- a/src/plugins/e-acsl/tests/special/e-acsl-valid.c +++ b/src/plugins/e-acsl/tests/special/e-acsl-valid.c @@ -1,6 +1,8 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: test option -e-acsl-no-valid STDOPT: #"@GLOBAL@ -eva -eva-verbose 0 -then -no-eva -e-acsl-no-valid" +*/ +/* run.config_dev MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -eva -eva-verbose 0 MACRO: ROOT_EACSL_GCC_OPTS_EXT --then --e-acsl-extra -e-acsl-no-valid */ diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.res.oracle similarity index 73% rename from src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/builtin.res.oracle index f829e96e46483dba4975d357c55444c4b1fba88d..ea338178977c5f4bea94846045470cd18c837b9a 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle +++ b/src/plugins/e-acsl/tests/special/oracle/builtin.res.oracle @@ -1,4 +1,4 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] tests/special/builtin.i:9: Warning: +[eva:alarm] tests/special/builtin.i:11: Warning: function __gen_e_acsl_f: postcondition got status unknown. diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-bittree-model.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-bittree-model.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/e-acsl-bittree-model.res.oracle diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-compile-dlmalloc.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-compile-dlmalloc.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-compile-dlmalloc.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/e-acsl-compile-dlmalloc.res.oracle diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle similarity index 69% rename from src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-functions.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle index 4661ead8e7059ddb6a7055c38aa6b21734ab6e5c..2c2f479abd8ae3c4f16bd78bcd19837fdac4fa00 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-functions.res.oracle +++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle @@ -1,4 +1,4 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] tests/special/e-acsl-functions.c:29: Warning: +[eva:alarm] tests/special/e-acsl-functions.c:31: Warning: function g: precondition *p ≡ 1 got status invalid. diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-rt-debug.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-rt-debug.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/e-acsl-rt-debug.res.oracle diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-segment-model.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-segment-model.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/e-acsl-segment-model.res.oracle diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.res.oracle similarity index 66% rename from src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle rename to src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.res.oracle index c14797a555bdba95b34959513897aa0d8b0e6455..3962383599fc1456473a1779f7639fbac2166bdf 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle +++ b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.res.oracle @@ -1,10 +1,10 @@ -[eva:alarm] tests/special/e-acsl-valid.c:37: Warning: +[eva:alarm] tests/special/e-acsl-valid.c:39: Warning: function f: precondition \valid(y) got status unknown. [e-acsl] beginning translation. -[e-acsl] tests/special/e-acsl-valid.c:28: Warning: +[e-acsl] tests/special/e-acsl-valid.c:30: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. -[e-acsl] tests/special/e-acsl-valid.c:24: Warning: +[e-acsl] tests/special/e-acsl-valid.c:26: Warning: E-ACSL construct `assigns clause in behavior' is not yet supported. Ignoring annotation. [e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c similarity index 95% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c rename to src/plugins/e-acsl/tests/special/oracle/gen_builtin.c index 6f5f431cd7548efe614f44aaf740829d590d387c..dad8120db26c802a2abfaa86a7f8d6e035a998f1 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c +++ b/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c @@ -40,7 +40,8 @@ int __gen_e_acsl_f(int i) int __gen_e_acsl_incr_app; __gen_e_acsl_incr_app = incr(__gen_e_acsl_at); __e_acsl_assert(__retres == __gen_e_acsl_incr_app,1,"Postcondition","f", - "\\result == incr(\\old(i))","tests/special/builtin.i",9); + "\\result == incr(\\old(i))","tests/special/builtin.i", + 11); return __retres; } } diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-bittree-model.c rename to src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-bittree-model.c diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-compile-dlmalloc.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-compile-dlmalloc.c rename to src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-compile-dlmalloc.c diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c similarity index 89% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c rename to src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c index d238464570c4ffc37cb18c6e8d7435e2f805b456..f94e292fc4234e8a9714433db943824ea6ea9922 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c +++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c @@ -19,7 +19,7 @@ int f(int *p) int __gen_e_acsl_and; if (0 <= i) __gen_e_acsl_and = i <= 1; else __gen_e_acsl_and = 0; __e_acsl_assert(__gen_e_acsl_and,1,"Invariant","f","0 <= i <= 1", - "tests/special/e-acsl-functions.c",11); + "tests/special/e-acsl-functions.c",13); } /*@ loop invariant 0 ≤ i ≤ 1; */ while (i < 1) { @@ -27,7 +27,7 @@ int f(int *p) i ++; if (0 <= i) __gen_e_acsl_and_2 = i <= 1; else __gen_e_acsl_and_2 = 0; __e_acsl_assert(__gen_e_acsl_and_2,1,"Invariant","f","0 <= i <= 1", - "tests/special/e-acsl-functions.c",11); + "tests/special/e-acsl-functions.c",13); } } __retres = 0; @@ -81,14 +81,14 @@ int __gen_e_acsl_f(int *p) __e_acsl_store_block((void *)(& p),(size_t)8); __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int)); __e_acsl_assert(__gen_e_acsl_initialized,1,"Precondition","f", - "\\initialized(p)","tests/special/e-acsl-functions.c",7); + "\\initialized(p)","tests/special/e-acsl-functions.c",9); __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int), (void *)p,(void *)(& p)); __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f", "mem_access: \\valid_read(p)", - "tests/special/e-acsl-functions.c",8); + "tests/special/e-acsl-functions.c",10); __e_acsl_assert(*p == 0,1,"Precondition","f","*p == 0", - "tests/special/e-acsl-functions.c",8); + "tests/special/e-acsl-functions.c",10); } { int __gen_e_acsl_valid_read_2; @@ -96,13 +96,13 @@ int __gen_e_acsl_f(int *p) (void *)p,(void *)(& p)); __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","f", "mem_access: \\valid_read(p)", - "tests/special/e-acsl-functions.c",9); + "tests/special/e-acsl-functions.c",11); __gen_e_acsl_at = *p; } __retres = f(p); __e_acsl_assert(__retres == __gen_e_acsl_at,1,"Postcondition","f", "\\result == \\old(*p)","tests/special/e-acsl-functions.c", - 9); + 11); __e_acsl_delete_block((void *)(& p)); return __retres; } diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c similarity index 98% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c rename to src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c index c56ee16b78b3a36e0e91479b02110be6524b942e..61a4e7c62bdaca2fcdeb4e0058b468ecf89b4797 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c +++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c @@ -100,7 +100,7 @@ int main(void) sizeof(int)); __e_acsl_assert(__gen_e_acsl_initialized,1,"Assertion","main", "\\initialized(&x)","tests/special/e-acsl-instrument.c", - 56); + 58); } /*@ assert \initialized(&x); */ ; { @@ -109,7 +109,7 @@ int main(void) sizeof(int)); __e_acsl_assert(__gen_e_acsl_initialized_2,1,"Assertion","main", "\\initialized(&y)","tests/special/e-acsl-instrument.c", - 57); + 59); } /*@ assert \initialized(&y); */ ; { @@ -139,7 +139,7 @@ int __gen_e_acsl_instrument2(int *p) __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p, (void *)(& p)); __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","instrument2", - "\\valid(p)","tests/special/e-acsl-instrument.c",29); + "\\valid(p)","tests/special/e-acsl-instrument.c",31); } __retres = instrument2(p); __e_acsl_delete_block((void *)(& p)); @@ -155,7 +155,7 @@ int __gen_e_acsl_uninstrument2(int *p) __gen_e_acsl_valid = __e_acsl_valid((void *)p,sizeof(int),(void *)p, (void *)(& p)); __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","uninstrument2", - "\\valid(p)","tests/special/e-acsl-instrument.c",14); + "\\valid(p)","tests/special/e-acsl-instrument.c",16); } __e_acsl_sound_verdict = 0; __retres = uninstrument2(p); diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-rt-debug.c rename to src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-rt-debug.c diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c similarity index 100% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-segment-model.c rename to src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-segment-model.c diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c similarity index 91% rename from src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c rename to src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c index d16e2cf103ff3562f7b464cbf1fd0f7fa813c820..91bf7941f61c7da887f82376a49311743af8e827 100644 --- a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c +++ b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c @@ -35,9 +35,9 @@ void f(int *x, int *y) (void *)x,(void *)(& x)); __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f", "mem_access: \\valid_read(x)", - "tests/special/e-acsl-valid.c",25); + "tests/special/e-acsl-valid.c",27); __e_acsl_assert(*x >= 0,1,"Precondition","f","*x >= 0", - "tests/special/e-acsl-valid.c",25); + "tests/special/e-acsl-valid.c",27); } /*@ requires *x ≥ 0; ensures 2 ≥ 1; @@ -47,7 +47,7 @@ void f(int *x, int *y) (*x) ++; } __e_acsl_assert(1,1,"Postcondition","f","2 >= 1", - "tests/special/e-acsl-valid.c",26); + "tests/special/e-acsl-valid.c",28); { int i = 0; /*@ loop invariant 0 ≤ i ≤ 1; @@ -60,10 +60,10 @@ void f(int *x, int *y) i ++; __e_acsl_assert(__gen_e_acsl_old_variant >= 0L,1,"Variant","f", "(old 2 - i) \342\211\245 0", - "tests/special/e-acsl-valid.c",31); + "tests/special/e-acsl-valid.c",33); __e_acsl_assert(__gen_e_acsl_old_variant > 2L - i,1,"Variant","f", "(old 2 - i) > 2 - i","tests/special/e-acsl-valid.c", - 31); + 33); } } __e_acsl_delete_block((void *)(& y)); @@ -122,30 +122,30 @@ void __gen_e_acsl_f(int *x, int *y) (void *)x,(void *)(& x)); __e_acsl_assert(__gen_e_acsl_valid_read,1,"RTE","f", "mem_access: \\valid_read(x)", - "tests/special/e-acsl-valid.c",15); + "tests/special/e-acsl-valid.c",17); __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)0, *x == 1); __gen_e_acsl_valid_read_2 = __e_acsl_valid_read((void *)x,sizeof(int), (void *)x,(void *)(& x)); __e_acsl_assert(__gen_e_acsl_valid_read_2,1,"RTE","f", "mem_access: \\valid_read(x)", - "tests/special/e-acsl-valid.c",19); + "tests/special/e-acsl-valid.c",21); __e_acsl_contract_set_behavior_assumes(__gen_e_acsl_contract,(size_t)1, *x == 0); __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y, (void *)(& y)); __e_acsl_assert(__gen_e_acsl_valid,1,"Precondition","f","\\valid(y)", - "tests/special/e-acsl-valid.c",10); + "tests/special/e-acsl-valid.c",12); __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors ((__e_acsl_contract_t const *)__gen_e_acsl_contract); __e_acsl_assert(__gen_e_acsl_active_bhvrs >= 1,1,"Precondition","f", "all behaviors complete","tests/special/e-acsl-valid.c", - 24); + 26); __gen_e_acsl_active_bhvrs = __e_acsl_contract_partial_count_all_behaviors ((__e_acsl_contract_t const *)__gen_e_acsl_contract); __e_acsl_assert(__gen_e_acsl_active_bhvrs <= 1,1,"Precondition","f", "all behaviors disjoint","tests/special/e-acsl-valid.c", - 24); + 26); } f(x,y); __e_acsl_contract_clean(__gen_e_acsl_contract); 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 be2b0df1fe6c6690b52b135e60671d8a735a3722..fe20ca61ec1fab5d249d345701b0e4e63a2d63b8 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,16 @@ tests/special/e-acsl-instrument.c: In function 'instrument2' -tests/special/e-acsl-instrument.c:29: Warning: no sound verdict for Precondition (guess: ok). +tests/special/e-acsl-instrument.c:31: Warning: no sound verdict for Precondition (guess: ok). the considered predicate is: \valid(p) tests/special/e-acsl-instrument.c: In function 'uninstrument2' -tests/special/e-acsl-instrument.c:14: Warning: no sound verdict for Precondition (guess: ok). +tests/special/e-acsl-instrument.c:16: Warning: no sound verdict for Precondition (guess: ok). the considered predicate is: \valid(p) tests/special/e-acsl-instrument.c: In function 'main' -tests/special/e-acsl-instrument.c:56: Warning: no sound verdict for Assertion (guess: ok). +tests/special/e-acsl-instrument.c:58: Warning: no sound verdict for Assertion (guess: ok). the considered predicate is: \initialized(&x) tests/special/e-acsl-instrument.c: In function 'main' -tests/special/e-acsl-instrument.c:57: Warning: no sound verdict for Assertion (guess: ok). +tests/special/e-acsl-instrument.c:59: Warning: no sound verdict for Assertion (guess: ok). the considered predicate is: \initialized(&y) diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c rename to src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_addr-by-val.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_addr-by-val.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_args.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_args.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_array.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_array.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_array.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_array.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_char.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_char.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_char.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_char.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_darray.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_darray.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_darray.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_darray.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_dpointer.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fptr.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_fptr.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_fptr.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_ptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_ptr.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_global_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_global_init.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_global_init.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_global_init.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_labels.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_labels.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_labels.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_labels.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_lit_string.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_lit_string.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_local_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_local_init.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_local_init.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_local_init.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc-asan.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_struct.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_struct.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_struct.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_struct.res.oracle diff --git a/src/plugins/e-acsl/tests/temporal/oracle_ci/t_while.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/temporal/oracle_ci/t_while.res.oracle rename to src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle 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 b847786468f62551a3b2b1ac91111f49e883c423..562cc4e026c35f45fdeb94e9e2c0b3aa32a65bf2 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_ci, run.config_dev +/* run.config 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 8d5a4b9a8eaaf6940e28365b5f7e6e709801a649..c48b3e093e24048261d1b2db5c1b19ca0a608591 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_ci, run.config_dev +/* run.config 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 f4166ccf69aeb1db1305d8dfeade9f84fabb1369..ff2e8be836240ac5e912b987a75f6279d755f697 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_ci, run.config_dev +/* run.config 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 6cd778f70977b16bc85b2c0bb16af2103e78f68f..e8f001a3a72234a6f6a1a7073b8ce02c82d9cd1f 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_ci, run.config_dev +/* run.config 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 5130ef693dfea9d778f0dc8b4713c5dc360165f0..88c1cf9712022c1c32ccf47259fe968c4f633f5b 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_ci, run.config_dev +/* run.config 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 ede8f8b481c202fae55e63c1b220191aa774ce01..215ede69a5ac728d2b0a61f805a1711ed12f1d45 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_ci, run.config_dev +/* run.config 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 e0f605d3ab0de91f4b0aa2cdaec73d41486df3d4..0afcc96640d51099799db3fc1e9b96033fbb43a2 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_ci, run.config_dev +/* run.config 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 f5a7f077f94dc05a6f5a58513db7d87fc30933be..d98643937bbd1161685ee1a6b7e265d41f53e0c1 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_ci, run.config_dev +/* run.config 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 fc0e99b84953c08242632d30f2be91e0baba8dac..d0637544973e1bac493f0bc6e51b672fe7863aba 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_ci, run.config_dev +/* run.config 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 016779b79af71d409e27a61d458af4249df331ed..1bb3e9a7d47b6ceafbfae6a9d2efc32b3fc76a94 100644 --- a/src/plugins/e-acsl/tests/temporal/t_getenv.c +++ b/src/plugins/e-acsl/tests/temporal/t_getenv.c @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Check temporal validity of environment string (via getenv function) */ 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 fa46d21a401e9ca8dbe0509f68c55ef6eb87f5e0..e6edd0e607f64408c6859d400df6d61aeb4f5c06 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_ci, run.config_dev +/* run.config 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 c9afc1ad4ccb053c19aa6ad104dc4807a91cb8ae..5d82c469b0fca0fea19e9c8867e9f6d1d05a8d60 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_ci, run.config_dev +/* run.config 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 634c6875cbea95e70faf24e1fac9f1d448517ca7..2469f352b4105cbdafccc9422054e0724ad84100 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_ci, run.config_dev +/* run.config 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 0a819870904c6ddac5311a0d875df1d19ad27f02..01afaf3dbcc4216c7b0c5d3d85ef91fb51e63a5d 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_ci, run.config_dev +/* run.config 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 542afcfa3701af31353d28b4635d2a0b631ec988..78f96e9145f8a1189dab9aad45a56ea0b1da1fd4 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_ci, run.config_dev +/* run.config 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 531c2053098ef90b313bd5616830c3b3f4792b49..9ae3b5d0a280fb86e55ce5f5f18fc32bc2022c58 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_ci, run.config_dev +/* run.config 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 250632f587345a6956b1c5ce31b6624792f2acd9..de4c6dc3bd74585c4c3d4a43b8ca669bc4c65733 100644 --- a/src/plugins/e-acsl/tests/temporal/t_scope.c +++ b/src/plugins/e-acsl/tests/temporal/t_scope.c @@ -1,4 +1,4 @@ -/* run.config_ci, run.config_dev +/* run.config COMMENT: Temporal analysis with respect to scopes */ diff --git a/src/plugins/e-acsl/tests/temporal/t_struct.c b/src/plugins/e-acsl/tests/temporal/t_struct.c index dd3526dc565ea0211752d0b2e649065e070ab578..e72e879cf605c315e6b69d6579dc479e4e6648f2 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_ci, run.config_dev +/* run.config 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 05a506120b1b6a69f425500bf441ba3fcc553e26..7f39075385affd69ef3175b72ce9090142ca9b59 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_ci, run.config_dev +/* run.config 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_ci b/src/plugins/e-acsl/tests/temporal/test_config similarity index 100% rename from src/plugins/e-acsl/tests/temporal/test_config_ci rename to src/plugins/e-acsl/tests/temporal/test_config diff --git a/src/plugins/e-acsl/tests/temporal/test_config_dev b/src/plugins/e-acsl/tests/temporal/test_config_dev index ddff8508c1e18074db4e26c6d93ee182b04ec0fc..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 @@ MACRO: ROOT_EACSL_GCC_OPTS_EXT --temporal -STDOPT: diff --git a/src/plugins/e-acsl/tests/test_config_ci.in b/src/plugins/e-acsl/tests/test_config.in similarity index 100% rename from src/plugins/e-acsl/tests/test_config_ci.in rename to src/plugins/e-acsl/tests/test_config.in