diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 587c8d50c53781efe1340e2a46672b9b449418e7..42fed87564b67486c3d808583424387c26f73437 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -173,7 +173,7 @@ ifeq (@MAY_RUN_TESTS@,yes) PLUGIN_TESTS_DIRS := \ examples \ bts \ - language_constructs \ + constructs \ arith \ memory \ gmp-only \ diff --git a/src/plugins/e-acsl/tests/language_constructs/false.i b/src/plugins/e-acsl/tests/constructs/false.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/false.i rename to src/plugins/e-acsl/tests/constructs/false.i diff --git a/src/plugins/e-acsl/tests/language_constructs/function_contract.i b/src/plugins/e-acsl/tests/constructs/function_contract.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/function_contract.i rename to src/plugins/e-acsl/tests/constructs/function_contract.i diff --git a/src/plugins/e-acsl/tests/language_constructs/ghost.i b/src/plugins/e-acsl/tests/constructs/ghost.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/ghost.i rename to src/plugins/e-acsl/tests/constructs/ghost.i diff --git a/src/plugins/e-acsl/tests/language_constructs/invariant.i b/src/plugins/e-acsl/tests/constructs/invariant.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/invariant.i rename to src/plugins/e-acsl/tests/constructs/invariant.i diff --git a/src/plugins/e-acsl/tests/language_constructs/labeled_stmt.i b/src/plugins/e-acsl/tests/constructs/labeled_stmt.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/labeled_stmt.i rename to src/plugins/e-acsl/tests/constructs/labeled_stmt.i diff --git a/src/plugins/e-acsl/tests/language_constructs/lazy.i b/src/plugins/e-acsl/tests/constructs/lazy.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/lazy.i rename to src/plugins/e-acsl/tests/constructs/lazy.i diff --git a/src/plugins/e-acsl/tests/language_constructs/loop.i b/src/plugins/e-acsl/tests/constructs/loop.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/loop.i rename to src/plugins/e-acsl/tests/constructs/loop.i diff --git a/src/plugins/e-acsl/tests/language_constructs/nested_code_annot.i b/src/plugins/e-acsl/tests/constructs/nested_code_annot.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/nested_code_annot.i rename to src/plugins/e-acsl/tests/constructs/nested_code_annot.i diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/false.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/false.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/false.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/false.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/function_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/function_contract.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/function_contract.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/function_contract.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_false.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_false.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_false.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_function_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_function_contract.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_function_contract.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_ghost.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_ghost.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_ghost.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_invariant.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_invariant.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_invariant.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_labeled_stmt.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_labeled_stmt.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_labeled_stmt.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_lazy.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_lazy.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_lazy.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_loop.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_loop.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_loop.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_nested_code_annot.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_nested_code_annot.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_nested_code_annot.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_result.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_result.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_result.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_stmt_contract.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_stmt_contract.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_stmt_contract.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_true.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_true.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_true.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_typedef.c b/src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/gen_typedef.c rename to src/plugins/e-acsl/tests/constructs/oracle_ci/gen_typedef.c diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/ghost.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/ghost.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/ghost.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/ghost.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/invariant.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/invariant.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/invariant.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/invariant.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/labeled_stmt.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/labeled_stmt.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/labeled_stmt.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/lazy.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/lazy.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/lazy.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/lazy.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/loop.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/loop.res.oracle similarity index 61% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/loop.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/loop.res.oracle index db7f9a77ff5ebcbc7f5e95180bfd7bb32cf96f7a..3ddc088c016438543c25b2cfac66013881da6335 100644 --- a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/loop.res.oracle +++ b/src/plugins/e-acsl/tests/constructs/oracle_ci/loop.res.oracle @@ -1,9 +1,9 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". -[eva:alarm] tests/language_constructs/loop.i:19: Warning: +[eva:alarm] tests/constructs/loop.i:19: Warning: loop invariant got status unknown. -[eva:alarm] tests/language_constructs/loop.i:19: Warning: +[eva:alarm] tests/constructs/loop.i:19: Warning: function __e_acsl_assert: precondition got status invalid. -[eva:alarm] tests/language_constructs/loop.i:19: Warning: +[eva:alarm] tests/constructs/loop.i:19: Warning: accessing uninitialized left-value. assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]); diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/nested_code_annot.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/nested_code_annot.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/nested_code_annot.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/result.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/result.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/result.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/result.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/stmt_contract.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/stmt_contract.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/true.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/true.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/true.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/true.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_ci/typedef.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_ci/typedef.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_ci/typedef.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_ci/typedef.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/false.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/false.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/false.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/function_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/function_contract.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/function_contract.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/ghost.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/ghost.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/ghost.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/invariant.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/invariant.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/invariant.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/labeled_stmt.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/labeled_stmt.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/lazy.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/lazy.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/lazy.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/loop.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/loop.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/loop.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/nested_code_annot.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/nested_code_annot.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/result.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/result.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/result.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/stmt_contract.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/stmt_contract.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/true.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/true.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/true.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/oracle_dev/typedef.res.oracle b/src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/oracle_dev/typedef.res.oracle rename to src/plugins/e-acsl/tests/constructs/oracle_dev/typedef.res.oracle diff --git a/src/plugins/e-acsl/tests/language_constructs/result.i b/src/plugins/e-acsl/tests/constructs/result.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/result.i rename to src/plugins/e-acsl/tests/constructs/result.i diff --git a/src/plugins/e-acsl/tests/language_constructs/stmt_contract.i b/src/plugins/e-acsl/tests/constructs/stmt_contract.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/stmt_contract.i rename to src/plugins/e-acsl/tests/constructs/stmt_contract.i diff --git a/src/plugins/e-acsl/tests/language_constructs/true.i b/src/plugins/e-acsl/tests/constructs/true.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/true.i rename to src/plugins/e-acsl/tests/constructs/true.i diff --git a/src/plugins/e-acsl/tests/language_constructs/typedef.i b/src/plugins/e-acsl/tests/constructs/typedef.i similarity index 100% rename from src/plugins/e-acsl/tests/language_constructs/typedef.i rename to src/plugins/e-acsl/tests/constructs/typedef.i