diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index dbaf48cb5455bc853c48cbceed4de2b3110d5752..38cfd1166919ebd0d70f72f08f076048ed551d26 100644
--- a/src/plugins/e-acsl/.gitignore
+++ b/src/plugins/e-acsl/.gitignore
@@ -54,19 +54,7 @@
/tests/*.annot
/tests/*_DEP
/tests/test_config
-/tests/runtime/*.cm*
-/tests/runtime/result/*
-/tests/format/result/*
-/tests/builtin/result/*
-/tests/temporal/result/*
-/tests/special/result/*
-/tests/no-main/result/*
-/tests/full-mmodel/result/*
-/tests/full-mmodel-only/result/*
-/tests/segment-only/result/*
-/tests/bts/result/*
-/tests/gmp/result/*
-/tests/reject/result/*
+/tests/*/result/*
/tests/check/obj/*
.frama-c
tests/ptests_config
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 012d174c550fd2b04f91bcdc2614640759dbc007..3b549b22fe161e27847f04d0cd091c27de15644c 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -171,12 +171,11 @@ ifeq (@MAY_RUN_TESTS@,yes)
-include in_frama_ci
PLUGIN_TESTS_DIRS := \
- format \
- runtime \
bts \
- gmp \
+ arith \
+ memory \
full-mmodel \
- segment-only \
+ format \
temporal \
special
diff --git a/src/plugins/e-acsl/tests/gmp/README.md b/src/plugins/e-acsl/tests/arith/README.md
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/README.md
rename to src/plugins/e-acsl/tests/arith/README.md
diff --git a/src/plugins/e-acsl/tests/gmp/arith.i b/src/plugins/e-acsl/tests/arith/arith.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/arith.i
rename to src/plugins/e-acsl/tests/arith/arith.i
diff --git a/src/plugins/e-acsl/tests/gmp/array.i b/src/plugins/e-acsl/tests/arith/array.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/array.i
rename to src/plugins/e-acsl/tests/arith/array.i
diff --git a/src/plugins/e-acsl/tests/gmp/at.i b/src/plugins/e-acsl/tests/arith/at.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/at.i
rename to src/plugins/e-acsl/tests/arith/at.i
diff --git a/src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/at_on-purely-logic-variables.c
rename to src/plugins/e-acsl/tests/arith/at_on-purely-logic-variables.c
diff --git a/src/plugins/e-acsl/tests/gmp/cast.i b/src/plugins/e-acsl/tests/arith/cast.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/cast.i
rename to src/plugins/e-acsl/tests/arith/cast.i
diff --git a/src/plugins/e-acsl/tests/gmp/comparison.i b/src/plugins/e-acsl/tests/arith/comparison.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/comparison.i
rename to src/plugins/e-acsl/tests/arith/comparison.i
diff --git a/src/plugins/e-acsl/tests/gmp/functions.c b/src/plugins/e-acsl/tests/arith/functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/functions.c
rename to src/plugins/e-acsl/tests/arith/functions.c
diff --git a/src/plugins/e-acsl/tests/gmp/functions_contiki.c b/src/plugins/e-acsl/tests/arith/functions_contiki.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/functions_contiki.c
rename to src/plugins/e-acsl/tests/arith/functions_contiki.c
diff --git a/src/plugins/e-acsl/tests/gmp/functions_rec.c b/src/plugins/e-acsl/tests/arith/functions_rec.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/functions_rec.c
rename to src/plugins/e-acsl/tests/arith/functions_rec.c
diff --git a/src/plugins/e-acsl/tests/gmp/integer_constant.i b/src/plugins/e-acsl/tests/arith/integer_constant.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/integer_constant.i
rename to src/plugins/e-acsl/tests/arith/integer_constant.i
diff --git a/src/plugins/e-acsl/tests/gmp/let.c b/src/plugins/e-acsl/tests/arith/let.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/let.c
rename to src/plugins/e-acsl/tests/arith/let.c
diff --git a/src/plugins/e-acsl/tests/gmp/longlong.i b/src/plugins/e-acsl/tests/arith/longlong.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/longlong.i
rename to src/plugins/e-acsl/tests/arith/longlong.i
diff --git a/src/plugins/e-acsl/tests/gmp/not.i b/src/plugins/e-acsl/tests/arith/not.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/not.i
rename to src/plugins/e-acsl/tests/arith/not.i
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/arith.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/arith.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/arith.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/arith.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle
similarity index 62%
rename from src/plugins/e-acsl/tests/gmp/oracle/arith.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle
index 49ade870a7844d9509bb53480298afdbb248db8f..38a48a7633bc1bd9ce121d8e99f5a422b09d05fa 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/arith.res.oracle
@@ -1,12 +1,12 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/arith.i:18: Warning:
+[eva:alarm] tests/arith/arith.i:18: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:34: Warning:
+[eva:alarm] tests/arith/arith.i:34: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/arith.i:34: Warning:
+[eva:alarm] tests/arith/arith.i:34: Warning:
signed overflow. assert -2147483648 ≤ 1 + __gen_e_acsl__7;
-[eva:alarm] tests/gmp/arith.i:34: Warning:
+[eva:alarm] tests/arith/arith.i:34: Warning:
signed overflow. assert 1 + __gen_e_acsl__7 ≤ 2147483647;
-[eva:alarm] tests/gmp/arith.i:34: Warning:
+[eva:alarm] tests/arith/arith.i:34: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/array.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/array.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/array.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/array.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/array.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/array.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3e67d49ba6f489b956ea155d471c63c57a47de33
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/array.res.oracle
@@ -0,0 +1,8 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/array.i:13: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:13: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/array.i:14: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/array.i:14: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/at.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/at.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1b2e6b52d1efc3ffa1b839a0d3fde9961a0799af
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
@@ -0,0 +1,9 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/at.i:12: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/at.i:14: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/at.i:48: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/at.i:49: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/at.i:50: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/at.i:26: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/at.i:28: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
similarity index 53%
rename from src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
index 6f8dd058c2e23fd0660a2eb821892b29c5bb18d9..41e3ddedf6b9a2429d3dd3af4bf79b709853a896 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/at_on-purely-logic-variables.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/at_on-purely-logic-variables.res.oracle
@@ -1,87 +1,87 @@
[e-acsl] beginning translation.
-[e-acsl] tests/gmp/at_on-purely-logic-variables.c:64: Warning:
+[e-acsl] tests/arith/at_on-purely-logic-variables.c:64: Warning:
E-ACSL construct
`\at on purely logic variables that needs to allocate too much memory (bigger than int_max bytes)'
is not yet supported.
Ignoring annotation.
-[e-acsl] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
+[e-acsl] tests/arith/at_on-purely-logic-variables.c:65: Warning:
E-ACSL construct `\at with logic variable linked to C variable'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:28: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:28: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + (__gen_e_acsl_j - 2));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:29: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:29: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:31: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:31: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:33: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:33: Warning:
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_3 +
((__gen_e_acsl_u - 9) * 11 + ((__gen_e_acsl_v - -5) - 1)));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:34: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:34: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:37: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:37: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_5 + ((__gen_e_acsl_k_3 - -9) - 1));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:41: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:41: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:43: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:43: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:44: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:44: Warning:
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_6 +
((__gen_e_acsl_u_3 - 9) * 32 + ((__gen_e_acsl_v_3 - -5) - 1)));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:45: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:45: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + ((__gen_e_acsl_n - 1) - 1));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at_2 + ((__gen_e_acsl_n - 1) - 1));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:7: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:7: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:6: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:6: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:8: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:8: Warning:
function __gen_e_acsl_f: postcondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
accessing uninitialized left-value.
assert \initialized(__gen_e_acsl_at + (__gen_e_acsl_w - 3));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:16: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:54: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:54: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:56: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:56: Warning:
accessing uninitialized left-value.
assert
\initialized(__gen_e_acsl_at_7 +
((__gen_e_acsl_u_5 - 10) * 300 +
(((__gen_e_acsl_v_5 - -10) - 1) * 100 +
((__gen_e_acsl_w - 100) - 1))));
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:63: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:63: Warning:
assertion got status unknown.
-[eva:alarm] tests/gmp/at_on-purely-logic-variables.c:65: Warning:
+[eva:alarm] tests/arith/at_on-purely-logic-variables.c:65: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/cast.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/cast.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/cast.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/cast.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
similarity index 78%
rename from src/plugins/e-acsl/tests/gmp/oracle/cast.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
index 91fde30486f7d9ecc718e9982b70a1434b27f74d..e4c1a84ed167fe3590dfcee976dc7c3902327fa7 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/cast.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
-[e-acsl] tests/gmp/cast.i:23: Warning:
+[e-acsl] tests/arith/cast.i:23: Warning:
E-ACSL construct `R to Int' is not yet supported. Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/comparison.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/comparison.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/comparison.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/comparison.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/comparison.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/comparison.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
similarity index 59%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
index 0851deb0f638262317b79a3190c0f20c0b37761d..52987f8cb85873505e7b239e37b417394cf058af 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions.res.oracle
@@ -1,14 +1,14 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/functions.c:44: Warning:
+[eva:alarm] tests/arith/functions.c:44: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:47: Warning:
+[eva:alarm] tests/arith/functions.c:47: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:48: Warning:
+[eva:alarm] tests/arith/functions.c:48: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:49: Warning:
+[eva:alarm] tests/arith/functions.c:49: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions.c:68: Warning:
+[eva:alarm] tests/arith/functions.c:68: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/gmp/functions.c:68: Warning:
+[eva:alarm] tests/arith/functions.c:68: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions_contiki.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions_contiki.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.res.oracle
similarity index 64%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions_contiki.res.oracle
index 57f78f5cdc08934b47a367198890e64a8a3455a6..e0a5361d26819c95c0cdb8107a6d169ec948d5ef 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions_contiki.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
-[e-acsl] tests/gmp/functions_contiki.c:27: Warning:
+[e-acsl] tests/arith/functions_contiki.c:27: Warning:
E-ACSL construct `logic functions with labels' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/functions_contiki.c:27: Warning:
+[eva:alarm] tests/arith/functions_contiki.c:27: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions_rec.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions_rec.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions_rec.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions_rec.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
similarity index 61%
rename from src/plugins/e-acsl/tests/gmp/oracle/functions_rec.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
index d6226e87d23134d7df3ce0d9e01f2c14905c7c76..139e052e16d866ef3bf085bde30123bfb2676f25 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/functions_rec.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/functions_rec.res.oracle
@@ -1,66 +1,69 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/functions_rec.c:26: Warning: assertion got status unknown.
-[eva] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:26: Warning:
+ assertion got status unknown.
+[eva] tests/arith/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/gmp/functions_rec.c:10: Warning:
+[eva] tests/arith/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva] tests/gmp/functions_rec.c:10: Warning:
+[eva] tests/arith/functions_rec.c:10: Warning:
recursive call during value analysis
- of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/gmp/functions_rec.c:10 <-
- __gen_e_acsl_f2 :: tests/gmp/functions_rec.c:26 <-
+ of __gen_e_acsl_f2_2 (__gen_e_acsl_f2_2 <- __gen_e_acsl_f2_2 :: tests/arith/functions_rec.c:10 <-
+ __gen_e_acsl_f2 :: tests/arith/functions_rec.c:26 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
division by zero. assert __gen_e_acsl_f2_8 ≢ 0;
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
signed overflow.
assert -2147483648 ≤ __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6;
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
signed overflow. assert __gen_e_acsl_f2_4 * __gen_e_acsl_f2_6 ≤ 2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
signed overflow.
assert
(int)(__gen_e_acsl_f2_4 * __gen_e_acsl_f2_6) / __gen_e_acsl_f2_8 ≤
2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
division by zero. assert __gen_e_acsl_f2_13 ≢ 0;
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
signed overflow.
assert -2147483648 ≤ __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11;
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
signed overflow.
assert __gen_e_acsl_f2_9 * __gen_e_acsl_f2_11 ≤ 2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:10: Warning:
+[eva:alarm] tests/arith/functions_rec.c:10: Warning:
signed overflow.
assert
(int)(__gen_e_acsl_f2_9 * __gen_e_acsl_f2_11) / __gen_e_acsl_f2_13 ≤
2147483647;
-[eva:alarm] tests/gmp/functions_rec.c:26: Warning:
+[eva:alarm] tests/arith/functions_rec.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/functions_rec.c:28: Warning: assertion got status unknown.
-[eva] tests/gmp/functions_rec.c:14: Warning:
+[eva:alarm] tests/arith/functions_rec.c:28: Warning:
+ assertion got status unknown.
+[eva] tests/arith/functions_rec.c:14: Warning:
recursive call during value analysis
- of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/gmp/functions_rec.c:14 <-
- __gen_e_acsl_f3 :: tests/gmp/functions_rec.c:28 <-
+ of __gen_e_acsl_f3_2 (__gen_e_acsl_f3_2 <- __gen_e_acsl_f3_2 :: tests/arith/functions_rec.c:14 <-
+ __gen_e_acsl_f3 :: tests/arith/functions_rec.c:28 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:30: Warning: assertion got status unknown.
-[eva] tests/gmp/functions_rec.c:17: Warning:
+[eva:alarm] tests/arith/functions_rec.c:30: Warning:
+ assertion got status unknown.
+[eva] tests/arith/functions_rec.c:17: Warning:
recursive call during value analysis
- of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/gmp/functions_rec.c:17 <-
- __gen_e_acsl_f4 :: tests/gmp/functions_rec.c:30 <-
+ of __gen_e_acsl_f4_2 (__gen_e_acsl_f4_2 <- __gen_e_acsl_f4_2 :: tests/arith/functions_rec.c:17 <-
+ __gen_e_acsl_f4 :: tests/arith/functions_rec.c:30 <-
main).
Assuming the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/functions_rec.c:30: Warning:
+[eva:alarm] tests/arith/functions_rec.c:30: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c b/src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_arith.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_arith.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_arith2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_arith2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_arith2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_array.c b/src/plugins/e-acsl/tests/arith/oracle/gen_array.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_array.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_array.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_array2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_array2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_array2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_at.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_at.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_at2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_at2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_at_on-purely-logic-variables2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_at_on-purely-logic-variables2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c b/src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_cast.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_cast.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_cast2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_cast2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_cast2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_comparison.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_comparison.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_comparison2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_comparison2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_comparison2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_functions.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_functions2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_functions_contiki2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_functions_rec2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_functions_rec2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_integer_constant2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_integer_constant2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let.c b/src/plugins/e-acsl/tests/arith/oracle/gen_let.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_let.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_let.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_let2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_let2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_let2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_longlong.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_longlong.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_longlong2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_longlong2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_longlong2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not.c b/src/plugins/e-acsl/tests/arith/oracle/gen_not.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_not.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_not.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_not2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_not2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_not2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_quantif.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_quantif.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_quantif2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_quantif2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_quantif2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c b/src/plugins/e-acsl/tests/arith/oracle/gen_reals.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_reals.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_reals.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_reals2.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/gen_reals2.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_reals2.c
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/integer_constant.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/integer_constant.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/integer_constant.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/integer_constant.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle
similarity index 71%
rename from src/plugins/e-acsl/tests/gmp/oracle/integer_constant.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle
index 5a492da3fd4128e9f0d2742af80b905237760728..6b57e2f2567a73c9c0cecf048b1085a58562d64c 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/integer_constant.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/integer_constant.i:11: Warning:
+[eva:alarm] tests/arith/integer_constant.i:11: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/let.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/let.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/let.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/let.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/let.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/let.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ca9d6da56ba3a181b86474b0bc1a30698b36e61c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
@@ -0,0 +1,19 @@
+[e-acsl] beginning translation.
+[e-acsl] tests/arith/let.c:30: Warning:
+ E-ACSL construct `let-binding on array or pointer' is not yet supported.
+ Ignoring annotation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/let.c:7: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:9: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:12: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:17: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:21: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:21: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/let.c:24: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:27: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:30: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:35: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/let.c:39: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/longlong.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/longlong.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/longlong.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/longlong.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle
similarity index 55%
rename from src/plugins/e-acsl/tests/gmp/oracle/longlong.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle
index 2360617faf6ad096890375cf3c02bdb7ed973496..124461612b970a0ba6842a2ef51aec04edd861ba 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/longlong.res.oracle
@@ -1,14 +1,14 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva] tests/gmp/longlong.i:9: Warning:
+[eva] tests/arith/longlong.i:9: Warning:
recursive call during value analysis
- of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
+ of my_pow (my_pow <- my_pow :: tests/arith/longlong.i:16 <- main). Assuming
the call has no effect. The analysis will be unsound.
-[eva:alarm] tests/gmp/longlong.i:10: Warning:
+[eva:alarm] tests/arith/longlong.i:10: Warning:
signed overflow. assert -2147483648 ≤ tmp * tmp;
-[eva:alarm] tests/gmp/longlong.i:10: Warning:
+[eva:alarm] tests/arith/longlong.i:10: Warning:
signed overflow. assert tmp * tmp ≤ 2147483647;
-[eva:alarm] tests/gmp/longlong.i:17: Warning:
+[eva:alarm] tests/arith/longlong.i:17: Warning:
function __gmpz_import: precondition got status unknown.
-[eva:alarm] tests/gmp/longlong.i:17: Warning:
+[eva:alarm] tests/arith/longlong.i:17: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/not.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/not.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/not.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/not.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/not.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/not.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/not.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/quantif.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/quantif.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..e34fffe72687422b0029223b19570a7b4c0d0f3c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
@@ -0,0 +1,25 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/quantif.i:9: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:10: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:11: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:15: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:15: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/quantif.i:20: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:24: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:24: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/quantif.i:30: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:30: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/quantif.i:31: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/quantif.i:32: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:32: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/quantif.i:33: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:33: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/quantif.i:37: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/quantif.i:40: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/reals.0.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/reals.0.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/reals.0.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/reals.1.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/oracle/reals.1.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/reals.1.res.oracle
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/reals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/reals.res.oracle
similarity index 52%
rename from src/plugins/e-acsl/tests/gmp/oracle/reals.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/reals.res.oracle
index b556402d9c02078689197c3880f6c352e3870b42..975ef40a79f060f8b00a6a94ed14e7779a22c44f 100644
--- a/src/plugins/e-acsl/tests/gmp/oracle/reals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/reals.res.oracle
@@ -1,48 +1,48 @@
-[kernel:parser:decimal-float] tests/gmp/reals.c:22: Warning:
+[kernel:parser:decimal-float] tests/arith/reals.c:22: Warning:
Floating-point constant 0.2f is not represented exactly. Will use 0x1.99999a0000000p-3.
(warn-once: no further messages from category 'parser:decimal-float' will be emitted)
[e-acsl] beginning translation.
[e-acsl] Warning: R to float: double rounding might cause unsoundness
-[e-acsl] tests/gmp/reals.c:19: Warning:
+[e-acsl] tests/arith/reals.c:19: Warning:
E-ACSL construct `predicate with no definition nor reads clause'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/reals.c:15: Warning:
+[eva:alarm] tests/arith/reals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:16: Warning:
+[eva:alarm] tests/arith/reals.c:16: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/reals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:18: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:18: Warning:
+[eva:alarm] tests/arith/reals.c:18: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/reals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
+[eva:alarm] tests/arith/reals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:19: Warning:
+[eva:alarm] tests/arith/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] tests/gmp/reals.c:19: Warning:
+[eva:alarm] tests/arith/reals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/gmp/reals.c:19: Warning:
+[eva:alarm] tests/arith/reals.c:19: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
-[eva:alarm] tests/gmp/reals.c:19: Warning:
+[eva:alarm] tests/arith/reals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:20: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:20: Warning:
+[eva:alarm] tests/arith/reals.c:20: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/reals.c:20: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/gmp/reals.c:20: Warning:
+[eva:alarm] tests/arith/reals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:21: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:21: Warning:
+[eva:alarm] tests/arith/reals.c:21: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/reals.c:21: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:25: Warning:
+[eva:alarm] tests/arith/reals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:26: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:26: Warning:
+[eva:alarm] tests/arith/reals.c:26: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/reals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:6: Warning:
+[eva:alarm] tests/arith/reals.c:6: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:6: Warning:
+[eva:alarm] tests/arith/reals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:32: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/reals.c:32: Warning:
+[eva:alarm] tests/arith/reals.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/reals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/quantif.i b/src/plugins/e-acsl/tests/arith/quantif.i
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/quantif.i
rename to src/plugins/e-acsl/tests/arith/quantif.i
diff --git a/src/plugins/e-acsl/tests/gmp/reals.c b/src/plugins/e-acsl/tests/arith/reals.c
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/reals.c
rename to src/plugins/e-acsl/tests/arith/reals.c
diff --git a/src/plugins/e-acsl/tests/gmp/reals1.c.notest b/src/plugins/e-acsl/tests/arith/reals1.c.notest
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/reals1.c.notest
rename to src/plugins/e-acsl/tests/arith/reals1.c.notest
diff --git a/src/plugins/e-acsl/tests/gmp/result/.gitkeep b/src/plugins/e-acsl/tests/arith/result/.gitkeep
similarity index 100%
rename from src/plugins/e-acsl/tests/gmp/result/.gitkeep
rename to src/plugins/e-acsl/tests/arith/result/.gitkeep
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.res.oracle
deleted file mode 100644
index b53db5cdd350ef838d5b42096d6424237952ae6c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/gmp/oracle/array.res.oracle
+++ /dev/null
@@ -1,8 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/array.i:13: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/array.i:13: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/array.i:14: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/array.i:14: Warning:
- function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.res.oracle
deleted file mode 100644
index b3ea1b65fec9a4ea89a4c44746757e24a9b8e238..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/gmp/oracle/at.res.oracle
+++ /dev/null
@@ -1,9 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/at.i:12: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:14: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:48: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:49: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:50: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:26: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/at.i:28: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/let.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/let.res.oracle
deleted file mode 100644
index f8c1c0d9938107d8020321184e68538a1af53c32..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/gmp/oracle/let.res.oracle
+++ /dev/null
@@ -1,19 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] tests/gmp/let.c:30: Warning:
- E-ACSL construct `let-binding on array or pointer' is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/let.c:7: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:9: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:12: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:14: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:17: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:21: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:21: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/let.c:24: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:27: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:30: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:32: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:35: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/let.c:39: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.res.oracle
deleted file mode 100644
index 6636cdc4391eb2f2ea94e51302a5ac438a55a6fd..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/gmp/quantif.i:9: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:10: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:11: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:15: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:15: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:20: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:24: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:24: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:30: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:30: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:31: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:32: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:32: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:33: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:33: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/quantif.i:37: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/quantif.i:40: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/addrOf.i b/src/plugins/e-acsl/tests/memory/addrOf.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/addrOf.i
rename to src/plugins/e-acsl/tests/memory/addrOf.i
diff --git a/src/plugins/e-acsl/tests/runtime/alias.i b/src/plugins/e-acsl/tests/memory/alias.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/alias.i
rename to src/plugins/e-acsl/tests/memory/alias.i
diff --git a/src/plugins/e-acsl/tests/runtime/base_addr.c b/src/plugins/e-acsl/tests/memory/base_addr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/base_addr.c
rename to src/plugins/e-acsl/tests/memory/base_addr.c
diff --git a/src/plugins/e-acsl/tests/runtime/block_length.c b/src/plugins/e-acsl/tests/memory/block_length.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/block_length.c
rename to src/plugins/e-acsl/tests/memory/block_length.c
diff --git a/src/plugins/e-acsl/tests/runtime/block_valid.c b/src/plugins/e-acsl/tests/memory/block_valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/block_valid.c
rename to src/plugins/e-acsl/tests/memory/block_valid.c
diff --git a/src/plugins/e-acsl/tests/runtime/bypassed_var.c b/src/plugins/e-acsl/tests/memory/bypassed_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/bypassed_var.c
rename to src/plugins/e-acsl/tests/memory/bypassed_var.c
diff --git a/src/plugins/e-acsl/tests/runtime/call.c b/src/plugins/e-acsl/tests/memory/call.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/call.c
rename to src/plugins/e-acsl/tests/memory/call.c
diff --git a/src/plugins/e-acsl/tests/runtime/compound_initializers.c b/src/plugins/e-acsl/tests/memory/compound_initializers.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/compound_initializers.c
rename to src/plugins/e-acsl/tests/memory/compound_initializers.c
diff --git a/src/plugins/e-acsl/tests/runtime/constructor.c b/src/plugins/e-acsl/tests/memory/constructor.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/constructor.c
rename to src/plugins/e-acsl/tests/memory/constructor.c
diff --git a/src/plugins/e-acsl/tests/runtime/ctype_macros.c b/src/plugins/e-acsl/tests/memory/ctype_macros.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/ctype_macros.c
rename to src/plugins/e-acsl/tests/memory/ctype_macros.c
diff --git a/src/plugins/e-acsl/tests/runtime/decl_in_switch.c b/src/plugins/e-acsl/tests/memory/decl_in_switch.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/decl_in_switch.c
rename to src/plugins/e-acsl/tests/memory/decl_in_switch.c
diff --git a/src/plugins/e-acsl/tests/runtime/early_exit.c b/src/plugins/e-acsl/tests/memory/early_exit.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/early_exit.c
rename to src/plugins/e-acsl/tests/memory/early_exit.c
diff --git a/src/plugins/e-acsl/tests/runtime/errno.c b/src/plugins/e-acsl/tests/memory/errno.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/errno.c
rename to src/plugins/e-acsl/tests/memory/errno.c
diff --git a/src/plugins/e-acsl/tests/runtime/false.i b/src/plugins/e-acsl/tests/memory/false.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/false.i
rename to src/plugins/e-acsl/tests/memory/false.i
diff --git a/src/plugins/e-acsl/tests/runtime/freeable.c b/src/plugins/e-acsl/tests/memory/freeable.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/freeable.c
rename to src/plugins/e-acsl/tests/memory/freeable.c
diff --git a/src/plugins/e-acsl/tests/runtime/function_contract.i b/src/plugins/e-acsl/tests/memory/function_contract.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/function_contract.i
rename to src/plugins/e-acsl/tests/memory/function_contract.i
diff --git a/src/plugins/e-acsl/tests/runtime/ghost.i b/src/plugins/e-acsl/tests/memory/ghost.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/ghost.i
rename to src/plugins/e-acsl/tests/memory/ghost.i
diff --git a/src/plugins/e-acsl/tests/runtime/goto.c b/src/plugins/e-acsl/tests/memory/goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/goto.c
rename to src/plugins/e-acsl/tests/memory/goto.c
diff --git a/src/plugins/e-acsl/tests/runtime/hidden_malloc.c b/src/plugins/e-acsl/tests/memory/hidden_malloc.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/hidden_malloc.c
rename to src/plugins/e-acsl/tests/memory/hidden_malloc.c
diff --git a/src/plugins/e-acsl/tests/runtime/init.c b/src/plugins/e-acsl/tests/memory/init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/init.c
rename to src/plugins/e-acsl/tests/memory/init.c
diff --git a/src/plugins/e-acsl/tests/runtime/init_function.c b/src/plugins/e-acsl/tests/memory/init_function.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/init_function.c
rename to src/plugins/e-acsl/tests/memory/init_function.c
diff --git a/src/plugins/e-acsl/tests/runtime/initialized.c b/src/plugins/e-acsl/tests/memory/initialized.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/initialized.c
rename to src/plugins/e-acsl/tests/memory/initialized.c
diff --git a/src/plugins/e-acsl/tests/runtime/invariant.i b/src/plugins/e-acsl/tests/memory/invariant.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/invariant.i
rename to src/plugins/e-acsl/tests/memory/invariant.i
diff --git a/src/plugins/e-acsl/tests/runtime/labeled_stmt.i b/src/plugins/e-acsl/tests/memory/labeled_stmt.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/labeled_stmt.i
rename to src/plugins/e-acsl/tests/memory/labeled_stmt.i
diff --git a/src/plugins/e-acsl/tests/runtime/lazy.i b/src/plugins/e-acsl/tests/memory/lazy.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/lazy.i
rename to src/plugins/e-acsl/tests/memory/lazy.i
diff --git a/src/plugins/e-acsl/tests/runtime/linear_search.i b/src/plugins/e-acsl/tests/memory/linear_search.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/linear_search.i
rename to src/plugins/e-acsl/tests/memory/linear_search.i
diff --git a/src/plugins/e-acsl/tests/runtime/literal_string.i b/src/plugins/e-acsl/tests/memory/literal_string.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/literal_string.i
rename to src/plugins/e-acsl/tests/memory/literal_string.i
diff --git a/src/plugins/e-acsl/tests/runtime/local_goto.c b/src/plugins/e-acsl/tests/memory/local_goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/local_goto.c
rename to src/plugins/e-acsl/tests/memory/local_goto.c
diff --git a/src/plugins/e-acsl/tests/memory/local_init.c b/src/plugins/e-acsl/tests/memory/local_init.c
new file mode 100644
index 0000000000000000000000000000000000000000..417add7d562873f47e823d8729def4c512f983fe
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/local_init.c
@@ -0,0 +1,18 @@
+/* run.config
+ COMMENT: test of a local initializer which contains an annotation
+ LOG: gen_@PTEST_NAME@.c
+ STDOPT: #"-eva -e-acsl-prepare -e-acsl-share ./share/e-acsl -lib-entry -then"
+*/
+
+int X = 0;
+int *p = &X;
+
+int f(void) {
+ int x = *p; // Eva's alarm in -lib-entry on this local initializer
+ return x;
+}
+
+int main(void) {
+ f();
+ return 0;
+}
diff --git a/src/plugins/e-acsl/tests/runtime/localvar.c b/src/plugins/e-acsl/tests/memory/localvar.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/localvar.c
rename to src/plugins/e-acsl/tests/memory/localvar.c
diff --git a/src/plugins/e-acsl/tests/runtime/loop.i b/src/plugins/e-acsl/tests/memory/loop.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/loop.i
rename to src/plugins/e-acsl/tests/memory/loop.i
diff --git a/src/plugins/e-acsl/tests/runtime/mainargs.c b/src/plugins/e-acsl/tests/memory/mainargs.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/mainargs.c
rename to src/plugins/e-acsl/tests/memory/mainargs.c
diff --git a/src/plugins/e-acsl/tests/runtime/memalign.c b/src/plugins/e-acsl/tests/memory/memalign.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/memalign.c
rename to src/plugins/e-acsl/tests/memory/memalign.c
diff --git a/src/plugins/e-acsl/tests/runtime/memsize.c b/src/plugins/e-acsl/tests/memory/memsize.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/memsize.c
rename to src/plugins/e-acsl/tests/memory/memsize.c
diff --git a/src/plugins/e-acsl/tests/runtime/nested_code_annot.i b/src/plugins/e-acsl/tests/memory/nested_code_annot.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/nested_code_annot.i
rename to src/plugins/e-acsl/tests/memory/nested_code_annot.i
diff --git a/src/plugins/e-acsl/tests/runtime/null.i b/src/plugins/e-acsl/tests/memory/null.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/null.i
rename to src/plugins/e-acsl/tests/memory/null.i
diff --git a/src/plugins/e-acsl/tests/runtime/offset.c b/src/plugins/e-acsl/tests/memory/offset.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/offset.c
rename to src/plugins/e-acsl/tests/memory/offset.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/addrOf.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/addrOf.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/alias.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/alias.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/base_addr.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/base_addr.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/block_length.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/block_length.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
similarity index 54%
rename from src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
index 48f95d7442c30a836bf0d015d4e12c0f1066e5da..f7890eb4d148566132d047ad43471cd28b8bdb82 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/block_valid.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/block_valid.res.oracle
@@ -1,14 +1,14 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/block_valid.c:49: Warning:
+[eva:alarm] tests/memory/block_valid.c:49: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/block_valid.c:50: Warning:
+[eva:alarm] tests/memory/block_valid.c:50: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/block_valid.c:52: Warning:
+[eva:alarm] tests/memory/block_valid.c:52: Warning:
assertion got status unknown.
-[eva:alarm] tests/runtime/block_valid.c:52: Warning:
+[eva:alarm] tests/memory/block_valid.c:52: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/block_valid.c:54: Warning:
+[eva:alarm] tests/memory/block_valid.c:54: Warning:
assertion got status unknown.
-[eva:alarm] tests/runtime/block_valid.c:54: Warning:
+[eva:alarm] tests/memory/block_valid.c:54: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/bypassed_var.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/bypassed_var.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/call.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/call.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/call.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/compound_initializers.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/compound_initializers.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/constructor.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/constructor.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle
similarity index 92%
rename from src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle
index 7fc6c545d83858430806aab62d29eec4d80e3402..270dcdb0d84448a3889a178d504aa1b53f9de220 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/ctype_macros.res.oracle
@@ -2,14 +2,14 @@
[e-acsl] Warning: annotating undefined function `isupper':
the generated program may miss memory instrumentation
if there are memory-related annotations.
-[e-acsl] tests/runtime/ctype_macros.c:39: Warning:
+[e-acsl] tests/memory/ctype_macros.c:39: Warning:
E-ACSL construct `disjoint behaviors' is not yet supported.
Ignoring annotation.
[e-acsl] FRAMAC_SHARE/libc/ctype.h:174: Warning:
E-ACSL construct `assigns clause in behavior' is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/ctype_macros.c:37: Warning:
+[eva:alarm] tests/memory/ctype_macros.c:37: Warning:
function __gen_e_acsl_isupper: precondition 'c_uchar_or_eof' got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/ctype.h:174: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.err.oracle b/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.err.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.err.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.err.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/decl_in_switch.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/decl_in_switch.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle
similarity index 66%
rename from src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle
index 9cf5edeffd7452eead7705ae3f3bcc5670598732..965ff85803169a13ec505dc05504dd6b12557d30 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/early_exit.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:locals-escaping] tests/runtime/early_exit.c:14: Warning:
+[eva:locals-escaping] tests/memory/early_exit.c:14: Warning:
locals {a} escaping the scope of a block of goto_bts through p
-[eva:alarm] tests/runtime/early_exit.c:18: Warning:
+[eva:alarm] tests/memory/early_exit.c:18: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/errno.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/errno.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/false.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/false.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/false.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
similarity index 52%
rename from src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
index f443fc5cbacd6b1b92b9f2f8470bc2ef4d62bf12..960337255a23364989fe34b319f8d60e1147cfd4 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/freeable.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/freeable.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/freeable.c:15: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/freeable.c:15: Warning:
+[eva:alarm] tests/memory/freeable.c:15: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/freeable.c:15: Warning:
accessing uninitialized left-value. assert \initialized(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/function_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/function_contract.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/function_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c b/src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_addrOf.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_addrOf.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_alias.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_alias.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_base_addr.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_base_addr.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c b/src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_block_length.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_block_length.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c b/src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_block_valid.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_block_valid.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c b/src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_bypassed_var.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_bypassed_var.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_call.c b/src/plugins/e-acsl/tests/memory/oracle/gen_call.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_call.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_call.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c b/src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_compound_initializers.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_compound_initializers.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_constructor.c b/src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_constructor.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_constructor.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_ctype_macros.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_ctype_macros.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_decl_in_switch.c b/src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_decl_in_switch.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_decl_in_switch.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c b/src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_early_exit.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_early_exit.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c b/src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_errno.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_errno.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_false.c b/src/plugins/e-acsl/tests/memory/oracle/gen_false.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_false.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_false.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_freeable.c b/src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_freeable.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_freeable.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_function_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_function_contract.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_function_contract.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ghost.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_ghost.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_ghost.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_goto.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_goto.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_hidden_malloc.c b/src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_hidden_malloc.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_hidden_malloc.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_init.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_init.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c b/src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_init_function.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_init_function.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c b/src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_initialized.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_initialized.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/memory/oracle/gen_invariant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_invariant.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_invariant.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/memory/oracle/gen_labeled_stmt.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_labeled_stmt.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_labeled_stmt.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/memory/oracle/gen_lazy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_lazy.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_lazy.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/memory/oracle/gen_linear_search.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_linear_search.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_linear_search.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_literal_string.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_literal_string.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_local_goto.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_local_goto.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
new file mode 100644
index 0000000000000000000000000000000000000000..daf584a9f5877d874ac6c8289d8b46005716f8b1
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
@@ -0,0 +1,21 @@
+/* Generated by Frama-C */
+#include "stdio.h"
+#include "stdlib.h"
+int X = 0;
+int *p = & X;
+int f(void)
+{
+ int x = *p;
+ return x;
+}
+
+int main(void)
+{
+ int __retres;
+ __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
+ f();
+ __retres = 0;
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/memory/oracle/gen_localvar.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_localvar.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_localvar.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_loop.c b/src/plugins/e-acsl/tests/memory/oracle/gen_loop.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_loop.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_loop.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c b/src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_mainargs.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_mainargs.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_memalign.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_memalign.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c b/src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_memsize.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_memsize.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/memory/oracle/gen_nested_code_annot.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_nested_code_annot.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_nested_code_annot.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_null.c b/src/plugins/e-acsl/tests/memory/oracle/gen_null.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_null.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_null.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c b/src/plugins/e-acsl/tests/memory/oracle/gen_offset.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_offset.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_offset.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c b/src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_other_constants.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_other_constants.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_ptr.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_ptr.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_ptr_init.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_ptr_init.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_ranges_in_builtins.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_ranges_in_builtins.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_result.c b/src/plugins/e-acsl/tests/memory/oracle/gen_result.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_result.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_result.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c b/src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_sizeof.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_sizeof.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c b/src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_stdout.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_stdout.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_stmt_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_stmt_contract.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_stmt_contract.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_true.c b/src/plugins/e-acsl/tests/memory/oracle/gen_true.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_true.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_true.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/memory/oracle/gen_typedef.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_typedef.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_typedef.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_valid.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_valid.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_alias.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_valid_alias.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_valid_alias.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_valid_in_contract.c b/src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_valid_in_contract.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_valid_in_contract.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_vector.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_vector.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_vector.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_vla.c b/src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/gen_vla.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_vla.c
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ghost.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/ghost.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/ghost.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/goto.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/goto.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
similarity index 60%
rename from src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
index f4cfabb6990983d8cd7c939d73910391343c4a89..c136f7aec42d0af2d20d219eb393b8605ff89ec2 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
@@ -1,9 +1,9 @@
-[kernel:typing:implicit-function-declaration] tests/runtime/hidden_malloc.c:11: Warning:
+[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: Warning:
Calling undeclared function realpath. Old style K&R code?
[e-acsl] beginning translation.
-[kernel:annot:missing-spec] tests/runtime/hidden_malloc.c:11: Warning:
+[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:11: Warning:
Neither code nor specification for function realpath, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
-[eva:invalid-assigns] tests/runtime/hidden_malloc.c:11:
+[eva:invalid-assigns] tests/memory/hidden_malloc.c:11:
Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
Ignoring.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/init.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/init_function.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/init_function.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
similarity index 64%
rename from src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
index c420e591edcef860a33f6edcb47fcd8ebab9b193..f7e7728886dc25b4bc1a2d9754b0bae21bbdf61d 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/initialized.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/initialized.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/initialized.c:85: Warning:
+[eva:alarm] tests/memory/initialized.c:85: Warning:
assertion got status unknown.
-[eva:alarm] tests/runtime/initialized.c:85: Warning:
+[eva:alarm] tests/memory/initialized.c:85: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/invariant.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/invariant.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/invariant.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/labeled_stmt.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/labeled_stmt.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/labeled_stmt.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/lazy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/lazy.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/lazy.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/linear_search.res.oracle
similarity index 57%
rename from src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/linear_search.res.oracle
index d5e052174b0d3499c9bbaacbf7978d8aab92673f..d801720f4043cecfef2c1d1bf7255324c1970132 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/linear_search.res.oracle
@@ -1,24 +1,24 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/linear_search.i:30: Warning:
+[eva:alarm] tests/memory/linear_search.i:30: Warning:
function __gen_e_acsl_search: precondition got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:7: Warning:
+[eva:alarm] tests/memory/linear_search.i:7: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:18: Warning:
+[eva:alarm] tests/memory/linear_search.i:18: Warning:
loop invariant got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:18: Warning:
+[eva:alarm] tests/memory/linear_search.i:18: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:10: Warning:
+[eva:alarm] tests/memory/linear_search.i:10: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:13: Warning:
+[eva:alarm] tests/memory/linear_search.i:13: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:10: Warning:
+[eva:alarm] tests/memory/linear_search.i:10: Warning:
function __gen_e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-[eva:alarm] tests/runtime/linear_search.i:13: Warning:
+[eva:alarm] tests/memory/linear_search.i:13: Warning:
function __gen_e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-[eva:alarm] tests/runtime/linear_search.i:31: Warning:
+[eva:alarm] tests/memory/linear_search.i:31: Warning:
assertion got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:33: Warning:
+[eva:alarm] tests/memory/linear_search.i:33: Warning:
function __gen_e_acsl_search: precondition got status unknown.
-[eva:alarm] tests/runtime/linear_search.i:34: Warning:
+[eva:alarm] tests/memory/linear_search.i:34: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/literal_string.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/literal_string.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/local_goto.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..97c5a744275a62525111600a2c3961c0f760350c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
@@ -0,0 +1,6 @@
+[eva:alarm] tests/memory/local_init.c:11: Warning:
+ out of bounds read. assert \valid_read(p);
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/memory/local_init.c:11: Warning:
+ out of bounds read. assert \valid_read(p);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/localvar.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/localvar.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/localvar.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/loop.res.oracle
similarity index 57%
rename from src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/loop.res.oracle
index 0d697ba994df2e47db808c6e5b5fbbd3c6bcc88e..fced089a74cdcc74be45c8872bb6c5c32c4fee60 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/loop.res.oracle
@@ -1,8 +1,8 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/loop.i:19: Warning: loop invariant got status unknown.
-[eva:alarm] tests/runtime/loop.i:19: Warning:
+[eva:alarm] tests/memory/loop.i:19: Warning: loop invariant got status unknown.
+[eva:alarm] tests/memory/loop.i:19: Warning:
function __e_acsl_assert: precondition got status invalid.
-[eva:alarm] tests/runtime/loop.i:19: Warning:
+[eva:alarm] tests/memory/loop.i:19: Warning:
accessing uninitialized left-value.
assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
similarity index 61%
rename from src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
index f74e35f0e120a351bf3d408ef97f23e92f884ac2..9eb9554ffef0f06f41d3400d0b0fd721a00bc77a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/mainargs.res.oracle
@@ -13,31 +13,31 @@
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/mainargs.c:12: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:12: Warning:
+[eva:alarm] tests/memory/mainargs.c:12: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/mainargs.c:12: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:13: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:13: Warning:
+[eva:alarm] tests/memory/mainargs.c:13: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/mainargs.c:13: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:15: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:15: Warning:
+[eva:alarm] tests/memory/mainargs.c:15: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/mainargs.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:15: Warning:
+[eva:alarm] tests/memory/mainargs.c:15: Warning:
out of bounds read. assert \valid_read(argv + argc);
-[eva:alarm] tests/runtime/mainargs.c:16: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:16: Warning:
+[eva:alarm] tests/memory/mainargs.c:16: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/mainargs.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:16: Warning:
+[eva:alarm] tests/memory/mainargs.c:16: Warning:
out of bounds read. assert \valid_read(argv + argc);
-[eva:alarm] tests/runtime/mainargs.c:16: Warning:
+[eva:alarm] tests/memory/mainargs.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:18: Warning:
+[eva:alarm] tests/memory/mainargs.c:18: Warning:
function __gen_e_acsl_strlen: precondition 'valid_string_s' got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:125: Warning:
function strlen: precondition 'valid_string_s' got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/string.h:127: Warning:
function __gen_e_acsl_strlen: postcondition 'acsl_c_equiv' got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:19: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:20: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/mainargs.c:20: Warning:
+[eva:alarm] tests/memory/mainargs.c:19: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/mainargs.c:20: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/mainargs.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
similarity index 74%
rename from src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
index b7fc1a1f56521acd0b52bf324c7c7253b3258ab3..674eddac861dff410a723d4a8016853a5ce17ca5 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memalign.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memalign.res.oracle
@@ -1,4 +1,4 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/memalign.c:14: Warning:
+[eva:alarm] tests/memory/memalign.c:14: Warning:
accessing uninitialized left-value. assert \initialized(memptr);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
similarity index 50%
rename from src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
index 742bcfb05433e896ed6b89247eb1d514c025bab1..fa55190b709b62274337a74a41e71d53d610d76e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/memsize.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/memsize.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/memsize.c:14: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/memsize.c:16: Warning:
+[eva:alarm] tests/memory/memsize.c:14: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/memsize.c:16: Warning:
assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/nested_code_annot.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/nested_code_annot.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/nested_code_annot.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/null.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/null.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/null.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/offset.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/offset.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/other_constants.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/other_constants.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3e740b14f9a10f31564924427327d86fcde5839e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle
@@ -0,0 +1,11 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/memory/ptr.i:17: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/ptr.i:17: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/ptr.i:18: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/ptr.i:18: Warning:
+ function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/memory/ptr.i:19: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/ptr.i:19: Warning:
+ function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/ptr_init.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/ptr_init.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
similarity index 67%
rename from src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
index 2b65e90e6d9994eb574ae54dceaccbaf1e78732d..a6b067c83c9b1f9067ea56155bc55976e2060ea8 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ranges_in_builtins.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/ranges_in_builtins.res.oracle
@@ -1,8 +1,8 @@
[e-acsl] beginning translation.
-[e-acsl] tests/runtime/ranges_in_builtins.c:64: Warning:
+[e-acsl] tests/memory/ranges_in_builtins.c:64: Warning:
E-ACSL construct `arithmetic over set of pointers or arrays'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/ranges_in_builtins.c:21: Warning:
+[eva:alarm] tests/memory/ranges_in_builtins.c:21: Warning:
assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/result.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/result.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/result.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/sizeof.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/sizeof.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..1dd58d9e80a90a6f03c81e9c316feeb7f88fb00d
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
@@ -0,0 +1,5 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/memory/stdout.c:8: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/stdout.c:9: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/stdout.c:10: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/stmt_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/stmt_contract.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/stmt_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/true.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/true.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/true.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/typedef.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/typedef.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/typedef.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
similarity index 77%
rename from src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
index 64c906c2a8179bfce839b4ab20491a2820609fa1..cd7f1aa87849c440a475eac77cb35c1ba49f4e6b 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/valid.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/valid.c:47: Warning:
+[eva:alarm] tests/memory/valid.c:47: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
similarity index 75%
rename from src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
index eb7dbcce9ea36cd59e4a476f5da95c0f78ac783c..194beb0f9576f47839057994a6637161333348c3 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/valid_alias.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/valid_alias.c:17: Warning:
+[eva:alarm] tests/memory/valid_alias.c:17: Warning:
accessing left-value that contains escaping addresses.
assert ¬\dangling(&a);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/oracle/valid_in_contract.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/valid_in_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
similarity index 53%
rename from src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
index 1891087e5580531e7cb0f22b3349948d9625b8f9..32603d785fad7cddc36c5fd7924515a3062e9735 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/vector.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/vector.c:26: Warning:
+[eva:alarm] tests/memory/vector.c:26: Warning:
accessing uninitialized left-value. assert \initialized(v2 + 2);
-[eva:alarm] tests/runtime/vector.c:28: Warning: assertion got status unknown.
+[eva:alarm] tests/memory/vector.c:28: Warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/vla.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
similarity index 68%
rename from src/plugins/e-acsl/tests/runtime/oracle/vla.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
index 2fb5e519e75a36fc2186e535355e5075b309325a..50d32fb5962e6100f4dd17fd0041edf6b524f1dd 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/vla.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/vla.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/vla.c:8: Warning:
+[eva:alarm] tests/memory/vla.c:8: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/vla.c:12: Warning:
+[eva:alarm] tests/memory/vla.c:12: Warning:
assertion got status invalid (stopping propagation).
diff --git a/src/plugins/e-acsl/tests/runtime/other_constants.i b/src/plugins/e-acsl/tests/memory/other_constants.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/other_constants.i
rename to src/plugins/e-acsl/tests/memory/other_constants.i
diff --git a/src/plugins/e-acsl/tests/runtime/ptr.i b/src/plugins/e-acsl/tests/memory/ptr.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/ptr.i
rename to src/plugins/e-acsl/tests/memory/ptr.i
diff --git a/src/plugins/e-acsl/tests/runtime/ptr_init.c b/src/plugins/e-acsl/tests/memory/ptr_init.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/ptr_init.c
rename to src/plugins/e-acsl/tests/memory/ptr_init.c
diff --git a/src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c b/src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/ranges_in_builtins.c
rename to src/plugins/e-acsl/tests/memory/ranges_in_builtins.c
diff --git a/src/plugins/e-acsl/tests/runtime/result.i b/src/plugins/e-acsl/tests/memory/result.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/result.i
rename to src/plugins/e-acsl/tests/memory/result.i
diff --git a/src/plugins/e-acsl/tests/runtime/result/.gitkeep b/src/plugins/e-acsl/tests/memory/result/.gitkeep
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/result/.gitkeep
rename to src/plugins/e-acsl/tests/memory/result/.gitkeep
diff --git a/src/plugins/e-acsl/tests/runtime/sizeof.i b/src/plugins/e-acsl/tests/memory/sizeof.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/sizeof.i
rename to src/plugins/e-acsl/tests/memory/sizeof.i
diff --git a/src/plugins/e-acsl/tests/runtime/stdout.c b/src/plugins/e-acsl/tests/memory/stdout.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/stdout.c
rename to src/plugins/e-acsl/tests/memory/stdout.c
diff --git a/src/plugins/e-acsl/tests/runtime/stmt_contract.i b/src/plugins/e-acsl/tests/memory/stmt_contract.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/stmt_contract.i
rename to src/plugins/e-acsl/tests/memory/stmt_contract.i
diff --git a/src/plugins/e-acsl/tests/runtime/true.i b/src/plugins/e-acsl/tests/memory/true.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/true.i
rename to src/plugins/e-acsl/tests/memory/true.i
diff --git a/src/plugins/e-acsl/tests/runtime/typedef.i b/src/plugins/e-acsl/tests/memory/typedef.i
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/typedef.i
rename to src/plugins/e-acsl/tests/memory/typedef.i
diff --git a/src/plugins/e-acsl/tests/runtime/valid.c b/src/plugins/e-acsl/tests/memory/valid.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/valid.c
rename to src/plugins/e-acsl/tests/memory/valid.c
diff --git a/src/plugins/e-acsl/tests/runtime/valid_alias.c b/src/plugins/e-acsl/tests/memory/valid_alias.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/valid_alias.c
rename to src/plugins/e-acsl/tests/memory/valid_alias.c
diff --git a/src/plugins/e-acsl/tests/runtime/valid_in_contract.c b/src/plugins/e-acsl/tests/memory/valid_in_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/valid_in_contract.c
rename to src/plugins/e-acsl/tests/memory/valid_in_contract.c
diff --git a/src/plugins/e-acsl/tests/runtime/vector.c b/src/plugins/e-acsl/tests/memory/vector.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/vector.c
rename to src/plugins/e-acsl/tests/memory/vector.c
diff --git a/src/plugins/e-acsl/tests/runtime/vla.c b/src/plugins/e-acsl/tests/memory/vla.c
similarity index 100%
rename from src/plugins/e-acsl/tests/runtime/vla.c
rename to src/plugins/e-acsl/tests/memory/vla.c
diff --git a/src/plugins/e-acsl/tests/runtime/local_init.c b/src/plugins/e-acsl/tests/runtime/local_init.c
deleted file mode 100644
index 77f64afba262be597862db14820e8533c1092801..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/runtime/local_init.c
+++ /dev/null
@@ -1,19 +0,0 @@
-/* run.config
- COMMENT: test of a local initializer which contains an annotation
- LOG: gen_@PTEST_NAME@.c
- OPT: -e-acsl-prepare -val -lib-entry -then -e-acsl -then-last -load-script tests/print.cmxs -print -ocode @PTEST_DIR@/result/gen_@PTEST_NAME@.c
- EXEC: ./scripts/testrun.sh @PTEST_NAME@ runtime "" "--frama-c=@frama-c@ -F -val -F -lib-entry --then --e-acsl-extra=-no-lib-entry --e-acsl-extra=-no-val"
-*/
-
-int X = 0;
-int *p = &X;
-
-int f(void) {
- int x = *p; // Eva add an alarms on this statement
- return x;
-}
-
-int main(void) {
- f();
- return 0;
-}
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c b/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
deleted file mode 100644
index 74be6cc7f5ffd1acaaeaea6925404131181be632..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
+++ /dev/null
@@ -1,43 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-int X = 0;
-int *p = & X;
-int f(void)
-{
- /*@ assert Eva: mem_access: \valid_read(p); */
- {
- int __gen_e_acsl_valid_read;
- __gen_e_acsl_valid_read = __e_acsl_valid_read((void *)p,sizeof(int),
- (void *)p,(void *)(& p));
- __e_acsl_assert(__gen_e_acsl_valid_read,(char *)"Assertion",(char *)"f",
- (char *)"Eva: mem_access: \\valid_read(p)",12);
- }
- int x = *p;
- return x;
-}
-
-void __e_acsl_globals_init(void)
-{
- static char __e_acsl_already_run = 0;
- if (! __e_acsl_already_run) {
- __e_acsl_already_run = 1;
- __e_acsl_store_block((void *)(& p),(size_t)4);
- __e_acsl_full_init((void *)(& p));
- }
- return;
-}
-
-int main(void)
-{
- int __retres;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)4);
- __e_acsl_globals_init();
- f();
- __retres = 0;
- __e_acsl_delete_block((void *)(& p));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
deleted file mode 100644
index c2843c7332f5f5435981966f53ef7d71bac43ee4..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
+++ /dev/null
@@ -1,37 +0,0 @@
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h (with preprocessing)
-[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
-[kernel] Parsing tests/runtime/local_init.c (with preprocessing)
-[eva] Analyzing an incomplete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
- __e_acsl_init ∈ [--..--]
- __e_acsl_heap_allocation_size ∈ [--..--]
- __e_acsl_math_HUGE_VAL ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- __e_acsl_math_HUGE_VALF ∈ [-3.40282346639e+38 .. 3.40282346639e+38]
- __e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
- X ∈ [--..--]
- p ∈ {{ NULL ; &S_p[0] }}
- S_p[0..1] ∈ [--..--]
-[eva:alarm] tests/runtime/local_init.c:12: Warning:
- out of bounds read. assert \valid_read(p);
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function f:
- x ∈ [--..--]
-[eva:final-states] Values at end of function main:
- __retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
- ----------------------------------------------------------------------------
- 2 functions analyzed (out of 2): 100% coverage.
- In these functions, 5 statements reached (out of 5): 100% coverage.
- ----------------------------------------------------------------------------
- No errors or warnings raised during the analysis.
- ----------------------------------------------------------------------------
- 1 alarm generated by the analysis:
- 1 invalid memory access
- ----------------------------------------------------------------------------
- No logical properties have been reached by the analysis.
- ----------------------------------------------------------------------------
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
deleted file mode 100644
index 3dcc9b788d4ad029061919f0e958bb2000187a92..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
+++ /dev/null
@@ -1,11 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/ptr.i:17: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/ptr.i:17: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/ptr.i:18: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/ptr.i:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/runtime/ptr.i:19: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/ptr.i:19: Warning:
- function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
deleted file mode 100644
index f4bab4760739d58deaf094532df53dc535bbb77c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/runtime/stdout.c:8: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/stdout.c:9: Warning: assertion got status unknown.
-[eva:alarm] tests/runtime/stdout.c:10: Warning: assertion got status unknown.