diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 3b549b22fe161e27847f04d0cd091c27de15644c..3d3906f75733a327c680d133eb8b2925c2a68d6a 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -171,7 +171,9 @@ ifeq (@MAY_RUN_TESTS@,yes)
-include in_frama_ci
PLUGIN_TESTS_DIRS := \
+ examples \
bts \
+ language_constructs \
arith \
memory \
full-mmodel \
diff --git a/src/plugins/e-acsl/tests/arith/README.md b/src/plugins/e-acsl/tests/arith/README.md
deleted file mode 100644
index f1092ef51c397a7f6a38c27cc6993e954887a745..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/README.md
+++ /dev/null
@@ -1 +0,0 @@
-Like runtime, but also test the -e-acsl-gmp-only mode.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.0.res.oracle
deleted file mode 100644
index c46fcfd437fbe80229820a34f46cab9345c29b1e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.0.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] tests/gmp/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] Analyzing a complete 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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_initialize
-[eva] using specification for function __e_acsl_full_init
-[eva] tests/gmp/functions_contiki.c:27:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function length
-[eva:alarm] tests/gmp/functions_contiki.c:27: Warning:
- assertion got status unknown.
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.1.res.oracle
deleted file mode 100644
index c46fcfd437fbe80229820a34f46cab9345c29b1e..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.1.res.oracle
+++ /dev/null
@@ -1,25 +0,0 @@
-[e-acsl] beginning translation.
-[e-acsl] tests/gmp/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] Analyzing a complete 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]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_store_block
-[eva] using specification for function __e_acsl_initialize
-[eva] using specification for function __e_acsl_full_init
-[eva] tests/gmp/functions_contiki.c:27:
- cannot evaluate ACSL term, unsupported ACSL construct: logic function length
-[eva:alarm] tests/gmp/functions_contiki.c:27: Warning:
- assertion got status unknown.
-[eva] using specification for function __e_acsl_delete_block
-[eva] using specification for function __e_acsl_memory_clean
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki2.c b/src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki2.c
deleted file mode 100644
index 259afb2e7cf7aff685e3f821c94a0a230968a678..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki2.c
+++ /dev/null
@@ -1,45 +0,0 @@
-/* Generated by Frama-C */
-#include "stdio.h"
-#include "stdlib.h"
-struct list {
- struct list *next ;
- int value ;
-};
-/*@
-logic ℤ length_aux{L}(struct list *l, ℤ n) =
- \at(n < 0? -1:
- (l ≡ (struct list *)((void *)0)? n:
- (n < 2147483647? length_aux(l->next, n + 1): -1)),
- L);
- */
-/*@ logic ℤ length{L}(struct list *l) = \at(length_aux(l, 0),L);
-
-*/
-int main(void)
-{
- int __retres;
- struct list node1;
- struct list node2;
- struct list node3;
- __e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
- __e_acsl_store_block((void *)(& node3),(size_t)16);
- __e_acsl_store_block((void *)(& node2),(size_t)16);
- __e_acsl_store_block((void *)(& node1),(size_t)16);
- __e_acsl_initialize((void *)(& node1.next),sizeof(struct list *));
- node1.next = & node2;
- __e_acsl_initialize((void *)(& node2.next),sizeof(struct list *));
- node2.next = & node3;
- struct list *l = & node1;
- __e_acsl_store_block((void *)(& l),(size_t)8);
- __e_acsl_full_init((void *)(& l));
- /*@ assert length(l) ≡ 3; */ ;
- __retres = 0;
- __e_acsl_delete_block((void *)(& l));
- __e_acsl_delete_block((void *)(& node3));
- __e_acsl_delete_block((void *)(& node2));
- __e_acsl_delete_block((void *)(& node1));
- __e_acsl_memory_clean();
- return __retres;
-}
-
-
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_reals.c b/src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_reals.c
rename to src/plugins/e-acsl/tests/arith/oracle/gen_rationals.c
diff --git a/src/plugins/e-acsl/tests/arith/oracle/reals.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
similarity index 50%
rename from src/plugins/e-acsl/tests/arith/oracle/reals.res.oracle
rename to src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
index 975ef40a79f060f8b00a6a94ed14e7779a22c44f..67c4a82c777f65f2dbe32802e3b32429ff0d3211 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/reals.res.oracle
+++ b/src/plugins/e-acsl/tests/arith/oracle/rationals.res.oracle
@@ -1,48 +1,48 @@
-[kernel:parser:decimal-float] tests/arith/reals.c:22: Warning:
+[kernel:parser:decimal-float] tests/arith/rationals.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/arith/reals.c:19: Warning:
+[e-acsl] tests/arith/rationals.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/arith/reals.c:15: Warning:
+[eva:alarm] tests/arith/rationals.c:15: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:16: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/reals.c:16: Warning:
+[eva:alarm] tests/arith/rationals.c:16: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:16: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:18: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/reals.c:18: Warning:
+[eva:alarm] tests/arith/rationals.c:18: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:18: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__6);
-[eva:alarm] tests/arith/reals.c:18: Warning:
+[eva:alarm] tests/arith/rationals.c:18: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] tests/arith/reals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:19: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/arith/reals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:19: Warning:
non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
-[eva:alarm] tests/arith/reals.c:19: Warning:
+[eva:alarm] tests/arith/rationals.c:19: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:20: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/reals.c:20: Warning:
+[eva:alarm] tests/arith/rationals.c:20: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:20: Warning:
non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/arith/reals.c:20: Warning:
+[eva:alarm] tests/arith/rationals.c:20: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:21: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/reals.c:21: Warning:
+[eva:alarm] tests/arith/rationals.c:21: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:21: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:25: Warning:
+[eva:alarm] tests/arith/rationals.c:25: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:26: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/reals.c:26: Warning:
+[eva:alarm] tests/arith/rationals.c:26: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:26: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:6: Warning:
+[eva:alarm] tests/arith/rationals.c:6: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/arith/reals.c:6: Warning:
+[eva:alarm] tests/arith/rationals.c:6: Warning:
function __gen_e_acsl_avg: postcondition got status unknown.
-[eva:alarm] tests/arith/reals.c:32: Warning: assertion got status unknown.
-[eva:alarm] tests/arith/reals.c:32: Warning:
+[eva:alarm] tests/arith/rationals.c:32: Warning: assertion got status unknown.
+[eva:alarm] tests/arith/rationals.c:32: Warning:
function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/reals.0.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/reals.0.res.oracle
deleted file mode 100644
index 2c4d33e93dd51c53b553bf0fd0719972b6b40452..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/reals.0.res.oracle
+++ /dev/null
@@ -1,73 +0,0 @@
-[kernel:parser:decimal-float] tests/gmp/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 construct `predicate with no definition nor reads clause'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete 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]
- __e_acsl_sound_verdict ∈ [--..--]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __gmpq_init
-[eva] using specification for function __gmpq_set_str
-[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_add
-[eva] using specification for function __gmpq_cmp
-[eva:alarm] tests/gmp/reals.c:15: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_clear
-[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/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] using specification for function __gmpq_get_d
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__6);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
-[eva:alarm] tests/gmp/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:
- non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/gmp/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] using specification for function __gmpq_sub
-[eva:alarm] tests/gmp/reals.c:21: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_mul
-[eva:alarm] tests/gmp/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] using specification for function __gmpq_set_si
-[eva:alarm] tests/gmp/reals.c:26: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_set
-[eva] using specification for function __gmpq_div
-[eva:alarm] tests/gmp/reals.c:6: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/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:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/oracle/reals.1.res.oracle b/src/plugins/e-acsl/tests/arith/oracle/reals.1.res.oracle
deleted file mode 100644
index 2c4d33e93dd51c53b553bf0fd0719972b6b40452..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/oracle/reals.1.res.oracle
+++ /dev/null
@@ -1,73 +0,0 @@
-[kernel:parser:decimal-float] tests/gmp/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 construct `predicate with no definition nor reads clause'
- is not yet supported.
- Ignoring annotation.
-[e-acsl] translation done in project "e-acsl".
-[eva] Analyzing a complete 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]
- __e_acsl_sound_verdict ∈ [--..--]
-[eva] using specification for function __e_acsl_memory_init
-[eva] using specification for function __e_acsl_assert
-[eva] using specification for function __gmpq_init
-[eva] using specification for function __gmpq_set_str
-[eva] using specification for function __gmpq_set_d
-[eva] using specification for function __gmpq_add
-[eva] using specification for function __gmpq_cmp
-[eva:alarm] tests/gmp/reals.c:15: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_clear
-[eva:alarm] tests/gmp/reals.c:16: Warning: assertion got status unknown.
-[eva:alarm] tests/gmp/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] using specification for function __gmpq_get_d
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__6);
-[eva:alarm] tests/gmp/reals.c:18: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__9);
-[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite double value. assert \is_finite(__gen_e_acsl__10);
-[eva:alarm] tests/gmp/reals.c:19: Warning:
- non-finite float value. assert \is_finite((float)__gen_e_acsl__9);
-[eva:alarm] tests/gmp/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:
- non-finite double value. assert \is_finite(__gen_e_acsl__12);
-[eva:alarm] tests/gmp/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] using specification for function __gmpq_sub
-[eva:alarm] tests/gmp/reals.c:21: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_mul
-[eva:alarm] tests/gmp/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] using specification for function __gmpq_set_si
-[eva:alarm] tests/gmp/reals.c:26: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva] using specification for function __gmpq_set
-[eva] using specification for function __gmpq_div
-[eva:alarm] tests/gmp/reals.c:6: Warning:
- function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/gmp/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:
- function __e_acsl_assert: precondition got status unknown.
-[eva] done for function main
diff --git a/src/plugins/e-acsl/tests/arith/reals.c b/src/plugins/e-acsl/tests/arith/rationals.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/reals.c
rename to src/plugins/e-acsl/tests/arith/rationals.c
diff --git a/src/plugins/e-acsl/tests/arith/reals1.c.notest b/src/plugins/e-acsl/tests/arith/reals1.c.notest
deleted file mode 100644
index d5bd43dc37b024f303e6ba2b69c90979de629ce5..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/tests/arith/reals1.c.notest
+++ /dev/null
@@ -1,16 +0,0 @@
-/* run.config
- COMMENT: real numbers
-*/
-
-/*@ ensures
- \let delta = 1;
- \let third_real = a/3;
- third_real - delta < \result < third_real + delta; */
-double third(double a) {
- return a/3;
-}
-
-int main(void) {
- int n = 1;
- third(11.7);
-}
\ No newline at end of file
diff --git a/src/plugins/e-acsl/tests/arith/functions_contiki.c b/src/plugins/e-acsl/tests/examples/functions_contiki.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/functions_contiki.c
rename to src/plugins/e-acsl/tests/examples/functions_contiki.c
diff --git a/src/plugins/e-acsl/tests/memory/linear_search.i b/src/plugins/e-acsl/tests/examples/linear_search.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/linear_search.i
rename to src/plugins/e-acsl/tests/examples/linear_search.i
diff --git a/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.res.oracle b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
similarity index 63%
rename from src/plugins/e-acsl/tests/arith/oracle/functions_contiki.res.oracle
rename to src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
index e0a5361d26819c95c0cdb8107a6d169ec948d5ef..2327ee08af4c360fa7edbcefdb921c527b678be7 100644
--- a/src/plugins/e-acsl/tests/arith/oracle/functions_contiki.res.oracle
+++ b/src/plugins/e-acsl/tests/examples/oracle/functions_contiki.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
-[e-acsl] tests/arith/functions_contiki.c:27: Warning:
+[e-acsl] tests/examples/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/arith/functions_contiki.c:27: Warning:
+[eva:alarm] tests/examples/functions_contiki.c:27: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki.c b/src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
similarity index 100%
rename from src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki.c
rename to src/plugins/e-acsl/tests/examples/oracle/gen_functions_contiki.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_linear_search.c b/src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_linear_search.c
rename to src/plugins/e-acsl/tests/examples/oracle/gen_linear_search.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle
similarity index 56%
rename from src/plugins/e-acsl/tests/memory/oracle/linear_search.res.oracle
rename to src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle
index d801720f4043cecfef2c1d1bf7255324c1970132..b63983be3e17ae3ca463ebecfc05a67f9a78d337 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/examples/oracle/linear_search.res.oracle
@@ -1,24 +1,24 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/linear_search.i:30: Warning:
+[eva:alarm] tests/examples/linear_search.i:30: Warning:
function __gen_e_acsl_search: precondition got status unknown.
-[eva:alarm] tests/memory/linear_search.i:7: Warning:
+[eva:alarm] tests/examples/linear_search.i:7: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/linear_search.i:18: Warning:
+[eva:alarm] tests/examples/linear_search.i:18: Warning:
loop invariant got status unknown.
-[eva:alarm] tests/memory/linear_search.i:18: Warning:
+[eva:alarm] tests/examples/linear_search.i:18: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/linear_search.i:10: Warning:
+[eva:alarm] tests/examples/linear_search.i:10: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/linear_search.i:13: Warning:
+[eva:alarm] tests/examples/linear_search.i:13: Warning:
function __e_acsl_assert: precondition got status unknown.
-[eva:alarm] tests/memory/linear_search.i:10: Warning:
+[eva:alarm] tests/examples/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/memory/linear_search.i:13: Warning:
+[eva:alarm] tests/examples/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/memory/linear_search.i:31: Warning:
+[eva:alarm] tests/examples/linear_search.i:31: Warning:
assertion got status unknown.
-[eva:alarm] tests/memory/linear_search.i:33: Warning:
+[eva:alarm] tests/examples/linear_search.i:33: Warning:
function __gen_e_acsl_search: precondition got status unknown.
-[eva:alarm] tests/memory/linear_search.i:34: Warning:
+[eva:alarm] tests/examples/linear_search.i:34: Warning:
assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/memory/false.i b/src/plugins/e-acsl/tests/language_constructs/false.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/false.i
rename to src/plugins/e-acsl/tests/language_constructs/false.i
diff --git a/src/plugins/e-acsl/tests/memory/function_contract.i b/src/plugins/e-acsl/tests/language_constructs/function_contract.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/function_contract.i
rename to src/plugins/e-acsl/tests/language_constructs/function_contract.i
diff --git a/src/plugins/e-acsl/tests/memory/ghost.i b/src/plugins/e-acsl/tests/language_constructs/ghost.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/ghost.i
rename to src/plugins/e-acsl/tests/language_constructs/ghost.i
diff --git a/src/plugins/e-acsl/tests/memory/invariant.i b/src/plugins/e-acsl/tests/language_constructs/invariant.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/invariant.i
rename to src/plugins/e-acsl/tests/language_constructs/invariant.i
diff --git a/src/plugins/e-acsl/tests/memory/labeled_stmt.i b/src/plugins/e-acsl/tests/language_constructs/labeled_stmt.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/labeled_stmt.i
rename to src/plugins/e-acsl/tests/language_constructs/labeled_stmt.i
diff --git a/src/plugins/e-acsl/tests/memory/lazy.i b/src/plugins/e-acsl/tests/language_constructs/lazy.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/lazy.i
rename to src/plugins/e-acsl/tests/language_constructs/lazy.i
diff --git a/src/plugins/e-acsl/tests/memory/loop.i b/src/plugins/e-acsl/tests/language_constructs/loop.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/loop.i
rename to src/plugins/e-acsl/tests/language_constructs/loop.i
diff --git a/src/plugins/e-acsl/tests/memory/nested_code_annot.i b/src/plugins/e-acsl/tests/language_constructs/nested_code_annot.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/nested_code_annot.i
rename to src/plugins/e-acsl/tests/language_constructs/nested_code_annot.i
diff --git a/src/plugins/e-acsl/tests/memory/oracle/false.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/false.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/false.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/false.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/function_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/function_contract.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/function_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_false.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_false.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_false.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_false.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_function_contract.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_function_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_function_contract.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_function_contract.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_ghost.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_ghost.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_ghost.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_invariant.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_invariant.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_invariant.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_invariant.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_labeled_stmt.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_labeled_stmt.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_labeled_stmt.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_lazy.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_lazy.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_lazy.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_lazy.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_loop.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_loop.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_loop.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_loop.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_nested_code_annot.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_nested_code_annot.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_nested_code_annot.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_result.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_result.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_result.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_result.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_stmt_contract.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_stmt_contract.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_stmt_contract.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_stmt_contract.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_true.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_true.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_true.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_true.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_typedef.c b/src/plugins/e-acsl/tests/language_constructs/oracle/gen_typedef.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_typedef.c
rename to src/plugins/e-acsl/tests/language_constructs/oracle/gen_typedef.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/ghost.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/ghost.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/ghost.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/invariant.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/invariant.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/invariant.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/labeled_stmt.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/labeled_stmt.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/labeled_stmt.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/lazy.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/lazy.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/lazy.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/loop.res.oracle
similarity index 52%
rename from src/plugins/e-acsl/tests/memory/oracle/loop.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/loop.res.oracle
index fced089a74cdcc74be45c8872bb6c5c32c4fee60..db7f9a77ff5ebcbc7f5e95180bfd7bb32cf96f7a 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/language_constructs/oracle/loop.res.oracle
@@ -1,8 +1,9 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[eva:alarm] tests/memory/loop.i:19: Warning: loop invariant got status unknown.
-[eva:alarm] tests/memory/loop.i:19: Warning:
+[eva:alarm] tests/language_constructs/loop.i:19: Warning:
+ loop invariant got status unknown.
+[eva:alarm] tests/language_constructs/loop.i:19: Warning:
function __e_acsl_assert: precondition got status invalid.
-[eva:alarm] tests/memory/loop.i:19: Warning:
+[eva:alarm] tests/language_constructs/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/memory/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/nested_code_annot.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/nested_code_annot.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/nested_code_annot.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/result.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/result.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/result.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/result.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/stmt_contract.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/stmt_contract.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/stmt_contract.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/true.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/true.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/true.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/true.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/language_constructs/oracle/typedef.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/typedef.res.oracle
rename to src/plugins/e-acsl/tests/language_constructs/oracle/typedef.res.oracle
diff --git a/src/plugins/e-acsl/tests/memory/result.i b/src/plugins/e-acsl/tests/language_constructs/result.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/result.i
rename to src/plugins/e-acsl/tests/language_constructs/result.i
diff --git a/src/plugins/e-acsl/tests/memory/stmt_contract.i b/src/plugins/e-acsl/tests/language_constructs/stmt_contract.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/stmt_contract.i
rename to src/plugins/e-acsl/tests/language_constructs/stmt_contract.i
diff --git a/src/plugins/e-acsl/tests/memory/true.i b/src/plugins/e-acsl/tests/language_constructs/true.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/true.i
rename to src/plugins/e-acsl/tests/language_constructs/true.i
diff --git a/src/plugins/e-acsl/tests/memory/typedef.i b/src/plugins/e-acsl/tests/language_constructs/typedef.i
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/typedef.i
rename to src/plugins/e-acsl/tests/language_constructs/typedef.i
diff --git a/src/plugins/e-acsl/tests/memory/localvar.c b/src/plugins/e-acsl/tests/memory/local_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/localvar.c
rename to src/plugins/e-acsl/tests/memory/local_var.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/gen_localvar.c b/src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/gen_localvar.c
rename to src/plugins/e-acsl/tests/memory/oracle/gen_local_var.c
diff --git a/src/plugins/e-acsl/tests/memory/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle
similarity index 100%
rename from src/plugins/e-acsl/tests/memory/oracle/localvar.res.oracle
rename to src/plugins/e-acsl/tests/memory/oracle/local_var.res.oracle