From c1e986263ec9e9f7f6df20dc6cbbcecf1db00c93 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 30 Aug 2019 11:10:14 +0200
Subject: [PATCH] [tests] rename gmp to arith and runtime to memory
---
src/plugins/e-acsl/.gitignore | 14 +---
src/plugins/e-acsl/Makefile.in | 7 +-
.../e-acsl/tests/{gmp => arith}/README.md | 0
.../e-acsl/tests/{gmp => arith}/arith.i | 0
.../e-acsl/tests/{gmp => arith}/array.i | 0
src/plugins/e-acsl/tests/{gmp => arith}/at.i | 0
.../at_on-purely-logic-variables.c | 0
.../e-acsl/tests/{gmp => arith}/cast.i | 0
.../e-acsl/tests/{gmp => arith}/comparison.i | 0
.../e-acsl/tests/{gmp => arith}/functions.c | 0
.../tests/{gmp => arith}/functions_contiki.c | 0
.../tests/{gmp => arith}/functions_rec.c | 0
.../tests/{gmp => arith}/integer_constant.i | 0
src/plugins/e-acsl/tests/{gmp => arith}/let.c | 0
.../e-acsl/tests/{gmp => arith}/longlong.i | 0
src/plugins/e-acsl/tests/{gmp => arith}/not.i | 0
.../{gmp => arith}/oracle/arith.0.res.oracle | 0
.../{gmp => arith}/oracle/arith.1.res.oracle | 0
.../{gmp => arith}/oracle/arith.res.oracle | 10 +--
.../{gmp => arith}/oracle/array.0.res.oracle | 0
.../{gmp => arith}/oracle/array.1.res.oracle | 0
.../tests/arith/oracle/array.res.oracle | 8 +++
.../{gmp => arith}/oracle/at.0.res.oracle | 0
.../{gmp => arith}/oracle/at.1.res.oracle | 0
.../e-acsl/tests/arith/oracle/at.res.oracle | 9 +++
.../at_on-purely-logic-variables.0.res.oracle | 0
.../at_on-purely-logic-variables.1.res.oracle | 0
.../at_on-purely-logic-variables.res.oracle | 64 +++++++++----------
.../{gmp => arith}/oracle/cast.0.res.oracle | 0
.../{gmp => arith}/oracle/cast.1.res.oracle | 0
.../{gmp => arith}/oracle/cast.res.oracle | 2 +-
.../oracle/comparison.0.res.oracle | 0
.../oracle/comparison.1.res.oracle | 0
.../oracle/comparison.res.oracle | 0
.../oracle/functions.0.res.oracle | 0
.../oracle/functions.1.res.oracle | 0
.../oracle/functions.res.oracle | 12 ++--
.../oracle/functions_contiki.0.res.oracle | 0
.../oracle/functions_contiki.1.res.oracle | 0
.../oracle/functions_contiki.res.oracle | 4 +-
.../oracle/functions_rec.0.res.oracle | 0
.../oracle/functions_rec.1.res.oracle | 0
.../oracle/functions_rec.res.oracle | 61 +++++++++---------
.../tests/{gmp => arith}/oracle/gen_arith.c | 0
.../tests/{gmp => arith}/oracle/gen_arith2.c | 0
.../tests/{gmp => arith}/oracle/gen_array.c | 0
.../tests/{gmp => arith}/oracle/gen_array2.c | 0
.../tests/{gmp => arith}/oracle/gen_at.c | 0
.../tests/{gmp => arith}/oracle/gen_at2.c | 0
.../oracle/gen_at_on-purely-logic-variables.c | 0
.../gen_at_on-purely-logic-variables2.c | 0
.../tests/{gmp => arith}/oracle/gen_cast.c | 0
.../tests/{gmp => arith}/oracle/gen_cast2.c | 0
.../{gmp => arith}/oracle/gen_comparison.c | 0
.../{gmp => arith}/oracle/gen_comparison2.c | 0
.../{gmp => arith}/oracle/gen_functions.c | 0
.../{gmp => arith}/oracle/gen_functions2.c | 0
.../oracle/gen_functions_contiki.c | 0
.../oracle/gen_functions_contiki2.c | 0
.../{gmp => arith}/oracle/gen_functions_rec.c | 0
.../oracle/gen_functions_rec2.c | 0
.../oracle/gen_integer_constant.c | 0
.../oracle/gen_integer_constant2.c | 0
.../tests/{gmp => arith}/oracle/gen_let.c | 0
.../tests/{gmp => arith}/oracle/gen_let2.c | 0
.../{gmp => arith}/oracle/gen_longlong.c | 0
.../{gmp => arith}/oracle/gen_longlong2.c | 0
.../tests/{gmp => arith}/oracle/gen_not.c | 0
.../tests/{gmp => arith}/oracle/gen_not2.c | 0
.../tests/{gmp => arith}/oracle/gen_quantif.c | 0
.../{gmp => arith}/oracle/gen_quantif2.c | 0
.../tests/{gmp => arith}/oracle/gen_reals.c | 0
.../tests/{gmp => arith}/oracle/gen_reals2.c | 0
.../oracle/integer_constant.0.res.oracle | 0
.../oracle/integer_constant.1.res.oracle | 0
.../oracle/integer_constant.res.oracle | 2 +-
.../{gmp => arith}/oracle/let.0.res.oracle | 0
.../{gmp => arith}/oracle/let.1.res.oracle | 0
.../e-acsl/tests/arith/oracle/let.res.oracle | 19 ++++++
.../oracle/longlong.0.res.oracle | 0
.../oracle/longlong.1.res.oracle | 0
.../{gmp => arith}/oracle/longlong.res.oracle | 12 ++--
.../{gmp => arith}/oracle/not.0.res.oracle | 0
.../{gmp => arith}/oracle/not.1.res.oracle | 0
.../{gmp => arith}/oracle/not.res.oracle | 0
.../oracle/quantif.0.res.oracle | 0
.../oracle/quantif.1.res.oracle | 0
.../tests/arith/oracle/quantif.res.oracle | 25 ++++++++
.../{gmp => arith}/oracle/reals.0.res.oracle | 0
.../{gmp => arith}/oracle/reals.1.res.oracle | 0
.../{gmp => arith}/oracle/reals.res.oracle | 48 +++++++-------
.../e-acsl/tests/{gmp => arith}/quantif.i | 0
.../e-acsl/tests/{gmp => arith}/reals.c | 0
.../tests/{gmp => arith}/reals1.c.notest | 0
.../tests/{gmp => arith}/result/.gitkeep | 0
.../e-acsl/tests/gmp/oracle/array.res.oracle | 8 ---
.../e-acsl/tests/gmp/oracle/at.res.oracle | 9 ---
.../e-acsl/tests/gmp/oracle/let.res.oracle | 19 ------
.../tests/gmp/oracle/quantif.res.oracle | 25 --------
.../e-acsl/tests/{runtime => memory}/addrOf.i | 0
.../e-acsl/tests/{runtime => memory}/alias.i | 0
.../tests/{runtime => memory}/base_addr.c | 0
.../tests/{runtime => memory}/block_length.c | 0
.../tests/{runtime => memory}/block_valid.c | 0
.../tests/{runtime => memory}/bypassed_var.c | 0
.../e-acsl/tests/{runtime => memory}/call.c | 0
.../compound_initializers.c | 0
.../tests/{runtime => memory}/constructor.c | 0
.../tests/{runtime => memory}/ctype_macros.c | 0
.../{runtime => memory}/decl_in_switch.c | 0
.../tests/{runtime => memory}/early_exit.c | 0
.../e-acsl/tests/{runtime => memory}/errno.c | 0
.../e-acsl/tests/{runtime => memory}/false.i | 0
.../tests/{runtime => memory}/freeable.c | 0
.../{runtime => memory}/function_contract.i | 0
.../e-acsl/tests/{runtime => memory}/ghost.i | 0
.../e-acsl/tests/{runtime => memory}/goto.c | 0
.../tests/{runtime => memory}/hidden_malloc.c | 0
.../e-acsl/tests/{runtime => memory}/init.c | 0
.../tests/{runtime => memory}/init_function.c | 0
.../tests/{runtime => memory}/initialized.c | 0
.../tests/{runtime => memory}/invariant.i | 0
.../tests/{runtime => memory}/labeled_stmt.i | 0
.../e-acsl/tests/{runtime => memory}/lazy.i | 0
.../tests/{runtime => memory}/linear_search.i | 0
.../{runtime => memory}/literal_string.i | 0
.../tests/{runtime => memory}/local_goto.c | 0
src/plugins/e-acsl/tests/memory/local_init.c | 18 ++++++
.../tests/{runtime => memory}/localvar.c | 0
.../e-acsl/tests/{runtime => memory}/loop.i | 0
.../tests/{runtime => memory}/mainargs.c | 0
.../tests/{runtime => memory}/memalign.c | 0
.../tests/{runtime => memory}/memsize.c | 0
.../{runtime => memory}/nested_code_annot.i | 0
.../e-acsl/tests/{runtime => memory}/null.i | 0
.../e-acsl/tests/{runtime => memory}/offset.c | 0
.../oracle/addrOf.res.oracle | 0
.../oracle/alias.res.oracle | 0
.../oracle/base_addr.res.oracle | 0
.../oracle/block_length.res.oracle | 0
.../oracle/block_valid.res.oracle | 12 ++--
.../oracle/bypassed_var.res.oracle | 0
.../oracle/call.res.oracle | 0
.../oracle/compound_initializers.res.oracle | 0
.../oracle/constructor.res.oracle | 0
.../oracle/ctype_macros.res.oracle | 4 +-
.../oracle/decl_in_switch.err.oracle | 0
.../oracle/decl_in_switch.res.oracle | 0
.../oracle/early_exit.res.oracle | 4 +-
.../oracle/errno.res.oracle | 0
.../oracle/false.res.oracle | 0
.../oracle/freeable.res.oracle | 4 +-
.../oracle/function_contract.res.oracle | 0
.../{runtime => memory}/oracle/gen_addrOf.c | 0
.../{runtime => memory}/oracle/gen_alias.c | 0
.../oracle/gen_base_addr.c | 0
.../oracle/gen_block_length.c | 0
.../oracle/gen_block_valid.c | 0
.../oracle/gen_bypassed_var.c | 0
.../{runtime => memory}/oracle/gen_call.c | 0
.../oracle/gen_compound_initializers.c | 0
.../oracle/gen_constructor.c | 0
.../oracle/gen_ctype_macros.c | 0
.../oracle/gen_decl_in_switch.c | 0
.../oracle/gen_early_exit.c | 0
.../{runtime => memory}/oracle/gen_errno.c | 0
.../{runtime => memory}/oracle/gen_false.c | 0
.../{runtime => memory}/oracle/gen_freeable.c | 0
.../oracle/gen_function_contract.c | 0
.../{runtime => memory}/oracle/gen_ghost.c | 0
.../{runtime => memory}/oracle/gen_goto.c | 0
.../oracle/gen_hidden_malloc.c | 0
.../{runtime => memory}/oracle/gen_init.c | 0
.../oracle/gen_init_function.c | 0
.../oracle/gen_initialized.c | 0
.../oracle/gen_invariant.c | 0
.../oracle/gen_labeled_stmt.c | 0
.../{runtime => memory}/oracle/gen_lazy.c | 0
.../oracle/gen_linear_search.c | 0
.../oracle/gen_literal_string.c | 0
.../oracle/gen_local_goto.c | 0
.../tests/memory/oracle/gen_local_init.c | 21 ++++++
.../{runtime => memory}/oracle/gen_localvar.c | 0
.../{runtime => memory}/oracle/gen_loop.c | 0
.../{runtime => memory}/oracle/gen_mainargs.c | 0
.../{runtime => memory}/oracle/gen_memalign.c | 0
.../{runtime => memory}/oracle/gen_memsize.c | 0
.../oracle/gen_nested_code_annot.c | 0
.../{runtime => memory}/oracle/gen_null.c | 0
.../{runtime => memory}/oracle/gen_offset.c | 0
.../oracle/gen_other_constants.c | 0
.../{runtime => memory}/oracle/gen_ptr.c | 0
.../{runtime => memory}/oracle/gen_ptr_init.c | 0
.../oracle/gen_ranges_in_builtins.c | 0
.../{runtime => memory}/oracle/gen_result.c | 0
.../{runtime => memory}/oracle/gen_sizeof.c | 0
.../{runtime => memory}/oracle/gen_stdout.c | 0
.../oracle/gen_stmt_contract.c | 0
.../{runtime => memory}/oracle/gen_true.c | 0
.../{runtime => memory}/oracle/gen_typedef.c | 0
.../{runtime => memory}/oracle/gen_valid.c | 0
.../oracle/gen_valid_alias.c | 0
.../oracle/gen_valid_in_contract.c | 0
.../{runtime => memory}/oracle/gen_vector.c | 0
.../{runtime => memory}/oracle/gen_vla.c | 0
.../oracle/ghost.res.oracle | 0
.../oracle/goto.res.oracle | 0
.../oracle/hidden_malloc.res.oracle | 6 +-
.../oracle/init.res.oracle | 0
.../oracle/init_function.res.oracle | 0
.../oracle/initialized.res.oracle | 4 +-
.../oracle/invariant.res.oracle | 0
.../oracle/labeled_stmt.res.oracle | 0
.../oracle/lazy.res.oracle | 0
.../oracle/linear_search.res.oracle | 22 +++----
.../oracle/literal_string.res.oracle | 0
.../oracle/local_goto.res.oracle | 0
.../tests/memory/oracle/local_init.res.oracle | 6 ++
.../oracle/localvar.res.oracle | 0
.../oracle/loop.res.oracle | 6 +-
.../oracle/mainargs.res.oracle | 30 ++++-----
.../oracle/memalign.res.oracle | 2 +-
.../oracle/memsize.res.oracle | 4 +-
.../oracle/nested_code_annot.res.oracle | 0
.../oracle/null.res.oracle | 0
.../oracle/offset.res.oracle | 0
.../oracle/other_constants.res.oracle | 0
.../e-acsl/tests/memory/oracle/ptr.res.oracle | 11 ++++
.../oracle/ptr_init.res.oracle | 0
.../oracle/ranges_in_builtins.res.oracle | 4 +-
.../oracle/result.res.oracle | 0
.../oracle/sizeof.res.oracle | 0
.../tests/memory/oracle/stdout.res.oracle | 5 ++
.../oracle/stmt_contract.res.oracle | 0
.../oracle/true.res.oracle | 0
.../oracle/typedef.res.oracle | 0
.../oracle/valid.res.oracle | 2 +-
.../oracle/valid_alias.res.oracle | 2 +-
.../oracle/valid_in_contract.res.oracle | 0
.../oracle/vector.res.oracle | 4 +-
.../{runtime => memory}/oracle/vla.res.oracle | 4 +-
.../{runtime => memory}/other_constants.i | 0
.../e-acsl/tests/{runtime => memory}/ptr.i | 0
.../tests/{runtime => memory}/ptr_init.c | 0
.../{runtime => memory}/ranges_in_builtins.c | 0
.../e-acsl/tests/{runtime => memory}/result.i | 0
.../tests/{runtime => memory}/result/.gitkeep | 0
.../e-acsl/tests/{runtime => memory}/sizeof.i | 0
.../e-acsl/tests/{runtime => memory}/stdout.c | 0
.../tests/{runtime => memory}/stmt_contract.i | 0
.../e-acsl/tests/{runtime => memory}/true.i | 0
.../tests/{runtime => memory}/typedef.i | 0
.../e-acsl/tests/{runtime => memory}/valid.c | 0
.../tests/{runtime => memory}/valid_alias.c | 0
.../{runtime => memory}/valid_in_contract.c | 0
.../e-acsl/tests/{runtime => memory}/vector.c | 0
.../e-acsl/tests/{runtime => memory}/vla.c | 0
src/plugins/e-acsl/tests/runtime/local_init.c | 19 ------
.../tests/runtime/oracle/gen_local_init.c | 43 -------------
.../runtime/oracle/local_init.res.oracle | 37 -----------
.../tests/runtime/oracle/ptr.res.oracle | 11 ----
.../tests/runtime/oracle/stdout.res.oracle | 5 --
262 files changed, 292 insertions(+), 356 deletions(-)
rename src/plugins/e-acsl/tests/{gmp => arith}/README.md (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/arith.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/array.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/at.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/at_on-purely-logic-variables.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/cast.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/comparison.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/functions.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/functions_contiki.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/functions_rec.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/integer_constant.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/let.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/longlong.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/not.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/arith.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/arith.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/arith.res.oracle (62%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/array.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/array.1.res.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/array.res.oracle
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/at.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/at.1.res.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/at.res.oracle
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/at_on-purely-logic-variables.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/at_on-purely-logic-variables.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/at_on-purely-logic-variables.res.oracle (53%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/cast.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/cast.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/cast.res.oracle (78%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/comparison.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/comparison.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/comparison.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions.res.oracle (59%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions_contiki.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions_contiki.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions_contiki.res.oracle (64%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions_rec.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions_rec.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/functions_rec.res.oracle (61%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_arith.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_arith2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_array.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_array2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_at.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_at2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_at_on-purely-logic-variables.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_at_on-purely-logic-variables2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_cast.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_cast2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_comparison.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_comparison2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_functions.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_functions2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_functions_contiki.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_functions_contiki2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_functions_rec.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_functions_rec2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_integer_constant.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_integer_constant2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_let.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_let2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_longlong.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_longlong2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_not.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_not2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_quantif.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_quantif2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_reals.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/gen_reals2.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/integer_constant.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/integer_constant.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/integer_constant.res.oracle (71%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/let.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/let.1.res.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/let.res.oracle
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/longlong.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/longlong.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/longlong.res.oracle (55%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/not.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/not.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/not.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/quantif.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/quantif.1.res.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/arith/oracle/quantif.res.oracle
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/reals.0.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/reals.1.res.oracle (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/oracle/reals.res.oracle (52%)
rename src/plugins/e-acsl/tests/{gmp => arith}/quantif.i (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/reals.c (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/reals1.c.notest (100%)
rename src/plugins/e-acsl/tests/{gmp => arith}/result/.gitkeep (100%)
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/array.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/at.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/let.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/gmp/oracle/quantif.res.oracle
rename src/plugins/e-acsl/tests/{runtime => memory}/addrOf.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/alias.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/base_addr.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/block_length.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/block_valid.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/bypassed_var.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/call.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/compound_initializers.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/constructor.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/ctype_macros.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/decl_in_switch.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/early_exit.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/errno.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/false.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/freeable.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/function_contract.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/ghost.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/goto.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/hidden_malloc.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/init.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/init_function.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/initialized.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/invariant.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/labeled_stmt.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/lazy.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/linear_search.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/literal_string.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/local_goto.c (100%)
create mode 100644 src/plugins/e-acsl/tests/memory/local_init.c
rename src/plugins/e-acsl/tests/{runtime => memory}/localvar.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/loop.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/mainargs.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/memalign.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/memsize.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/nested_code_annot.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/null.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/offset.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/addrOf.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/alias.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/base_addr.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/block_length.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/block_valid.res.oracle (54%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/bypassed_var.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/call.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/compound_initializers.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/constructor.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/ctype_macros.res.oracle (92%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/decl_in_switch.err.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/decl_in_switch.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/early_exit.res.oracle (66%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/errno.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/false.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/freeable.res.oracle (52%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/function_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_addrOf.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_alias.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_base_addr.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_block_length.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_block_valid.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_bypassed_var.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_call.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_compound_initializers.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_constructor.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_ctype_macros.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_decl_in_switch.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_early_exit.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_errno.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_false.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_freeable.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_function_contract.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_ghost.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_goto.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_hidden_malloc.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_init.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_init_function.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_initialized.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_invariant.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_labeled_stmt.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_lazy.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_linear_search.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_literal_string.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_local_goto.c (100%)
create mode 100644 src/plugins/e-acsl/tests/memory/oracle/gen_local_init.c
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_localvar.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_loop.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_mainargs.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_memalign.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_memsize.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_nested_code_annot.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_null.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_offset.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_other_constants.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_ptr.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_ptr_init.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_ranges_in_builtins.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_result.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_sizeof.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_stdout.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_stmt_contract.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_true.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_typedef.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_valid.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_valid_alias.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_valid_in_contract.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_vector.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/gen_vla.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/ghost.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/goto.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/hidden_malloc.res.oracle (60%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/init.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/init_function.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/initialized.res.oracle (64%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/invariant.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/labeled_stmt.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/lazy.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/linear_search.res.oracle (57%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/literal_string.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/local_goto.res.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/memory/oracle/local_init.res.oracle
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/localvar.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/loop.res.oracle (57%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/mainargs.res.oracle (61%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/memalign.res.oracle (74%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/memsize.res.oracle (50%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/nested_code_annot.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/null.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/offset.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/other_constants.res.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/memory/oracle/ptr.res.oracle
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/ptr_init.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/ranges_in_builtins.res.oracle (67%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/result.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/sizeof.res.oracle (100%)
create mode 100644 src/plugins/e-acsl/tests/memory/oracle/stdout.res.oracle
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/stmt_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/true.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/typedef.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/valid.res.oracle (77%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/valid_alias.res.oracle (75%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/valid_in_contract.res.oracle (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/vector.res.oracle (53%)
rename src/plugins/e-acsl/tests/{runtime => memory}/oracle/vla.res.oracle (68%)
rename src/plugins/e-acsl/tests/{runtime => memory}/other_constants.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/ptr.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/ptr_init.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/ranges_in_builtins.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/result.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/result/.gitkeep (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/sizeof.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/stdout.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/stmt_contract.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/true.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/typedef.i (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/valid.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/valid_alias.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/valid_in_contract.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/vector.c (100%)
rename src/plugins/e-acsl/tests/{runtime => memory}/vla.c (100%)
delete mode 100644 src/plugins/e-acsl/tests/runtime/local_init.c
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/gen_local_init.c
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/ptr.res.oracle
delete mode 100644 src/plugins/e-acsl/tests/runtime/oracle/stdout.res.oracle
diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore
index dbaf48cb545..38cfd116691 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 012d174c550..3b549b22fe1 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 49ade870a78..38a48a7633b 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 00000000000..3e67d49ba6f
--- /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 00000000000..1b2e6b52d1e
--- /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 6f8dd058c2e..41e3ddedf6b 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 91fde30486f..e4c1a84ed16 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 0851deb0f63..52987f8cb85 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 57f78f5cdc0..e0a5361d268 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 d6226e87d23..139e052e16d 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 5a492da3fd4..6b57e2f2567 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 00000000000..ca9d6da56ba
--- /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 2360617faf6..124461612b9 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 00000000000..e34fffe7268
--- /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 b556402d9c0..975ef40a79f 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 b53db5cdd35..00000000000
--- 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 b3ea1b65fec..00000000000
--- 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 f8c1c0d9938..00000000000
--- 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 6636cdc4391..00000000000
--- 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 00000000000..417add7d562
--- /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 48f95d7442c..f7890eb4d14 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 7fc6c545d83..270dcdb0d84 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 9cf5edeffd7..965ff858031 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 f443fc5cbac..960337255a2 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 00000000000..daf584a9f58
--- /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 f4cfabb6990..c136f7aec42 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 c420e591edc..f7e7728886d 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 d5e052174b0..d801720f404 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 00000000000..97c5a744275
--- /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 0d697ba994d..fced089a74c 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 f74e35f0e12..9eb9554ffef 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 b7fc1a1f565..674eddac861 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 742bcfb0543..fa55190b709 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 00000000000..3e740b14f9a
--- /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 2b65e90e6d9..a6b067c83c9 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 00000000000..1dd58d9e80a
--- /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 64c906c2a81..cd7f1aa8784 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 eb7dbcce9ea..194beb0f957 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 1891087e558..32603d785fa 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 2fb5e519e75..50d32fb5962 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 77f64afba26..00000000000
--- 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 74be6cc7f5f..00000000000
--- 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 c2843c7332f..00000000000
--- 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 3dcc9b788d4..00000000000
--- 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 f4bab476073..00000000000
--- 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.
--
GitLab