Merge branch 'feature/basile/eacsl-remove-config-ci' into 'master'

[eacsl] Replace CI test config with default test config

See merge request frama-c/frama-c!3236

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

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/* \
   )
 

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

src/plugins/e-acsl/tests/arith/array.i

-/* run.config_ci
+/* run.config
    COMMENT: arrays
    STDOPT: #"-eva-slevel 5"
 */

src/plugins/e-acsl/tests/arith/bitwise.c

-/* 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>
 

src/plugins/e-acsl/tests/arith/functions_rec.c

-/* run.config_ci
+/* run.config
    COMMENT: recursive logic functions
    STDOPT: +"-eva-unroll-recursive-calls 100"
 */

src/plugins/e-acsl/tests/arith/longlong.i

-/* run.config_ci
+/* run.config
    COMMENT: upgrading longlong to GMP
    STDOPT: +"-eva-unroll-recursive-calls 8"
 */

src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle → src/plugins/e-acsl/tests/arith/oracle/bitwise.res.oracle

 [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.