From 2a0e80ad166a5bbcf5db3bc3174ac32654266975 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 30 Aug 2019 11:34:40 +0200
Subject: [PATCH] [tests] improve test organization
---
src/plugins/e-acsl/Makefile.in | 2 +
src/plugins/e-acsl/tests/arith/README.md | 1 -
.../oracle/functions_contiki.0.res.oracle | 25 -------
.../oracle/functions_contiki.1.res.oracle | 25 -------
.../arith/oracle/gen_functions_contiki2.c | 45 ------------
.../oracle/{gen_reals.c => gen_rationals.c} | 0
...{reals.res.oracle => rationals.res.oracle} | 48 ++++++------
.../tests/arith/oracle/reals.0.res.oracle | 73 -------------------
.../tests/arith/oracle/reals.1.res.oracle | 73 -------------------
.../tests/arith/{reals.c => rationals.c} | 0
.../e-acsl/tests/arith/reals1.c.notest | 16 ----
.../{arith => examples}/functions_contiki.c | 0
.../{memory => examples}/linear_search.i | 0
.../oracle/functions_contiki.res.oracle | 4 +-
.../oracle/gen_functions_contiki.c | 0
.../oracle/gen_linear_search.c | 0
.../oracle/linear_search.res.oracle | 22 +++---
.../{memory => language_constructs}/false.i | 0
.../function_contract.i | 0
.../{memory => language_constructs}/ghost.i | 0
.../invariant.i | 0
.../labeled_stmt.i | 0
.../{memory => language_constructs}/lazy.i | 0
.../{memory => language_constructs}/loop.i | 0
.../nested_code_annot.i | 0
.../oracle/false.res.oracle | 0
.../oracle/function_contract.res.oracle | 0
.../oracle/gen_false.c | 0
.../oracle/gen_function_contract.c | 0
.../oracle/gen_ghost.c | 0
.../oracle/gen_invariant.c | 0
.../oracle/gen_labeled_stmt.c | 0
.../oracle/gen_lazy.c | 0
.../oracle/gen_loop.c | 0
.../oracle/gen_nested_code_annot.c | 0
.../oracle/gen_result.c | 0
.../oracle/gen_stmt_contract.c | 0
.../oracle/gen_true.c | 0
.../oracle/gen_typedef.c | 0
.../oracle/ghost.res.oracle | 0
.../oracle/invariant.res.oracle | 0
.../oracle/labeled_stmt.res.oracle | 0
.../oracle/lazy.res.oracle | 0
.../oracle/loop.res.oracle | 7 +-
.../oracle/nested_code_annot.res.oracle | 0
.../oracle/result.res.oracle | 0
.../oracle/stmt_contract.res.oracle | 0
.../oracle/true.res.oracle | 0
.../oracle/typedef.res.oracle | 0
.../{memory => language_constructs}/result.i | 0
.../stmt_contract.i | 0
.../{memory => language_constructs}/true.i | 0
.../{memory => language_constructs}/typedef.i | 0
.../tests/memory/{localvar.c => local_var.c} | 0
.../{gen_localvar.c => gen_local_var.c} | 0
...calvar.res.oracle => local_var.res.oracle} | 0
56 files changed, 43 insertions(+), 298 deletions(-)
delete mode 100644 src/plugins/e-acsl/tests/arith/README.md
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle/functions_contiki.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle/functions_contiki.1.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle/gen_functions_contiki2.c
rename src/plugins/e-acsl/tests/arith/oracle/{gen_reals.c => gen_rationals.c} (100%)
rename src/plugins/e-acsl/tests/arith/oracle/{reals.res.oracle => rationals.res.oracle} (50%)
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle/reals.0.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/arith/oracle/reals.1.res.oracle
rename src/plugins/e-acsl/tests/arith/{reals.c => rationals.c} (100%)
delete mode 100644 src/plugins/e-acsl/tests/arith/reals1.c.notest
rename src/plugins/e-acsl/tests/{arith => examples}/functions_contiki.c (100%)
rename src/plugins/e-acsl/tests/{memory => examples}/linear_search.i (100%)
rename src/plugins/e-acsl/tests/{arith => examples}/oracle/functions_contiki.res.oracle (63%)
rename src/plugins/e-acsl/tests/{arith => examples}/oracle/gen_functions_contiki.c (100%)
rename src/plugins/e-acsl/tests/{memory => examples}/oracle/gen_linear_search.c (100%)
rename src/plugins/e-acsl/tests/{memory => examples}/oracle/linear_search.res.oracle (56%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/false.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/function_contract.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/ghost.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/invariant.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/labeled_stmt.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/lazy.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/loop.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/nested_code_annot.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/false.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/function_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_false.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_function_contract.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_ghost.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_invariant.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_labeled_stmt.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_lazy.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_loop.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_nested_code_annot.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_result.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_stmt_contract.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_true.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/gen_typedef.c (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/ghost.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/invariant.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/labeled_stmt.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/lazy.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/loop.res.oracle (52%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/nested_code_annot.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/result.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/stmt_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/true.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/oracle/typedef.res.oracle (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/result.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/stmt_contract.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/true.i (100%)
rename src/plugins/e-acsl/tests/{memory => language_constructs}/typedef.i (100%)
rename src/plugins/e-acsl/tests/memory/{localvar.c => local_var.c} (100%)
rename src/plugins/e-acsl/tests/memory/oracle/{gen_localvar.c => gen_local_var.c} (100%)
rename src/plugins/e-acsl/tests/memory/oracle/{localvar.res.oracle => local_var.res.oracle} (100%)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 3b549b22fe1..3d3906f7573 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 f1092ef51c3..00000000000
--- 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 c46fcfd437f..00000000000
--- 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 c46fcfd437f..00000000000
--- 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 259afb2e7cf..00000000000
--- 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 975ef40a79f..67c4a82c777 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 2c4d33e93dd..00000000000
--- 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 2c4d33e93dd..00000000000
--- 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 d5bd43dc37b..00000000000
--- 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 e0a5361d268..2327ee08af4 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 d801720f404..b63983be3e1 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 fced089a74c..db7f9a77ff5 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
--
GitLab