From a41e8b4b37a19c9a09ca925f134fb86eff8d9a1f Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 6 Mar 2015 14:15:17 +0100
Subject: [PATCH] [tests] new test directory 'bts'
---
src/plugins/e-acsl/.gitignore | 1 +
src/plugins/e-acsl/Makefile.in | 2 +-
.../tests/{e-acsl-runtime => bts}/bts1304.i | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1307.i | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1324.i | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1326.i | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1390.c | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1398.c | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1399.c | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1478.c | 4 +-
.../tests/{e-acsl-runtime => bts}/bts1700.i | 2 +-
.../tests/{e-acsl-runtime => bts}/bts1717.i | 4 +-
.../oracle/bts1304.0.err.oracle | 0
.../oracle/bts1304.0.res.oracle | 6 +--
.../oracle/bts1304.1.err.oracle | 0
.../oracle/bts1304.1.res.oracle | 6 +--
.../oracle/bts1304.err.oracle | 0
.../oracle/bts1304.res.oracle | 0
.../oracle/bts1307.0.err.oracle | 0
.../oracle/bts1307.0.res.oracle | 26 +++++------
.../oracle/bts1307.1.err.oracle | 0
.../oracle/bts1307.1.res.oracle | 44 +++++++++----------
.../oracle/bts1307.err.oracle | 0
.../oracle/bts1307.res.oracle | 0
.../oracle/bts1324.0.err.oracle | 0
.../oracle/bts1324.0.res.oracle | 12 ++---
.../oracle/bts1324.1.err.oracle | 0
.../oracle/bts1324.1.res.oracle | 16 +++----
.../oracle/bts1326.0.err.oracle | 0
.../oracle/bts1326.0.res.oracle | 6 +--
.../oracle/bts1326.1.err.oracle | 0
.../oracle/bts1326.1.res.oracle | 8 ++--
.../oracle/bts1390.0.err.oracle | 0
.../oracle/bts1390.0.res.oracle | 30 ++++++-------
.../oracle/bts1390.1.err.oracle | 0
.../oracle/bts1390.1.res.oracle | 24 +++++-----
.../oracle/bts1390.err.oracle | 0
.../oracle/bts1390.res.oracle | 0
.../oracle/bts1398.0.err.oracle | 0
.../oracle/bts1398.0.res.oracle | 2 +-
.../oracle/bts1398.1.err.oracle | 0
.../oracle/bts1398.1.res.oracle | 2 +-
.../oracle/bts1399.0.err.oracle | 0
.../oracle/bts1399.0.res.oracle | 14 +++---
.../oracle/bts1399.1.err.oracle | 0
.../oracle/bts1399.1.res.oracle | 10 ++---
.../oracle/bts1478.0.err.oracle | 0
.../oracle/bts1478.0.res.oracle | 14 +++---
.../oracle/bts1478.1.err.oracle | 0
.../oracle/bts1478.1.res.oracle | 14 +++---
.../oracle/bts1700.0.err.oracle | 0
.../oracle/bts1700.0.res.oracle | 14 +++---
.../oracle/bts1700.1.err.oracle | 0
.../oracle/bts1700.1.res.oracle | 14 +++---
.../oracle/bts1700.err.log | 0
.../oracle/bts1700.err.oracle | 0
.../oracle/bts1700.res.log | 0
.../oracle/bts1700.res.oracle | 0
.../oracle/bts1717.0.err.oracle | 0
.../oracle/bts1717.0.res.oracle | 4 +-
.../oracle/bts1717.1.err.oracle | 0
.../oracle/bts1717.1.res.oracle | 4 +-
.../oracle/gen_bts1304.c | 0
.../oracle/gen_bts13042.c | 0
.../oracle/gen_bts1307.c | 0
.../oracle/gen_bts13072.c | 0
.../oracle/gen_bts1324.c | 0
.../oracle/gen_bts13242.c | 0
.../oracle/gen_bts1326.c | 0
.../oracle/gen_bts13262.c | 0
.../oracle/gen_bts1390.c | 0
.../oracle/gen_bts13902.c | 0
.../oracle/gen_bts1398.c | 0
.../oracle/gen_bts13982.c | 0
.../oracle/gen_bts1399.c | 0
.../oracle/gen_bts13992.c | 0
.../oracle/gen_bts1478.c | 0
.../oracle/gen_bts14782.c | 0
.../oracle/gen_bts1700.c | 0
.../oracle/gen_bts1717.c | 0
.../oracle/gen_bts17172.c | 0
src/plugins/e-acsl/tests/bts/test_config | 2 +
82 files changed, 158 insertions(+), 155 deletions(-)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1304.i (62%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1307.i (72%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1324.i (61%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1326.i (62%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1390.c (73%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1398.c (58%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1399.c (71%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1478.c (54%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1700.i (59%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/bts1717.i (60%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1304.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1304.0.res.oracle (87%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1304.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1304.1.res.oracle (87%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1304.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1304.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1307.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1307.0.res.oracle (55%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1307.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1307.1.res.oracle (57%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1307.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1307.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1324.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1324.0.res.oracle (72%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1324.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1324.1.res.oracle (79%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1326.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1326.0.res.oracle (83%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1326.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1326.1.res.oracle (88%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1390.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1390.0.res.oracle (64%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1390.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1390.1.res.oracle (54%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1390.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1390.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1398.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1398.0.res.oracle (97%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1398.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1398.1.res.oracle (97%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1399.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1399.0.res.oracle (86%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1399.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1399.1.res.oracle (89%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1478.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1478.0.res.oracle (72%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1478.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1478.1.res.oracle (77%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.0.res.oracle (78%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.1.res.oracle (78%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.err.log (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.res.log (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1700.res.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1717.0.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1717.0.res.oracle (91%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1717.1.err.oracle (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/bts1717.1.res.oracle (91%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1304.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts13042.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1307.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts13072.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1324.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts13242.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1326.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts13262.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1390.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts13902.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1398.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts13982.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1399.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts13992.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1478.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts14782.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1700.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts1717.c (100%)
rename src/plugins/e-acsl/tests/{e-acsl-runtime => bts}/oracle/gen_bts17172.c (100%)
create mode 100644 src/plugins/e-acsl/tests/bts/test_config
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index b90605ae71a..0c1e1f185e9 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -74,6 +74,7 @@
/tests/e-acsl-reject/result/*.annot
/tests/e-acsl-reject/result/*_DEP
/tests/e-acsl-reject/result/*.log
+/tests/bts/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 514602db126..81ebb9c4d0a 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -112,7 +112,7 @@ $(PLUGIN_DIR)/local_config.ml: $(PLUGIN_DIR)/Makefile.in VERSION
ifeq (@MAY_RUN_TESTS@,yes)
-PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime
+PLUGIN_TESTS_DIRS:=e-acsl-reject e-acsl-runtime bts
E_ACSL_TESTS: $(PLUGIN_DIR)/tests/test_config
endif
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i b/src/plugins/e-acsl/tests/bts/bts1304.i
similarity index 62%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i
rename to src/plugins/e-acsl/tests/bts/bts1304.i
index b1266ba553f..ef6a48c1e39 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1304.i
+++ b/src/plugins/e-acsl/tests/bts/bts1304.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: argument of functions must be kept, so keep its parameter
- EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1304.c > /dev/null && ./gcc_test.sh bts1304
- EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13042.c > /dev/null && ./gcc_test.sh bts13042
+ EXECNOW: LOG gen_bts1304.c BIN gen_bts1304.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1304.c > /dev/null && ./gcc_test.sh bts1304
+ EXECNOW: LOG gen_bts13042.c BIN gen_bts13042.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1304.i -constfold -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13042.c > /dev/null && ./gcc_test.sh bts13042
*/
struct msgA { int type; int a[2]; };
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1307.i b/src/plugins/e-acsl/tests/bts/bts1307.i
similarity index 72%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1307.i
rename to src/plugins/e-acsl/tests/bts/bts1307.i
index b488258b842..12968768efd 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1307.i
+++ b/src/plugins/e-acsl/tests/bts/bts1307.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: spec with floats and reals
- EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1307.c > /dev/null && ./gcc_test.sh bts1307
- EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13072.c > /dev/null && ./gcc_test.sh bts13072
+ EXECNOW: LOG gen_bts1307.c BIN gen_bts1307.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1307.c > /dev/null && ./gcc_test.sh bts1307
+ EXECNOW: LOG gen_bts13072.c BIN gen_bts13072.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1307.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13072.c > /dev/null && ./gcc_test.sh bts13072
*/
/*@ requires \valid(Mtmax_in);
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i b/src/plugins/e-acsl/tests/bts/bts1324.i
similarity index 61%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
rename to src/plugins/e-acsl/tests/bts/bts1324.i
index 05456f90c43..1aa50971818 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1324.i
+++ b/src/plugins/e-acsl/tests/bts/bts1324.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: fixed bug with typing of universal quantification
- EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1324.c > /dev/null && ./gcc_test.sh bts1324
- EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13242.c > /dev/null && ./gcc_test.sh bts13242
+ EXECNOW: LOG gen_bts1324.c BIN gen_bts1324.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1324.c > /dev/null && ./gcc_test.sh bts1324
+ EXECNOW: LOG gen_bts13242.c BIN gen_bts13242.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1324.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13242.c > /dev/null && ./gcc_test.sh bts13242
*/
/*@ behavior yes:
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1326.i b/src/plugins/e-acsl/tests/bts/bts1326.i
similarity index 62%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1326.i
rename to src/plugins/e-acsl/tests/bts/bts1326.i
index 23de84e0965..63412190fca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1326.i
+++ b/src/plugins/e-acsl/tests/bts/bts1326.i
@@ -1,7 +1,7 @@
/* run.config
COMMENT: complex term left-values
- EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1326.c > /dev/null && ./gcc_test.sh bts1326
- EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13262.c > /dev/null && ./gcc_test.sh bts13262
+ EXECNOW: LOG gen_bts1326.c BIN gen_bts1326.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1326.c > /dev/null && ./gcc_test.sh bts1326
+ EXECNOW: LOG gen_bts13262.c BIN gen_bts13262.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1326.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13262.c > /dev/null && ./gcc_test.sh bts13262
*/
typedef int ArrayInt[5];
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c b/src/plugins/e-acsl/tests/bts/bts1390.c
similarity index 73%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c
rename to src/plugins/e-acsl/tests/bts/bts1390.c
index 2dbb1177ced..0d203d313af 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1390.c
+++ b/src/plugins/e-acsl/tests/bts/bts1390.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: bts #1390, issue with typing of quantified variables
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
- EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1390.c > /dev/null && ./gcc_test.sh bts1390
- EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13902.c > /dev/null && ./gcc_test.sh bts13902
+ EXECNOW: LOG gen_bts1390.c BIN gen_bts1390.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1390.c > /dev/null && ./gcc_test.sh bts1390
+ EXECNOW: LOG gen_bts13902.c BIN gen_bts13902.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1390.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13902.c > /dev/null && ./gcc_test.sh bts13902
*/
#include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c
similarity index 58%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1398.c
rename to src/plugins/e-acsl/tests/bts/bts1398.c
index 2fb52b52cc7..c1480633d82 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/bts1398.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: variadic function call
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
- EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1398.c > /dev/null && ./gcc_test.sh bts1398 > /dev/null
- EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13982.c > /dev/null && ./gcc_test.sh bts13982 > /dev/null
+ EXECNOW: LOG gen_bts1398.c BIN gen_bts1398.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1398.c > /dev/null && ./gcc_test.sh bts1398 > /dev/null
+ EXECNOW: LOG gen_bts13982.c BIN gen_bts13982.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1398.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13982.c > /dev/null && ./gcc_test.sh bts13982 > /dev/null
*/
#include "stdio.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1399.c b/src/plugins/e-acsl/tests/bts/bts1399.c
similarity index 71%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1399.c
rename to src/plugins/e-acsl/tests/bts/bts1399.c
index bccd7be8cae..c246d7acc6b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1399.c
+++ b/src/plugins/e-acsl/tests/bts/bts1399.c
@@ -1,8 +1,8 @@
/* run.config
COMMENT: complex fields and indexes + potential RTE in \initialized
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\"" +"-val-builtin __malloc:Frama_C_alloc_size -val-builtin __free:Frama_C_free"
- EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1399.c > /dev/null && ./gcc_test.sh bts1399
- EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts13992.c > /dev/null && ./gcc_test.sh bts13992
+ EXECNOW: LOG gen_bts1399.c BIN gen_bts1399.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1399.c > /dev/null && ./gcc_test.sh bts1399
+ EXECNOW: LOG gen_bts13992.c BIN gen_bts13992.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1399.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts13992.c > /dev/null && ./gcc_test.sh bts13992
*/
#include "stdlib.h"
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c b/src/plugins/e-acsl/tests/bts/bts1478.c
similarity index 54%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
rename to src/plugins/e-acsl/tests/bts/bts1478.c
index 5270202b6e3..a5fadbe4dd5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1478.c
+++ b/src/plugins/e-acsl/tests/bts/bts1478.c
@@ -1,7 +1,7 @@
/* run.config
COMMENT: bts #1478 about wrong detection of initializers in pre-analysis
- EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1478.c > /dev/null && ./gcc_test.sh bts1478
- EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
+ EXECNOW: LOG gen_bts1478.c BIN gen_bts1478.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1478.c > /dev/null && ./gcc_test.sh bts1478
+ EXECNOW: LOG gen_bts14782.c BIN gen_bts14782.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1478.c -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts14782.c > /dev/null && ./gcc_test.sh bts14782
*/
int global_i;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i b/src/plugins/e-acsl/tests/bts/bts1700.i
similarity index 59%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i
rename to src/plugins/e-acsl/tests/bts/bts1700.i
index bcf7a9e9f42..b76adfe91c3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1700.i
+++ b/src/plugins/e-acsl/tests/bts/bts1700.i
@@ -1,6 +1,6 @@
/* run.config
COMMENT: pointer to an empty struct
- EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
+ EXECNOW: LOG gen_bts1700.c BIN gen_bts1700.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/bts/bts1700.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1700.c > /dev/null && ./gcc_test.sh bts1700
*/
struct toto {};
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1717.i b/src/plugins/e-acsl/tests/bts/bts1717.i
similarity index 60%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/bts1717.i
rename to src/plugins/e-acsl/tests/bts/bts1717.i
index 5a7a6fed157..3164300f751 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/bts1717.i
+++ b/src/plugins/e-acsl/tests/bts/bts1717.i
@@ -1,8 +1,8 @@
/* run.config
COMMENT: bts #1717, issue with labels on memory-related statements
STDOPT: #"-cpp-extra-args=\"-I`@frama-c@ -print-share-path`/libc\""
- EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts1717.c > /dev/null && ./gcc_test.sh bts1717
- EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_bts17172.c > /dev/null && ./gcc_test.sh bts17172
+ EXECNOW: LOG gen_bts1717.c BIN gen_bts1717.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts1717.c > /dev/null && ./gcc_test.sh bts1717
+ EXECNOW: LOG gen_bts17172.c BIN gen_bts17172.out @frama-c@ -cpp-extra-args="-I`@frama-c@ -print-share-path`/libc" -e-acsl-share ./share/e-acsl ./tests/bts/bts1717.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/bts/result/gen_bts17172.c > /dev/null && ./gcc_test.sh bts17172
*/
int main(void) {
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
similarity index 87%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
index 85cef0bc324..343190f2f5b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1304.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1304.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -19,10 +19,10 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
+tests/bts/bts1304.i:23:[value] entering loop for the first time
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] Assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
similarity index 87%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
index 85cef0bc324..343190f2f5b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1304.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1304.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -19,10 +19,10 @@
__e_acsl_internal_heap ∈ [--..--]
__memory_size ∈ [--..--]
[value] using specification for function __store_block
-tests/e-acsl-runtime/bts1304.i:23:[value] entering loop for the first time
+tests/bts/bts1304.i:23:[value] entering loop for the first time
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1304.i:25:[value] Assertion got status unknown.
+tests/bts/bts1304.i:25:[value] Assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1304.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
similarity index 55%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
index e383dfcf607..838283a10e0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle
@@ -5,12 +5,12 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1307.i (no preprocessing)
-tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
+[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
+tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
@@ -24,21 +24,21 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid.
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
+tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] using specification for function __valid_read
[value] user error: type long double not implemented. Using double instead
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
+tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed.
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
similarity index 57%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
index 3105455c7cb..6edfe90528a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle
@@ -5,12 +5,12 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1307.i (no preprocessing)
-tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
+[kernel] Parsing tests/bts/bts1307.i (no preprocessing)
+tests/bts/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:13:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
+tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
@@ -24,18 +24,18 @@ tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: approximating a real number
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1307.i:7:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:8:[value] Function foo: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:9:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid.
+tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid.
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
+tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
@@ -43,7 +43,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_init
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Assertion 'E_ACSL' got status valid.
+tests/bts/bts1307.i:13:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function __gmpz_tdiv_q
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid.
@@ -54,16 +54,16 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: preconditio
[value] user error: type long double not implemented. Using double instead
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
-tests/e-acsl-runtime/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:21:[value] Function __e_acsl_bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:19:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:20:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:21:[value] Function bar: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:25:[value] Function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
+tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
+tests/bts/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
+tests/bts/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
+tests/bts/bts1307.i:21:[value] Function __e_acsl_bar: precondition got status valid.
+tests/bts/bts1307.i:19:[value] Function bar: precondition got status valid.
+tests/bts/bts1307.i:20:[value] Function bar: precondition got status valid.
+tests/bts/bts1307.i:21:[value] Function bar: precondition got status valid.
+tests/bts/bts1307.i:25:[value] Function bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
+tests/bts/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
similarity index 72%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
index f9945f408bf..22f38a1f1f1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1324.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1324.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -20,16 +20,16 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __initialize
-tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
+tests/bts/bts1324.i:8:[value] entering loop for the first time
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:15:[value] entering loop for the first time
+tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
+tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
similarity index 79%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
index a40f3257ff6..2632721388e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1324.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1324.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -33,7 +33,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition go
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1324.i:8:[value] entering loop for the first time
+tests/bts/bts1324.i:8:[value] entering loop for the first time
[value] using specification for function __gmpz_cmp
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
@@ -43,15 +43,15 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid.
[value] using specification for function __gmpz_get_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
-tests/e-acsl-runtime/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
-tests/e-acsl-runtime/bts1324.i:15:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2);
+tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2);
+tests/bts/bts1324.i:15:[value] entering loop for the first time
+tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
+tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
similarity index 83%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
index 9ccad28dc80..af73383a57f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1326.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1326.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -21,12 +21,12 @@
[value] using specification for function __store_block
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
similarity index 88%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
index 2914d3321ef..0e6763434b0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1326.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1326.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -21,7 +21,7 @@
[value] using specification for function __store_block
[value] using specification for function __initialize
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid.
[value] using specification for function __gmpz_init_set_si
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_init
@@ -33,7 +33,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition g
[value] using specification for function __gmpz_cmp
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
-tests/e-acsl-runtime/bts1326.i:11:[value] Assertion 'E_ACSL' got status valid.
+tests/bts/bts1326.i:11:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
@@ -42,7 +42,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: preconditio
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid.
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
+tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
similarity index 64%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
index 18ba293c49a..9a7fea6d52e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1390.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1390.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -30,7 +30,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition go
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid.
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
+tests/bts/bts1390.c:15:[value] entering loop for the first time
[value] using specification for function __gmpz_init_set_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
[value] using specification for function __gmpz_cmp
@@ -38,28 +38,28 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_get_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2);
+tests/bts/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2);
[value] using specification for function __gmpz_add
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid.
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
-tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
+tests/bts/bts1390.c:11:[value] entering loop for the first time
+tests/bts/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2);
+tests/bts/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:13:[value] entering loop for the first time
+tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] entering loop for the first time
[value] using specification for function __offset
-tests/e-acsl-runtime/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
+tests/bts/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2);
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
similarity index 54%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
index 1e234aff2a3..a58c7cfbb96 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1390.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1390.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -21,23 +21,23 @@
[value] using specification for function __store_block
[value] using specification for function __full_init
[value] using specification for function __literal_string
-tests/e-acsl-runtime/bts1390.c:15:[value] entering loop for the first time
+tests/bts/bts1390.c:15:[value] entering loop for the first time
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1390.c:11:[value] entering loop for the first time
-tests/e-acsl-runtime/bts1390.c:20:[value] entering loop for the first time
+tests/bts/bts1390.c:11:[value] entering loop for the first time
+tests/bts/bts1390.c:20:[value] entering loop for the first time
[value] using specification for function __delete_block
-tests/e-acsl-runtime/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:13:[value] entering loop for the first time
+tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] entering loop for the first time
[value] using specification for function __offset
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
-tests/e-acsl-runtime/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
-tests/e-acsl-runtime/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
-tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
similarity index 97%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
index ab093acca16..704fb9ba63c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1398.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1398.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
similarity index 97%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
index ab093acca16..704fb9ba63c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1398.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1398.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1398.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
similarity index 86%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
index dedc732a7e9..4ac929543e0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle
@@ -5,18 +5,18 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1399.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1399.c (with preprocessing)
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\free' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
@@ -39,7 +39,7 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
-tests/e-acsl-runtime/bts1399.c:24:[value] Assertion got status valid.
+tests/bts/bts1399.c:24:[value] Assertion got status valid.
[value] using specification for function __gmpz_init_set_ui
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
@@ -49,7 +49,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid.
[value] using specification for function __gmpz_init
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid.
-tests/e-acsl-runtime/bts1399.c:24:[value] Assertion 'E_ACSL' got status valid.
+tests/bts/bts1399.c:24:[value] Assertion 'E_ACSL' got status valid.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_q
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
similarity index 89%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
index ca35a04cc9c..ba312920833 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle
@@ -5,16 +5,16 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1399.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1399.c (with preprocessing)
[e-acsl] beginning translation.
FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\allocable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:187:[e-acsl] warning: E-ACSL construct `\freeable' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:171:[e-acsl] warning: E-ACSL construct `\fresh' is not yet supported. Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `complete behaviors' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
-tests/e-acsl-runtime/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
+tests/bts/bts1399.c:19:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
FRAMAC_SHARE/libc/stdlib.h:159:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
Ignoring annotation.
@@ -47,7 +47,7 @@ FRAMAC_SHARE/libc/stdlib.h:176:[e-acsl] warning: E-ACSL construct `\allocate' is
FRAMAC_SHARE/libc/stdlib.h:162:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
FRAMAC_SHARE/libc/stdlib.h:167:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.)
[value] using specification for function __initialize
-tests/e-acsl-runtime/bts1399.c:24:[value] Assertion got status valid.
+tests/bts/bts1399.c:24:[value] Assertion got status valid.
[value] using specification for function __valid_read
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
similarity index 72%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
index 819a1984571..6e5736c4a8f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1478.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1478.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -22,16 +22,16 @@
global_i_ptr ∈ {{ &global_i }}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __valid
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
-tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
similarity index 77%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
index 646927eca20..34b0792d501 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1478.c (with preprocessing)
+[kernel] Parsing tests/bts/bts1478.c (with preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -22,9 +22,9 @@
global_i_ptr ∈ {{ &global_i }}
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid.
[value] using specification for function __gmpz_init_set_si
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid.
[value] using specification for function __gmpz_cmp
@@ -36,9 +36,9 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] using specification for function __gmpz_clear
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:11:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status valid.
-tests/e-acsl-runtime/bts1478.c:13:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid.
+tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid.
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
similarity index 78%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
index 825a120a9f8..e7b7193eb2f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1700.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1700.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -20,16 +20,16 @@
__memory_size ∈ [--..--]
FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:150:[kernel] 0-sized location
[value] using specification for function __store_block
-tests/e-acsl-runtime/bts1700.i:9:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[value] Assertion got status unknown.
+tests/bts/bts1700.i:9:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[value] Assertion got status unknown.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1700.i:12:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[value] Assertion got status unknown.
+tests/bts/bts1700.i:12:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[value] Assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
similarity index 78%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
index 825a120a9f8..e7b7193eb2f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1700.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1700.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -20,16 +20,16 @@
__memory_size ∈ [--..--]
FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:150:[kernel] 0-sized location
[value] using specification for function __store_block
-tests/e-acsl-runtime/bts1700.i:9:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:10:[value] Assertion got status unknown.
+tests/bts/bts1700.i:9:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[kernel] 0-sized location
+tests/bts/bts1700.i:10:[value] Assertion got status unknown.
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown.
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1700.i:12:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[kernel] 0-sized location
-tests/e-acsl-runtime/bts1700.i:13:[value] Assertion got status unknown.
+tests/bts/bts1700.i:12:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[kernel] 0-sized location
+tests/bts/bts1700.i:13:[value] Assertion got status unknown.
[value] using specification for function __initialized
[value] using specification for function __delete_block
[value] using specification for function __e_acsl_memory_clean
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.log b/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.log
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.log
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.err.log
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.log b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.log
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.log
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.res.log
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1700.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1700.res.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.0.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
similarity index 91%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
index a0a3562292b..5aafc7dfe0f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.0.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1717.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1717.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -20,7 +20,7 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1717.i:13:[value] Assertion got status valid.
+tests/bts/bts1717.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.err.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.err.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.1.err.oracle
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
similarity index 91%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle
rename to src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
index a0a3562292b..5aafc7dfe0f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1717.1.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle
@@ -5,7 +5,7 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel_api.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_bittree.h (with preprocessing)
[kernel] Parsing FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h (with preprocessing)
-[kernel] Parsing tests/e-acsl-runtime/bts1717.i (no preprocessing)
+[kernel] Parsing tests/bts/bts1717.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
@@ -20,7 +20,7 @@
__memory_size ∈ [--..--]
[value] using specification for function __store_block
[value] using specification for function __full_init
-tests/e-acsl-runtime/bts1717.i:13:[value] Assertion got status valid.
+tests/bts/bts1717.i:13:[value] Assertion got status valid.
[value] using specification for function __initialized
[value] using specification for function __valid
[value] using specification for function e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1304.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1304.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13042.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13042.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1307.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1307.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13072.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13072.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1324.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1324.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13242.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13242.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1326.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1326.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13262.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13262.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1390.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1390.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13902.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13902.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1398.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1398.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13982.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13982.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1399.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1399.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts13992.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts13992.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1478.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1478.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts14782.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts14782.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1700.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1700.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts1717.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts1717.c
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c b/src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
similarity index 100%
rename from src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_bts17172.c
rename to src/plugins/e-acsl/tests/bts/oracle/gen_bts17172.c
diff --git a/src/plugins/e-acsl/tests/bts/test_config b/src/plugins/e-acsl/tests/bts/test_config
new file mode 100644
index 00000000000..bcf70a16ce7
--- /dev/null
+++ b/src/plugins/e-acsl/tests/bts/test_config
@@ -0,0 +1,2 @@
+OPT: -check -e-acsl -then-on e-acsl -val -no-val-show-progress -no-results
+OPT: -check -e-acsl -e-acsl-gmp-only -then-on e-acsl -val -no-val-show-progress -no-results
--
GitLab