[tests] config ci

src/plugins/e-acsl/.gitignore

@@ -54,7 +54,9 @@
 /tests/*.annot
 /tests/*_DEP
 /tests/test_config
-/tests/*/result/*
+/tests/test_config_ci
+/tests/test_config_dev
+/tests/*/result*/*
 /tests/check/obj/*
 .frama-c
 tests/ptests_config

src/plugins/e-acsl/Makefile.in

@@ -181,27 +181,37 @@ PLUGIN_TESTS_DIRS := \
 	format \
 	temporal \
 	special
-
 # [JS 2019/02/26] deactivate tests 'builtin' as long as setjmp/longjmp is not
 # supported.
-#	builtin \
+#	builtin
+
+PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.cmxs
+
+DEV=
+ifeq ("$(DEV)","yes")
+  EACSL_TEST_CONFIG=dev
+else
+  EACSL_TEST_CONFIG:=ci
+endif
+PLUGIN_PTESTS_OPTS:=-config $(EACSL_TEST_CONFIG)
 
-PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
-E_ACSL_TESTS: $(EACSL_PLUGIN_DIR)/tests/test_config
+E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: \
+	$(EACSL_PLUGIN_DIR)/tests/ptests_config \
+	$(EACSL_PLUGIN_DIR)/tests/test_config_$(EACSL_TEST_CONFIG)
 
-E_ACSL_DEFAULT_TESTS: \
-	$(EACSL_PLUGIN_DIR)/tests/test_config \
-	$(EACSL_PLUGIN_DIR)/tests/print.cmxs \
-	$(EACSL_PLUGIN_DIR)/tests/print.cmo
+$(EACSL_PLUGIN_DIR)/tests/test_config_ci: \
+		$(EACSL_PLUGIN_DIR)/tests/test_config_ci.in \
+		$(EACSL_PLUGIN_DIR)/Makefile
+	$(PRINT_MAKING) $@
+	$(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
 
-$(EACSL_PLUGIN_DIR)/tests/test_config: \
-		$(EACSL_PLUGIN_DIR)/tests/test_config.in \
+$(EACSL_PLUGIN_DIR)/tests/test_config_dev: \
+		$(EACSL_PLUGIN_DIR)/tests/test_config_dev.in \
 		$(EACSL_PLUGIN_DIR)/Makefile
 	$(PRINT_MAKING) $@
 	$(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
 
-tests:: $(EACSL_PLUGIN_DIR)/tests/ptests_config \
-	$(EACSL_PLUGIN_DIR)/tests/print.cmxs
+tests:: $(EACSL_PLUGIN_DIR)/tests/ptests_config
 
 clean::
 	for d in $(E_ACSL_EXTRA_DIRS); do \

src/plugins/e-acsl/tests/memory/decl_in_switch.c → src/plugins/e-acsl/known_bugs/decl_in_switch.c

-/* run.config
+/* run.config_ci
    DONTRUN:
    COMMENT: Variables declared in the body of switch statements so far cannot
    COMMENT: be tracked

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

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

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

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

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

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