diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index 38cfd1166919ebd0d70f72f08f076048ed551d26..f5ee39fdfacb148fe2e6ab6c724865925290ea92 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/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
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index c65ee7fc37ac62d05fe10711f2df2c334cf27b75..587c8d50c53781efe1340e2a46672b9b449418e7 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/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 \
diff --git a/src/plugins/e-acsl/tests/memory/decl_in_switch.c b/src/plugins/e-acsl/known_bugs/decl_in_switch.c
similarity index 94%
rename from src/plugins/e-acsl/tests/memory/decl_in_switch.c
rename to src/plugins/e-acsl/known_bugs/decl_in_switch.c
index 4914dfe74a3f67fc2cf0914437a93c4ce020dbc1..16ddbbf61bb37e21594a834a8130c0b82062fb0c 100644
--- a/src/plugins/e-acsl/tests/memory/decl_in_switch.c
+++ b/src/plugins/e-acsl/known_bugs/decl_in_switch.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
DONTRUN:
COMMENT: Variables declared in the body of switch statements so far cannot
COMMENT: be tracked
diff --git a/src/plugins/e-acsl/tests/arith/array.i b/src/plugins/e-acsl/tests/arith/array.i
index 8e988f14f86815cf8dbb0be0a22f8864ab29c7ba..6211cf0950134f6a9c05becab68884473392be21 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
+/* run.config_ci
COMMENT: arrays
STDOPT: #"-slevel 5"
*/
diff --git a/src/plugins/e-acsl/tests/arith/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
index f875751830f2c898213468d691b395a2ed642b2f..8feb6f4e59dde504eb7ad2e4374c94867e39802a 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
+/* run.config_ci
COMMENT: recursive logic functions
STDOPT: +"-eva-ignore-recursive-calls"
*/
diff --git a/src/plugins/e-acsl/tests/arith/longlong.i b/src/plugins/e-acsl/tests/arith/longlong.i
index e013c42e76bbfafbd10611ddfa80ab90567ba575..9be4c44511b20d6b432aee24fd7b92f026d3cd9f 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
+/* run.config_ci
COMMENT: upgrading longlong to GMP
STDOPT: +"-eva-ignore-recursive-calls"
*/
diff --git a/src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/arith.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/array.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/array.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/array.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/at.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/at_on-purely-logic-variables.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/cast.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/cast.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/comparison.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/comparison.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/functions.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/functions.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/functions_rec.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_arith.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_array.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_array.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_at.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_at.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_at_on-purely-logic-variables.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_cast.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_comparison.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions_rec.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_integer_constant.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_let.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_let.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_longlong.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_not.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_not.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_quantif.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c b/src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
rename to src/plugins/e-acsl/tests/arith/oracle_ci/gen_rationals.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/integer_constant.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/integer_constant.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/let.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/let.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/longlong.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/not.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/not.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/not.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/not.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/quantif.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle_ci/rationals.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/result/.gitkeep b/src/plugins/e-acsl/tests/arith/result_ci/.gitkeep
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/result/.gitkeep
rename to src/plugins/e-acsl/tests/arith/result_ci/.gitkeep
diff --git a/src/plugins/e-acsl/tests/bts/bts1395.i b/src/plugins/e-acsl/tests/bts/bts1395.i
index 6b82653a96baf7ce2a68119d105cc35fce8a6232..ef01c83d78b3a55f12e943321f73fdc7567fe102 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
+/* run.config_ci
COMMENT: recursive function
STDOPT: +"-eva-ignore-recursive-calls"
*/
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1304.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1304.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1307.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1324.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1324.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1326.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1326.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1326.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1390.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1395.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1398.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1399.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1399.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1399.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1478.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1478.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1478.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1700.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1700.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1717.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1717.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1717.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1718.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1718.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1718.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1740.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1740.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1837.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts1837.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2191.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2191.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2191.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2192.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2231.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2231.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2231.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2252.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2252.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2305.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2305.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2305.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2386.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2386.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2386.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts2406.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/bts2406.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/bts2406.res.oracle
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1304.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1307.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1324.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1326.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1390.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1395.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1395.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1398.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1399.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1478.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1700.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1717.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1718.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1718.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1740.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1740.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts1837.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts1837.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2191.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2191.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2192.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2192.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2231.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2231.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2252.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2252.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2305.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2305.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2386.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2386.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_bts2406.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_bts2406.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c b/src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/gen_issue69.c
rename to src/plugins/e-acsl/tests/bts/oracle_ci/gen_issue69.c
diff --git a/src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/issue69.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/bts/oracle/issue69.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle_ci/issue69.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strcat.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcat.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strcmp.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcmp.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strcpy.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strcpy.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c b/src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/gen_strlen.c
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/gen_strlen.c
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strcat.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strcat.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strcmp.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strcmp.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strcpy.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strcpy.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle b/src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/oracle/strlen.res.oracle
rename to src/plugins/e-acsl/tests/builtin/oracle_ci/strlen.res.oracle
diff --git a/src/plugins/e-acsl/tests/builtin/test_config b/src/plugins/e-acsl/tests/builtin/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/builtin/test_config
rename to src/plugins/e-acsl/tests/builtin/test_config_ci
diff --git a/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_ci/functions_contiki.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
rename to src/plugins/e-acsl/tests/examples/oracle_ci/functions_contiki.res.oracle
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
rename to src/plugins/e-acsl/tests/examples/oracle_ci/gen_functions_contiki.c
diff --git a/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
rename to src/plugins/e-acsl/tests/examples/oracle_ci/gen_linear_search.c
diff --git a/src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle
rename to src/plugins/e-acsl/tests/examples/oracle_ci/linear_search.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/fprintf.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/gen_fprintf.c
rename to src/plugins/e-acsl/tests/format/oracle_ci/gen_fprintf.c
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/gen_printf.c
rename to src/plugins/e-acsl/tests/format/oracle_ci/gen_printf.c
diff --git a/src/plugins/e-acsl/tests/format/oracle/gen_printf2.c b/src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/gen_printf2.c
rename to src/plugins/e-acsl/tests/format/oracle_ci/gen_printf2.c
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.0.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.0.err.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.0.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.0.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.1.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.1.err.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.1.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.1.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.err.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.err.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.err.oracle
diff --git a/src/plugins/e-acsl/tests/format/oracle/printf.res.oracle b/src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/format/oracle/printf.res.oracle
rename to src/plugins/e-acsl/tests/format/oracle_ci/printf.res.oracle
diff --git a/src/plugins/e-acsl/tests/format/printf.c b/src/plugins/e-acsl/tests/format/printf.c
index 2bfcc362380d9ea2951b3e3e027d1134b3e0c367..79b0538a529afe29d2bad344be9a71e3755cc5b1 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
+/* run.config_ci
COMMENT: Check detection of format-string vulnerabilities via printf
DONTRUN:
*/
diff --git a/src/plugins/e-acsl/tests/format/test_config b/src/plugins/e-acsl/tests/format/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/format/test_config
rename to src/plugins/e-acsl/tests/format/test_config_ci
diff --git a/src/plugins/e-acsl/tests/full-mmodel/let-alias.c b/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
index e21140b029593287b96bc31795fdb841d7b44aa5..c1c5817fe5bc13885101a89fb083ffb8c4c1f204 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
+++ b/src/plugins/e-acsl/tests/full-mmodel/let-alias.c
@@ -6,6 +6,5 @@ int main(void) {
int t[4] = {1,2,3,4};
/*@ assert \let u = t + 1; *(u + 2) == 4; */ ;
/*@ assert (\let u = t + 1; *(u + 2)) == 4; */ ;
-
return 0;
}
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/addrOf.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf.c
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf2.c
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_let-alias.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/gen_let-alias.c
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_let-alias.c
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/let-alias.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/oracle/let-alias.res.oracle
rename to src/plugins/e-acsl/tests/full-mmodel/oracle_ci/let-alias.res.oracle
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config b/src/plugins/e-acsl/tests/full-mmodel/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/full-mmodel/test_config
rename to src/plugins/e-acsl/tests/full-mmodel/test_config_ci
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/arith.res.oracle
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/arith.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/functions.res.oracle
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/functions.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/gen_arith.c
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_arith.c
diff --git a/src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c b/src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/oracle/gen_functions.c
rename to src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c
diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config b/src/plugins/e-acsl/tests/gmp-only/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp-only/test_config
rename to src/plugins/e-acsl/tests/gmp-only/test_config_ci
diff --git a/src/plugins/e-acsl/tests/language_constructs/invariant.i b/src/plugins/e-acsl/tests/language_constructs/invariant.i
index 5cf1d2275293ee8c1a3736460c00f1499e261b53..76cbdb63c7169236217d0cb3a519aea09562eafd 100644
--- a/src/plugins/e-acsl/tests/language_constructs/invariant.i
+++ b/src/plugins/e-acsl/tests/language_constructs/invariant.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: invariant
STDOPT: +"-slevel 11"
*/
diff --git a/src/plugins/e-acsl/tests/language_constructs/loop.i b/src/plugins/e-acsl/tests/language_constructs/loop.i
index 329c01164f94caa6e98649ac0e2e313922fd48ed..4b0b3193ee1d889a17180daf26e085cd7a67cd0c 100644
--- a/src/plugins/e-acsl/tests/language_constructs/loop.i
+++ b/src/plugins/e-acsl/tests/language_constructs/loop.i
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: loop invariants
STDOPT: +"-slevel 160"
*/
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/false.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/false.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/false.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/false.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/function_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/function_contract.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/function_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_false.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_false.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_false.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_false.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_function_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_function_contract.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_function_contract.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_ghost.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_ghost.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_invariant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_invariant.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_invariant.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_labeled_stmt.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_labeled_stmt.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_labeled_stmt.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_lazy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_lazy.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_lazy.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_loop.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_loop.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_loop.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_loop.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_nested_code_annot.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_nested_code_annot.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_nested_code_annot.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_result.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_result.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_result.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_result.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_stmt_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_stmt_contract.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_stmt_contract.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_true.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_true.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_true.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_true.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_typedef.c
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/gen_typedef.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_typedef.c
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/ghost.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/ghost.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/ghost.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/invariant.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/invariant.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/invariant.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/labeled_stmt.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/labeled_stmt.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/labeled_stmt.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/lazy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/lazy.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/lazy.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/loop.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/loop.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/loop.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/nested_code_annot.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/nested_code_annot.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/nested_code_annot.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/result.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/result.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/result.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/result.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/stmt_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/stmt_contract.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/stmt_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/true.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/true.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/true.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/true.res.oracle
diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle_ci/typedef.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/language_constructs/oracle/typedef.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle_ci/typedef.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/ctype_macros.c b/src/plugins/e-acsl/tests/memory/ctype_macros.c
index 664996beecc4da2690be0ea8452617df66835f35..c5f033b1ddcd89bbd15fea0c9bc1a3226db11003 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
+/* run.config_ci
COMMENT: Tests for function-based implementation of ctype.h features
*/
diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c
index 2c7440cdb2f6384bcc9ed5735c6bf103b8f876c9..3f088213229d0076f623744b7ba65444efd8ce00 100644
--- a/src/plugins/e-acsl/tests/memory/local_init.c
+++ b/src/plugins/e-acsl/tests/memory/local_init.c
@@ -1,4 +1,4 @@
-/* run.config
+/* run.config_ci
COMMENT: test of a local initializer which contains an annotation
LOG: gen_@PTEST_NAME@.c
STDOPT: #"-lib-entry -eva -e-acsl-prepare -e-acsl-share ./share/e-acsl -then -no-lib-entry"
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
deleted file mode 100644
index 15d0281d5ae0b4dc878a687bc8131e19bc4aecae..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
+++ /dev/null
@@ -1,24 +0,0 @@
-/* Generated by Frama-C */
-int main(int argc, char **argv)
-{
- int __retres;
- __e_acsl_memory_init(& argc,& argv,8UL);
- __e_acsl_store_block((void *)(& argc),4UL);
- {
- int *p;
- __e_acsl_store_block((void *)(& p),8UL);
- switch (argc) {
- default: ;
- __e_acsl_full_init((void *)(& p));
- p = & argc;
- break;
- }
- __e_acsl_delete_block((void *)(& p));
- }
- __retres = 0;
- __e_acsl_delete_block((void *)(& argc));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/addrOf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/addrOf.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/alias.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/alias.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/base_addr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/base_addr.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/block_length.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/block_length.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/block_valid.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/block_valid.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/bypassed_var.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/bypassed_var.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/call.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/call.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/call.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/call.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/compound_initializers.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/compound_initializers.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ctype_macros.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.err.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.err.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.err.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/decl_in_switch.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/early_exit.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/early_exit.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/errno.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/errno.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/freeable.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/freeable.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_addrOf.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_alias.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_base_addr.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_length.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_block_valid.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_bypassed_var.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_call.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_call.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_call.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_compound_initializers.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_constructor.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ctype_macros.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/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_ci/gen_decl_in_switch.c
new file mode 100644
index 0000000000000000000000000000000000000000..44c5d1497e4120146834c9da6a048d63af4800c6
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_decl_in_switch.c
@@ -0,0 +1,146 @@
+/* Generated by Frama-C */
+typedef unsigned long size_t;
+struct __e_acsl_mpz_struct {
+ int _mp_alloc ;
+ int _mp_size ;
+ unsigned long *_mp_d ;
+};
+typedef struct __e_acsl_mpz_struct __e_acsl_mpz_struct;
+typedef __e_acsl_mpz_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpz_t)[1];
+struct __e_acsl_mpq_struct {
+ __e_acsl_mpz_struct _mp_num ;
+ __e_acsl_mpz_struct _mp_den ;
+};
+typedef struct __e_acsl_mpq_struct __e_acsl_mpq_struct;
+typedef __e_acsl_mpq_struct ( __attribute__((__FC_BUILTIN__)) __e_acsl_mpq_t)[1];
+typedef struct _IO_FILE FILE;
+/*@ ghost extern int __e_acsl_init; */
+
+extern size_t __e_acsl_heap_allocation_size;
+
+typedef unsigned short __uint16_t;
+typedef unsigned int __uint32_t;
+typedef unsigned long __uint64_t;
+typedef long __off_t;
+typedef long __off64_t;
+struct _IO_FILE;
+typedef void _IO_lock_t;
+struct _IO_marker {
+ struct _IO_marker *_next ;
+ struct _IO_FILE *_sbuf ;
+ int _pos ;
+};
+struct _IO_FILE {
+ int _flags ;
+ char *_IO_read_ptr ;
+ char *_IO_read_end ;
+ char *_IO_read_base ;
+ char *_IO_write_base ;
+ char *_IO_write_ptr ;
+ char *_IO_write_end ;
+ char *_IO_buf_base ;
+ char *_IO_buf_end ;
+ char *_IO_save_base ;
+ char *_IO_backup_base ;
+ char *_IO_save_end ;
+ struct _IO_marker *_markers ;
+ struct _IO_FILE *_chain ;
+ int _fileno ;
+ int _flags2 ;
+ __off_t _old_offset ;
+ unsigned short _cur_column ;
+ signed char _vtable_offset ;
+ char _shortbuf[1] ;
+ _IO_lock_t *_lock ;
+ __off64_t _offset ;
+ void *__pad1 ;
+ void *__pad2 ;
+ void *__pad3 ;
+ void *__pad4 ;
+ size_t __pad5 ;
+ int _mode ;
+ char _unused2[((unsigned long)15 * sizeof(int) - (unsigned long)4 * sizeof(void *)) - sizeof(size_t)] ;
+};
+/* compiler builtin:
+ unsigned int __builtin_bswap32(unsigned int); */
+/* compiler builtin:
+ unsigned long __builtin_bswap64(unsigned long); */
+__inline static unsigned int __bswap_32(unsigned int __bsx)
+{
+ unsigned int tmp;
+ tmp = __builtin_bswap32(__bsx);
+ return tmp;
+}
+
+__inline static __uint64_t __bswap_64(__uint64_t __bsx)
+{
+ __uint64_t tmp;
+ tmp = __builtin_bswap64(__bsx);
+ return tmp;
+}
+
+__inline static __uint16_t __uint16_identity(__uint16_t __x)
+{
+ return __x;
+}
+
+__inline static __uint32_t __uint32_identity(__uint32_t __x)
+{
+ return __x;
+}
+
+__inline static __uint64_t __uint64_identity(__uint64_t __x)
+{
+ return __x;
+}
+
+/*@
+predicate diffSize{L1, L2}(ℤ i) =
+ \at(__e_acsl_heap_allocation_size,L1) -
+ \at(__e_acsl_heap_allocation_size,L2) ≡ i;
+
+*/
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_init)(
+int *x_0, char ***x_1, unsigned long x_2);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_store_block)(
+void *x_0, unsigned long x_1);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_full_init)(
+void *x_0);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_delete_block)(
+void *x_0);
+
+extern __attribute__((__FC_BUILTIN__)) int ( /* missing proto */ __e_acsl_memory_clean)(
+void);
+
+int main(int argc, char **argv)
+{
+ int __retres;
+ __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_memory_init(& argc,& argv,8UL);
+ __e_acsl_store_block((void *)(& argc),4UL);
+ {
+ int *p;
+ __e_acsl_store_block((void *)(& p),8UL);
+ __e_acsl_store_block((void *)(& p),8UL);
+ switch (argc) {
+ default: ;
+ __e_acsl_full_init((void *)(& p));
+ __e_acsl_full_init((void *)(& p));
+ p = & argc;
+ break;
+ }
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& p));
+ }
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& argc));
+ __e_acsl_memory_clean();
+ __e_acsl_delete_block((void *)(& argc));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_early_exit.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_errno.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_freeable.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_goto.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_hidden_malloc.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_init.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_init.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_init_function.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_initialized.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_literal_string.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_init.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_var.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_mainargs.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_memalign.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_memsize.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_null.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_null.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_offset.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_offset.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_other_constants.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_ptr_init.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_ranges_in_builtins.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_sizeof.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_stdout.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_alias.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_valid_in_contract.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_vector.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
rename to src/plugins/e-acsl/tests/memory/oracle_ci/gen_vla.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/goto.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/goto.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/init.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/init_function.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/init_function.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/initialized.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/initialized.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/literal_string.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/literal_string.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/local_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_var.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/local_var.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/mainargs.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/memalign.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/memsize.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/null.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/null.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/null.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/null.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/offset.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/offset.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/other_constants.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/other_constants.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ptr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ptr.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ptr_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ptr_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/ranges_in_builtins.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/sizeof.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/sizeof.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/stdout.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/stdout.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/valid.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/valid.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/valid_alias.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/valid_alias.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/valid_in_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/valid_in_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/vector.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/vector.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle_ci/vla.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/result/.gitkeep b/src/plugins/e-acsl/tests/memory/result/.gitkeep
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/e-acsl/tests/special/builtin.i b/src/plugins/e-acsl/tests/special/builtin.i
index d69bd72b8d556abc685098033d511751ca58905a..5a4e114c5423bcdbdc2dc0f7a29cde752351a3b1 100644
--- a/src/plugins/e-acsl/tests/special/builtin.i
+++ b/src/plugins/e-acsl/tests/special/builtin.i
@@ -1,10 +1,7 @@
-/* run.config
- LOG: gen_builtin.c
- OPT: -e-acsl-builtins incr -machdep gcc_x86_64 -check -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c
- EXECNOW: ./scripts/testrun.sh builtin special "1" "--frama-c=@frama-c@ -F -e-acsl-builtins=incr"
- LOG: gen_builtin2.c
- OPT: -e-acsl-builtins incr -machdep gcc_x86_64 -check -e-acsl -e-acsl-gmp-only -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_builtin2.c
+/* run.config_ci
COMMENT: -e-acsl-builtins
+ LOG: gen_builtin.c
+ STDOPT: #"-e-acsl-builtins incr"
*/
int incr(int);
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 4eecfd5f7960aed8372b6d3301640fe9d7b50700..dbed3c949013f461bd4ff205c05f15c92334ac89 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-functions.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-functions.c
@@ -1,7 +1,7 @@
-/* run.config
+/* run.config_ci
COMMENT: test option -e-acsl-functions
LOG: gen_@PTEST_NAME@.c
- OPT: -machdep gcc_x86_64 -e-acsl-functions f -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -eva-verbose 0 -eva
+ STDOPT: #"-e-acsl-functions f"
*/
/*@ requires \initialized(p);
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 b0b1206198c9e96a170c51956d467a61419b8637..6fa83da775798aa4e4ae3c389c9d2a654bb018fc 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-instrument.c
@@ -1,7 +1,7 @@
-/* run.config
+/* run.config_ci
COMMENT: test option -e-acsl-instrument; cannot run Eva on this example
LOG: gen_@PTEST_NAME@.c
- OPT: -variadic-no-translation -machdep gcc_x86_64 -e-acsl-instrument="@@all,-uninstrument1,-uninstrument2" -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0
+ STDOPT: #"-e-acsl-instrument='@@all,-uninstrument1,-uninstrument2'"
*/
#include <stdarg.h>
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 f5582dbc7b9da34fb6f172488e3d826dbd1a3d96..0991da238f6abea0dc712b85916fbcadf6d1d2b1 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-valid.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-valid.c
@@ -1,10 +1,8 @@
-/* run.config
+/* run.config_ci
COMMENT: test option -e-acsl-no-valid
+ DONTRUN:
LOG: gen_@PTEST_NAME@.c
- OPT: -e-acsl-prepare -val -value-verbose 0 -machdep gcc_x86_64 -then -check -e-acsl-valid -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@.c -kernel-verbose 0 -value-verbose 0
- EXECNOW: ./scripts/testrun.sh @PTEST_NAME@ special "" "--frama-c=@frama-c@"
- LOG: gen_@PTEST_NAME@2.c
- OPT: -e-acsl-prepare -val -value-verbose 0 -machdep gcc_x86_64 -then -check -e-acsl-no-valid -e-acsl -then-last -load-script tests/print.cmxs -print -ocode tests/special/result/gen_@PTEST_NAME@2.c -kernel-verbose 0 -value-verbose 0
+ STDOPT: #"-e-acsl-prepare -e-acsl-share ./share/e-acsl -eva -eva-verbose 0 -then -e-acsl-no-valid"
*/
#include <stdlib.h>
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
deleted file mode 100644
index 274bdbe69e1a2b66be3ef24030464585c4d743f5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.0.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/special/builtin.i (no preprocessing)
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle b/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
deleted file mode 100644
index 274bdbe69e1a2b66be3ef24030464585c4d743f5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle/builtin.1.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/special/builtin.i (no preprocessing)
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle
deleted file mode 100644
index 5dff555c37e6255063e166ee303495b5adfdf7f8..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.0.res.oracle
+++ /dev/null
@@ -1,21 +0,0 @@
-[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:27: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `variant' is not yet supported. Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:31: Warning:
- E-ACSL construct `complete behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:31: Warning:
- E-ACSL construct `disjoint behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:13: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:22: 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/e-acsl-valid.1.res.oracle b/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle
deleted file mode 100644
index fb7c8f0d5a323a3ed53d286a0a09e0aca4d7e898..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-valid.1.res.oracle
+++ /dev/null
@@ -1,18 +0,0 @@
-[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:27: Warning:
- E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `variant' is not yet supported. Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `complete behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:28: Warning:
- E-ACSL construct `disjoint behaviors' is not yet supported.
- Ignoring annotation.
-[e-acsl] tests/special/e-acsl-valid.c:12: 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/gen_builtin2.c b/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
deleted file mode 100644
index 42faeb3e95b99c64878f1e870b179242bd68c200..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin2.c
+++ /dev/null
@@ -1,58 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-extern int __e_acsl_sound_verdict;
-
-int incr(int x);
-
-/*@ ensures \result ≡ incr(\old(i)); */
-int __gen_e_acsl_f(int i);
-
-int f(int i)
-{
- int j = i + 1;
- return j;
-}
-
-int incr(int x)
-{
- int __retres;
- __retres = x + 1;
- return __retres;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- int i = __gen_e_acsl_f(2);
- __retres = 0;
- return __retres;
-}
-
-/*@ ensures \result ≡ incr(\old(i)); */
-int __gen_e_acsl_f(int i)
-{
- int __gen_e_acsl_at;
- int __retres;
- __gen_e_acsl_at = i;
- __retres = f(i);
- {
- __e_acsl_mpz_t __gen_e_acsl_result;
- int __gen_e_acsl_incr_app;
- __e_acsl_mpz_t __gen_e_acsl_app;
- int __gen_e_acsl_eq;
- __gmpz_init_set_si(__gen_e_acsl_result,(long)__retres);
- __gen_e_acsl_incr_app = incr(__gen_e_acsl_at);
- __gmpz_init_set_si(__gen_e_acsl_app,(long)__gen_e_acsl_incr_app);
- __gen_e_acsl_eq = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_result),
- (__e_acsl_mpz_struct const *)(__gen_e_acsl_app));
- __e_acsl_assert(__gen_e_acsl_eq == 0,(char *)"Postcondition",(char *)"f",
- (char *)"\\result == incr(\\old(i))",12);
- __gmpz_clear(__gen_e_acsl_result);
- __gmpz_clear(__gen_e_acsl_app);
- return __retres;
- }
-}
-
-
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c b/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
deleted file mode 100644
index 1818b56a4a2c792554e61c5b9ec6d25e5e976750..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid2.c
+++ /dev/null
@@ -1,116 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-extern int __e_acsl_sound_verdict;
-
-/*@ requires \valid(y);
- requires *x ≥ 0;
- ensures *\old(x) ≡ \old(*x) + 1;
- assigns *x;
- assigns *x \from *x, x;
-
- behavior b1:
- assumes *x ≡ 1;
- ensures *\old(x) < 0;
- assigns \nothing;
-
- behavior b2:
- assumes *x ≡ 0;
- ensures *\old(x) ≡ 1;
-
- complete behaviors b2, b1;
- disjoint behaviors b1, b2;
- */
-void __gen_e_acsl_f(int *x, int *y);
-
-void f(int *x, int *y)
-{
- /*@ requires *x ≥ 0;
- ensures 2 ≥ 1;
- assigns *x; */
- {
- {
- int __gen_e_acsl_valid_read;
- __e_acsl_store_block((void *)(& y),(size_t)8);
- __e_acsl_store_block((void *)(& x),(size_t)8);
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)x,sizeof(int),
- (void *)x,(void *)(& x));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"RTE",(char *)"f",
- (char *)"mem_access: \\valid_read(x)",27);
- __e_acsl_assert(*x >= 0,(char *)"Precondition",(char *)"f",
- (char *)"*x >= 0",27);
- }
- __e_acsl_initialize((void *)x,sizeof(int));
- (*x) ++;
- __e_acsl_assert(1,(char *)"Postcondition",(char *)"f",(char *)"2 >= 1",
- 28);
- }
- {
- int i = 0;
- /*@ loop invariant 0 ≤ i ≤ 1;
- loop variant 2 - i; */
- while (i < 1) {
- /*@ assert 1 ≡ 1; */ ;
- /*@ assert \valid(y); */ ;
- i ++;
- }
- }
- __e_acsl_delete_block((void *)(& y));
- __e_acsl_delete_block((void *)(& x));
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- int x = 0;
- __e_acsl_store_block((void *)(& x),(size_t)4);
- __e_acsl_full_init((void *)(& x));
- int *y = malloc(sizeof(int));
- __e_acsl_store_block((void *)(& y),(size_t)8);
- __e_acsl_full_init((void *)(& y));
- __gen_e_acsl_f(& x,y);
- __retres = 0;
- __e_acsl_delete_block((void *)(& y));
- __e_acsl_delete_block((void *)(& x));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-/*@ requires \valid(y);
- requires *x ≥ 0;
- ensures *\old(x) ≡ \old(*x) + 1;
- assigns *x;
- assigns *x \from *x, x;
-
- behavior b1:
- assumes *x ≡ 1;
- ensures *\old(x) < 0;
- assigns \nothing;
-
- behavior b2:
- assumes *x ≡ 0;
- ensures *\old(x) ≡ 1;
-
- complete behaviors b2, b1;
- disjoint behaviors b1, b2;
- */
-void __gen_e_acsl_f(int *x, int *y)
-{
- {
- int __gen_e_acsl_valid;
- __e_acsl_store_block((void *)(& y),(size_t)8);
- __e_acsl_store_block((void *)(& x),(size_t)8);
- __gen_e_acsl_valid = __e_acsl_valid((void *)y,sizeof(int),(void *)y,
- (void *)(& y));
- __e_acsl_assert(__gen_e_acsl_valid,(char *)"Precondition",(char *)"f",
- (char *)"\\valid(y)",12);
- }
- f(x,y);
- __e_acsl_delete_block((void *)(& y));
- __e_acsl_delete_block((void *)(& x));
- return;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..f829e96e46483dba4975d357c55444c4b1fba88d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/builtin.res.oracle
@@ -0,0 +1,4 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/special/builtin.i:9: Warning:
+ function __gen_e_acsl_f: postcondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-functions.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/special/oracle/e-acsl-functions.res.oracle
rename to src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-functions.res.oracle
diff --git a/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
similarity index 81%
rename from src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
rename to src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
index 10d0bb2429c656141ec1da23f443f176827c2075..aabd7fab72b0dbd8439dbcae86b304ca634d327f 100644
--- a/src/plugins/e-acsl/tests/special/oracle/e-acsl-instrument.res.oracle
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-instrument.res.oracle
@@ -8,3 +8,7 @@
[e-acsl] tests/special/e-acsl-instrument.c:58: Warning:
ignoring effect of variadic function vol
[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/special/e-acsl-instrument.c:44: Warning:
+ accessing uninitialized left-value.
+ assert \initialized(&tmp);
+ (tmp from vararg)
diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8a102a933b40c01c21491f96630d750b81d7f818
--- /dev/null
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-valid.res.oracle
@@ -0,0 +1,40 @@
+[eva:alarm] tests/special/e-acsl-valid.c:36: Warning:
+ function f: precondition \valid(y) got status unknown.
+[e-acsl] beginning translation.
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:165: Warning:
+ Neither code nor specification for function aligned_alloc, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:181: Warning:
+ Neither code nor specification for function __e_acsl_mspaces_init, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:446: Warning:
+ Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:450: Warning:
+ Neither code nor specification for function __e_acsl_builtin_fprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:454: Warning:
+ Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:458: Warning:
+ Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:462: Warning:
+ Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:467: Warning:
+ Neither code nor specification for function __e_acsl_builtin_syslog, generating default assigns from the prototype
+[kernel:annot:missing-spec] FRAMAC_SHARE/e-acsl/e_acsl.h:488: Warning:
+ Neither code nor specification for function __e_acsl_floating_point_exception, generating default assigns from the prototype
+[kernel] Current source was: tests/special/e-acsl-valid.c:33
+ The full backtrace is:
+ Raised at file "src/libraries/project/project.ml", line 405, characters 59-66
+ Called from file "src/main.ml", line 155, characters 14-1023
+ Called from file "src/main.ml", line 121, characters 12-34
+ Called from file "src/libraries/project/state_builder.ml", line 565, characters 17-22
+ Called from file "src/main.ml", line 258, characters 11-56
+ Called from file "queue.ml", line 121, characters 6-15
+ Called from file "src/kernel_internals/runtime/boot.ml", line 36, characters 4-20
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 792, characters 2-9
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 807, characters 30-76
+ Called from file "src/kernel_services/cmdline_parameters/cmdline.ml", line 229, characters 4-8
+
+ Unexpected error (E_ACSL.Misc.Unregistered_library_function("__e_acsl_store_block")).
+ Please report as 'crash' at http://bts.frama-c.com/.
+ Your Frama-C version is 19.0+dev (Potassium).
+ Note that a version and a backtrace alone often do not contain enough
+ information to understand the bug. Guidelines for reporting bugs are at:
+ http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
similarity index 93%
rename from src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
index e2cb3cb48980c6fac8d50def5c7a7dee80900094..a1e4cd5f61765508c79776859fe56db818208453 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_builtin.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_builtin.c
@@ -42,7 +42,7 @@ int __gen_e_acsl_f(int i)
__gen_e_acsl_incr_app = incr(__gen_e_acsl_at);
__e_acsl_assert(__retres == __gen_e_acsl_incr_app,
(char *)"Postcondition",(char *)"f",
- (char *)"\\result == incr(\\old(i))",12);
+ (char *)"\\result == incr(\\old(i))",9);
return __retres;
}
}
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-functions.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-functions.c
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
similarity index 98%
rename from src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
index 36e9221c01c15ab537afe24a99c8076106d6a0ea..b3bd734d1350fa922b5e19ad1fafbe2be5f011e4 100644
--- a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-instrument.c
+++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-instrument.c
@@ -75,6 +75,7 @@ int vol(int n , ...)
int tmp;
__builtin_va_start(vl,n);
tmp = __builtin_va_arg (vl, int);
+ /*@ assert Eva: initialization: \initialized(&tmp); */
int r = tmp;
__builtin_va_end(vl);
__retres = 1;
diff --git a/src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/special/oracle/gen_e-acsl-valid.c
rename to src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-valid.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_addr-by-val.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_args.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_args.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_array.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_array.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_char.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_char.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_darray.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_darray.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_dpointer.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_dpointer.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_fptr.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fptr.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_lib.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_lib.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_fun_ptr.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_fun_ptr.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_getenv.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_getenv.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_global_init.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_labels.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_labels.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_lit_string.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_lit_string.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_local_init.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc-asan.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc-asan.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_malloc.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_malloc.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_memcpy.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_memcpy.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_scope.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_scope.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_struct.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_struct.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c b/src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/gen_t_while.c
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/gen_t_while.c
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_addr-by-val.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_addr-by-val.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_args.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_args.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_args.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_array.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_array.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_array.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_array.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_char.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_char.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_char.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_char.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_darray.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_darray.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_darray.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_darray.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_dpointer.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_dpointer.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_dpointer.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fptr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_fptr.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_fptr.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_lib.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_ptr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_fun_ptr.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_fun_ptr.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_getenv.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_global_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_global_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_global_init.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_global_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_labels.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_labels.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_labels.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_labels.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_lit_string.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_lit_string.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_lit_string.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_local_init.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_local_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_local_init.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_local_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc-asan.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc-asan.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_malloc.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_malloc.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_memcpy.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_scope.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_scope.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_struct.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_struct.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_struct.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_struct.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle_ci/t_while.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/oracle/t_while.res.oracle
rename to src/plugins/e-acsl/tests/temporal/oracle_ci/t_while.res.oracle
diff --git a/src/plugins/e-acsl/tests/temporal/test_config b/src/plugins/e-acsl/tests/temporal/test_config_ci
similarity index 100%
rename from src/plugins/e-acsl/tests/temporal/test_config
rename to src/plugins/e-acsl/tests/temporal/test_config_ci
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config_ci.in
similarity index 100%
rename from src/plugins/e-acsl/tests/test_config.in
rename to src/plugins/e-acsl/tests/test_config_ci.in
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
new file mode 100644
index 0000000000000000000000000000000000000000..7a8c9c6721a4081c286dd33a331f8f57ee4db8f5
--- /dev/null
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -0,0 +1,12 @@
+MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
+MACRO: GLOBAL -machdep gcc_x86_64 -variadic-no-translation -verbose 0
+MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1
+MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive
+MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
+LOG: gen_@PTEST_NAME@.c
+OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
+EXEC: e-acsl-gcc.sh -c -X -F="-verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run -O @DEST@.run && ./@DEST@.run.e-acsl
+FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
+COMMENT: This regex works around the tendency of Frama-C to transform
+COMMENT: absolute path into relative ones whenever the file is not too far
+COMMENT: away from cwd.