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/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/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/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/gmp-only/test_config b/src/plugins/e-acsl/tests/gmp-only/test_config new file mode 100644 index 0000000000000000000000000000000000000000..e69447aecb415446e1813d1d1154ecdbb77a0a57 --- /dev/null +++ b/src/plugins/e-acsl/tests/gmp-only/test_config @@ -0,0 +1 @@ +STDOPT: #"-e-acsl-gmp-only" 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/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