From 6b1da34ed53309e539df26d5e270e76394270da7 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 16 Jun 2021 10:44:21 +0200
Subject: [PATCH] [eacsl] Replace CI test config with default test config
---
src/plugins/e-acsl/.gitignore | 1 +
src/plugins/e-acsl/Makefile.in | 37 ++++++++++---------
src/plugins/e-acsl/headers/header_spec.txt | 12 +++---
.../builtin/{test_config_ci => test_config} | 0
.../format/{test_config_ci => test_config} | 0
.../{test_config_ci => test_config} | 0
src/plugins/e-acsl/tests/gmp-only/test_config | 1 +
.../temporal/{test_config_ci => test_config} | 0
.../{test_config_ci.in => test_config.in} | 0
9 files changed, 27 insertions(+), 24 deletions(-)
rename src/plugins/e-acsl/tests/builtin/{test_config_ci => test_config} (100%)
rename src/plugins/e-acsl/tests/format/{test_config_ci => test_config} (100%)
rename src/plugins/e-acsl/tests/full-mtracking/{test_config_ci => test_config} (100%)
create mode 100644 src/plugins/e-acsl/tests/gmp-only/test_config
rename src/plugins/e-acsl/tests/temporal/{test_config_ci => test_config} (100%)
rename src/plugins/e-acsl/tests/{test_config_ci.in => test_config.in} (100%)
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 5543dbdb43e..571f4326b06 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 b2befe524f2..bc2d25e3ede 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 82e0dc5a87c..7f24e72705c 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 00000000000..e69447aecb4
--- /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
--
GitLab