From 379375a7f5b5ba2f7df601c9d6eca6babdb6bb9e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 28 Sep 2020 16:16:08 +0200
Subject: [PATCH] [aorai] split test dir in order to always launch
ltl2ba-independent tests
---
src/plugins/aorai/Makefile.in | 14 +++++++-------
src/plugins/aorai/tests/aorai/bts1289.i | 14 --------------
src/plugins/aorai/tests/aorai/formals.i | 9 ---------
.../tests/aorai/generate_assigns_bts1290.i | 9 ---------
src/plugins/aorai/tests/aorai/hoare_seq.i | 14 --------------
src/plugins/aorai/tests/aorai/not_prm.i | 7 -------
.../aorai/oracle_prove/monostate.res.oracle | 1 -
.../oracle_prove/test_factorial2.res.oracle | 4 ----
src/plugins/aorai/tests/aorai/other.c | 17 -----------------
.../aorai/tests/aorai/result_prove/.empty | 0
src/plugins/aorai/tests/aorai/seq.i | 14 --------------
src/plugins/aorai/tests/aorai/single_call.i | 5 -----
.../tests/{aorai => aorai_ltl}/call_tree.c | 0
.../tests/{aorai => aorai_ltl}/call_tree.ltl | 0
.../aorai/tests/{aorai => aorai_ltl}/goto.c | 2 +-
.../aorai/tests/{aorai => aorai_ltl}/goto.ltl | 0
.../{aorai => aorai_ltl}/oracle/goto.res.oracle | 4 ++--
.../oracle/test_boucle.res.oracle | 4 ++--
.../oracle/test_boucle1.res.oracle | 2 +-
.../oracle/test_boucle2.res.oracle | 2 +-
.../oracle/test_boucle3.res.oracle | 2 +-
.../oracle/test_factorial.res.oracle | 2 +-
.../oracle/test_recursion1.res.oracle | 8 ++++----
.../oracle/test_recursion2.0.res.oracle | 2 +-
.../oracle/test_recursion2.1.res.oracle | 2 +-
.../oracle/test_switch2.res.oracle | 6 +++---
.../oracle/test_switch3.res.oracle | 2 +-
.../oracle/test_switch3_et_recursion.res.oracle | 4 ++--
.../oracle/test_switch3_if.res.oracle | 2 +-
.../oracle/test_switch3_return.res.oracle | 2 +-
.../oracle_prove/goto.res.oracle | 4 ++--
.../oracle_prove/test_boucle.res.oracle | 4 ++--
.../oracle_prove/test_boucle1.res.oracle | 2 +-
.../oracle_prove/test_boucle2.res.oracle | 2 +-
.../oracle_prove/test_boucle3.res.oracle | 2 +-
.../oracle_prove/test_factorial.res.oracle | 4 ++++
.../oracle_prove/test_recursion1.res.oracle | 8 ++++----
.../oracle_prove/test_recursion2.0.res.oracle | 2 +-
.../oracle_prove/test_recursion2.1.res.oracle | 2 +-
.../oracle_prove/test_switch2.res.oracle | 6 +++---
.../oracle_prove/test_switch3.res.oracle | 2 +-
.../test_switch3_et_recursion.res.oracle | 4 ++--
.../oracle_prove/test_switch3_if.res.oracle | 2 +-
.../oracle_prove/test_switch3_return.res.oracle | 2 +-
.../tests/{aorai => aorai_ltl}/test_boucle.c | 2 +-
.../tests/{aorai => aorai_ltl}/test_boucle.ltl | 0
.../tests/{aorai => aorai_ltl}/test_boucle1.c | 2 +-
.../tests/{aorai => aorai_ltl}/test_boucle1.ltl | 0
.../tests/{aorai => aorai_ltl}/test_boucle2.c | 2 +-
.../tests/{aorai => aorai_ltl}/test_boucle2.ltl | 0
.../tests/{aorai => aorai_ltl}/test_boucle3.c | 2 +-
.../tests/{aorai => aorai_ltl}/test_boucle3.ltl | 0
.../tests/{aorai => aorai_ltl}/test_factorial.c | 2 +-
.../{aorai => aorai_ltl}/test_factorial.ltl | 0
.../{aorai => aorai_ltl}/test_recursion1.c | 2 +-
.../{aorai => aorai_ltl}/test_recursion1.ltl | 0
.../{aorai => aorai_ltl}/test_recursion2.c | 4 ++--
.../test_recursion2.promela | 0
.../test_recursion3.promela | 0
.../tests/{aorai => aorai_ltl}/test_switch2.c | 2 +-
.../tests/{aorai => aorai_ltl}/test_switch2.ltl | 0
.../tests/{aorai => aorai_ltl}/test_switch3.c | 2 +-
.../tests/{aorai => aorai_ltl}/test_switch3.ltl | 0
.../test_switch3_et_recursion.c | 2 +-
.../test_switch3_et_recursion.ltl | 0
.../{aorai => aorai_ltl}/test_switch3_if.c | 2 +-
.../{aorai => aorai_ltl}/test_switch3_return.c | 2 +-
.../aorai/tests/{aorai => aorai_ya}/assigns.c | 6 +++---
.../aorai/tests/{aorai => aorai_ya}/assigns.ya | 0
.../tests/{aorai => aorai_ya}/assigns_det.ya | 0
.../tests/{aorai => aorai_ya}/bts1289-2.ya | 0
src/plugins/aorai/tests/aorai_ya/bts1289.i | 14 ++++++++++++++
.../aorai/tests/{aorai => aorai_ya}/bts1289.ya | 0
.../{aorai => aorai_ya}/declared_function.i | 0
.../{aorai => aorai_ya}/declared_function.ya | 0
.../tests/{aorai => aorai_ya}/deterministic.i | 2 +-
.../tests/{aorai => aorai_ya}/deterministic.ya | 0
src/plugins/aorai/tests/aorai_ya/formals.i | 9 +++++++++
.../aorai/tests/{aorai => aorai_ya}/formals.ya | 0
.../tests/aorai_ya/generate_assigns_bts1290.i | 9 +++++++++
.../generate_assigns_bts1290.ya | 0
src/plugins/aorai/tests/aorai_ya/hoare_seq.i | 14 ++++++++++++++
.../tests/{aorai => aorai_ya}/hoare_seq.ya | 0
.../aorai/tests/{aorai => aorai_ya}/incorrect.i | 0
.../tests/{aorai => aorai_ya}/incorrect.ya | 0
.../tests/{aorai => aorai_ya}/loop_bts1050.i | 2 +-
.../tests/{aorai => aorai_ya}/loop_bts1050.ya | 0
.../aorai/tests/{aorai => aorai_ya}/monostate.i | 0
.../tests/{aorai => aorai_ya}/monostate.ya | 0
.../tests/{aorai => aorai_ya}/name_projects.ml | 0
src/plugins/aorai/tests/aorai_ya/not_prm.i | 7 +++++++
.../aorai/tests/{aorai => aorai_ya}/not_prm.ya | 0
.../oracle/assigns.0.res.oracle | 2 +-
.../oracle/assigns.1.res.oracle | 2 +-
.../oracle}/assigns.2.res.oracle | 2 +-
.../oracle/bts1289.0.res.oracle | 2 +-
.../oracle/bts1289.1.res.oracle | 2 +-
.../oracle/declared_function.res.oracle | 2 +-
.../oracle/deterministic.res.oracle | 2 +-
.../oracle/formals.res.oracle | 2 +-
.../oracle/generate_assigns_bts1290.res.oracle | 2 +-
.../oracle/hoare_seq.res.oracle | 2 +-
.../oracle/incorrect.res.oracle | 2 +-
.../oracle/loop_bts1050.res.oracle | 2 +-
.../oracle/monostate.res.oracle | 4 ++--
.../oracle/not_prm.res.oracle | 2 +-
.../{aorai => aorai_ya}/oracle/other.res.oracle | 2 +-
.../{aorai => aorai_ya}/oracle/seq.res.oracle | 2 +-
.../oracle/seq_loop.res.oracle | 2 +-
.../oracle/single_call.res.oracle | 2 +-
.../oracle/test_acces_params.res.oracle | 2 +-
.../oracle/test_acces_params2.res.oracle | 2 +-
.../test_boucle_rechercheTableau.res.oracle | 6 +++---
.../oracle/test_factorial.res.oracle} | 4 ++--
.../oracle/test_recursion4.res.oracle | 2 +-
.../oracle/test_recursion5.res.oracle | 6 +++---
.../oracle/test_struct.res.oracle | 2 +-
.../oracle_prove/assigns.0.res.oracle | 2 +-
.../oracle_prove/assigns.1.res.oracle | 2 +-
.../oracle_prove}/assigns.2.res.oracle | 2 +-
.../oracle_prove/bts1289.0.res.oracle | 2 +-
.../oracle_prove/bts1289.1.res.oracle | 2 +-
.../oracle_prove/declared_function.res.oracle | 2 +-
.../oracle_prove/deterministic.res.oracle | 2 +-
.../oracle_prove/formals.res.oracle | 2 +-
.../generate_assigns_bts1290.res.oracle | 2 +-
.../oracle_prove/hoare_seq.res.oracle | 2 +-
.../oracle_prove/incorrect.res.oracle | 2 +-
.../oracle_prove/loop_bts1050.res.oracle | 2 +-
.../aorai_ya/oracle_prove/monostate.res.oracle | 1 +
.../oracle_prove/not_prm.res.oracle | 2 +-
.../oracle_prove/other.res.oracle | 2 +-
.../oracle_prove/seq.res.oracle | 2 +-
.../oracle_prove/seq_loop.res.oracle | 2 +-
.../oracle_prove/single_call.res.oracle | 2 +-
.../oracle_prove/test_acces_params.res.oracle | 2 +-
.../oracle_prove/test_acces_params2.res.oracle | 2 +-
.../test_boucle_rechercheTableau.res.oracle | 6 +++---
.../oracle_prove/test_factorial.res.oracle | 2 +-
.../oracle_prove/test_recursion4.res.oracle | 2 +-
.../oracle_prove/test_recursion5.res.oracle | 6 +++---
.../oracle_prove/test_struct.res.oracle | 2 +-
src/plugins/aorai/tests/aorai_ya/other.c | 17 +++++++++++++++++
.../aorai/tests/{aorai => aorai_ya}/other.ya | 0
src/plugins/aorai/tests/aorai_ya/seq.i | 14 ++++++++++++++
.../aorai/tests/{aorai => aorai_ya}/seq.ya | 0
.../aorai/tests/{aorai => aorai_ya}/seq_loop.i | 2 +-
.../aorai/tests/{aorai => aorai_ya}/seq_loop.ya | 0
src/plugins/aorai/tests/aorai_ya/single_call.i | 5 +++++
.../tests/{aorai => aorai_ya}/single_call.ya | 0
.../{aorai => aorai_ya}/test_acces_params.c | 2 +-
.../{aorai => aorai_ya}/test_acces_params.ya | 0
.../{aorai => aorai_ya}/test_acces_params2.c | 2 +-
.../{aorai => aorai_ya}/test_acces_params2.ya | 0
.../test_boucle_rechercheTableau.c | 2 +-
.../test_boucle_rechercheTableau.ya | 0
.../test_factorial.c} | 2 +-
.../tests/{aorai => aorai_ya}/test_factorial.ya | 0
.../tests/{aorai => aorai_ya}/test_recursion4.c | 2 +-
.../{aorai => aorai_ya}/test_recursion4.ya | 0
.../tests/{aorai => aorai_ya}/test_recursion5.c | 2 +-
.../{aorai => aorai_ya}/test_recursion5.ya | 0
.../tests/{aorai => aorai_ya}/test_struct.c | 2 +-
.../tests/{aorai => aorai_ya}/test_struct.ya | 0
164 files changed, 230 insertions(+), 230 deletions(-)
delete mode 100644 src/plugins/aorai/tests/aorai/bts1289.i
delete mode 100644 src/plugins/aorai/tests/aorai/formals.i
delete mode 100644 src/plugins/aorai/tests/aorai/generate_assigns_bts1290.i
delete mode 100644 src/plugins/aorai/tests/aorai/hoare_seq.i
delete mode 100644 src/plugins/aorai/tests/aorai/not_prm.i
delete mode 100644 src/plugins/aorai/tests/aorai/oracle_prove/monostate.res.oracle
delete mode 100644 src/plugins/aorai/tests/aorai/oracle_prove/test_factorial2.res.oracle
delete mode 100644 src/plugins/aorai/tests/aorai/other.c
delete mode 100644 src/plugins/aorai/tests/aorai/result_prove/.empty
delete mode 100644 src/plugins/aorai/tests/aorai/seq.i
delete mode 100644 src/plugins/aorai/tests/aorai/single_call.i
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/call_tree.c (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/call_tree.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/goto.c (72%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/goto.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/goto.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_boucle.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_boucle1.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_boucle2.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_boucle3.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_factorial.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_recursion1.res.oracle (97%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_recursion2.0.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_recursion2.1.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_switch2.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_switch3.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_switch3_et_recursion.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_switch3_if.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle/test_switch3_return.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/goto.res.oracle (74%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_boucle.res.oracle (71%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_boucle1.res.oracle (83%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_boucle2.res.oracle (76%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_boucle3.res.oracle (76%)
create mode 100644 src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_recursion1.res.oracle (69%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_recursion2.0.res.oracle (79%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_recursion2.1.res.oracle (79%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_switch2.res.oracle (69%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_switch3.res.oracle (65%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_switch3_et_recursion.res.oracle (61%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_switch3_if.res.oracle (65%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/oracle_prove/test_switch3_return.res.oracle (64%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle.c (69%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle1.c (92%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle1.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle2.c (87%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle2.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle3.c (87%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_boucle3.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_factorial.c (91%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_factorial.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_recursion1.c (91%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_recursion1.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_recursion2.c (91%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_recursion2.promela (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_recursion3.promela (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch2.c (87%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch2.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch3.c (91%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch3.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch3_et_recursion.c (80%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch3_et_recursion.ltl (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch3_if.c (90%)
rename src/plugins/aorai/tests/{aorai => aorai_ltl}/test_switch3_return.c (91%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/assigns.c (50%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/assigns.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/assigns_det.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/bts1289-2.ya (100%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/bts1289.i
rename src/plugins/aorai/tests/{aorai => aorai_ya}/bts1289.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/declared_function.i (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/declared_function.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/deterministic.i (58%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/deterministic.ya (100%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/formals.i
rename src/plugins/aorai/tests/{aorai => aorai_ya}/formals.ya (100%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.i
rename src/plugins/aorai/tests/{aorai => aorai_ya}/generate_assigns_bts1290.ya (100%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/hoare_seq.i
rename src/plugins/aorai/tests/{aorai => aorai_ya}/hoare_seq.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/incorrect.i (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/incorrect.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/loop_bts1050.i (81%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/loop_bts1050.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/monostate.i (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/monostate.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/name_projects.ml (100%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/not_prm.i
rename src/plugins/aorai/tests/{aorai => aorai_ya}/not_prm.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/assigns.0.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/assigns.1.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai/oracle_prove => aorai_ya/oracle}/assigns.2.res.oracle (83%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/bts1289.0.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/bts1289.1.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/declared_function.res.oracle (97%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/deterministic.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/formals.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/generate_assigns_bts1290.res.oracle (96%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/hoare_seq.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/incorrect.res.oracle (96%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/loop_bts1050.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/monostate.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/not_prm.res.oracle (97%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/other.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/seq.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/seq_loop.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/single_call.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/test_acces_params.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/test_acces_params2.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/test_boucle_rechercheTableau.res.oracle (97%)
rename src/plugins/aorai/tests/{aorai/oracle/test_factorial2.res.oracle => aorai_ya/oracle/test_factorial.res.oracle} (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/test_recursion4.res.oracle (99%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/test_recursion5.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle/test_struct.res.oracle (98%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/assigns.0.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/assigns.1.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai/oracle => aorai_ya/oracle_prove}/assigns.2.res.oracle (83%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/bts1289.0.res.oracle (79%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/bts1289.1.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/declared_function.res.oracle (81%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/deterministic.res.oracle (66%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/formals.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/generate_assigns_bts1290.res.oracle (65%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/hoare_seq.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/incorrect.res.oracle (86%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/loop_bts1050.res.oracle (66%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/oracle_prove/monostate.res.oracle
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/not_prm.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/other.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/seq.res.oracle (68%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/seq_loop.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/single_call.res.oracle (67%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/test_acces_params.res.oracle (76%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/test_acces_params2.res.oracle (76%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/test_boucle_rechercheTableau.res.oracle (63%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/test_factorial.res.oracle (65%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/test_recursion4.res.oracle (65%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/test_recursion5.res.oracle (66%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/oracle_prove/test_struct.res.oracle (66%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/other.c
rename src/plugins/aorai/tests/{aorai => aorai_ya}/other.ya (100%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/seq.i
rename src/plugins/aorai/tests/{aorai => aorai_ya}/seq.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/seq_loop.i (58%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/seq_loop.ya (100%)
create mode 100644 src/plugins/aorai/tests/aorai_ya/single_call.i
rename src/plugins/aorai/tests/{aorai => aorai_ya}/single_call.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_acces_params.c (65%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_acces_params.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_acces_params2.c (74%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_acces_params2.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_boucle_rechercheTableau.c (79%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_boucle_rechercheTableau.ya (100%)
rename src/plugins/aorai/tests/{aorai/test_factorial2.c => aorai_ya/test_factorial.c} (89%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_factorial.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_recursion4.c (78%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_recursion4.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_recursion5.c (87%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_recursion5.ya (100%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_struct.c (56%)
rename src/plugins/aorai/tests/{aorai => aorai_ya}/test_struct.ya (100%)
diff --git a/src/plugins/aorai/Makefile.in b/src/plugins/aorai/Makefile.in
index 0e0b5764a30..5b8af2dea19 100644
--- a/src/plugins/aorai/Makefile.in
+++ b/src/plugins/aorai/Makefile.in
@@ -73,14 +73,14 @@ PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
PLUGIN_HAS_EXT_DOC:=no # [JS 2010/07/28] was 'yes'
# but prevent 'make src-distrib to work
-# if ltltoba is not present, do not attempt to run any test.
-ifneq (@HAS_LTLTOBA@,yes)
-PLUGIN_NO_TEST:=yes
-PLUGIN_NO_DEFAULT_TEST:=yes
+# aorai_ya can always be run
+PLUGIN_TESTS_DIRS:=aorai_ya
+
+ifeq (@HAS_LTLTOBA@,yes)
+PLUGIN_TESTS_DIRS+=aorai_ltl
endif
-PLUGIN_TESTS_DIRS:=aorai
-PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/Aorai_test.ml $(PLUGIN_DIR)/tests/aorai/name_projects.ml
+PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/Aorai_test.ml $(PLUGIN_DIR)/tests/aorai_ya/name_projects.ml
include $(FRAMAC_SHARE)/Makefile.dynamic
@@ -101,7 +101,7 @@ $(Aorai_DIR)/tests/test_config_prove: \
$(SED) -e 's!@AORAI_WP_SHARE@!$(AORAI_WP_SHARE)!' $< > $@
$(CHMOD_RO) $@
-Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/Aorai_test.cmxs $(Aorai_DIR)/tests/Aorai_test.cmo $(Aorai_DIR)/tests/aorai/name_projects.cmxs $(Aorai_DIR)/tests/aorai/name_projects.cmo
+Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/Aorai_test.cmxs $(Aorai_DIR)/tests/Aorai_test.cmo $(Aorai_DIR)/tests/aorai_ya/name_projects.cmxs $(Aorai_DIR)/tests/aorai_ya/name_projects.cmo
# Regenerating the Makefile on need
diff --git a/src/plugins/aorai/tests/aorai/bts1289.i b/src/plugins/aorai/tests/aorai/bts1289.i
deleted file mode 100644
index 9cf6122636b..00000000000
--- a/src/plugins/aorai/tests/aorai/bts1289.i
+++ /dev/null
@@ -1,14 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/bts1289.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata tests/aorai/bts1289-2.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- */
-
-void a(void) {}
-
-void main(void)
-{
- //@ loop assigns i;
- for (int i=0; i<10; ++i)
- a();
-}
-
diff --git a/src/plugins/aorai/tests/aorai/formals.i b/src/plugins/aorai/tests/aorai/formals.i
deleted file mode 100644
index 6ff8527a52c..00000000000
--- a/src/plugins/aorai/tests/aorai/formals.i
+++ /dev/null
@@ -1,9 +0,0 @@
-/* run.config*
-OPT: -aorai-automata tests/aorai/formals.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int f(int x) { return x; }
-
-int g(int y) { return y; }
-
-int main() { f(1); g(2); }
diff --git a/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.i b/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.i
deleted file mode 100644
index 81fb7f1a514..00000000000
--- a/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.i
+++ /dev/null
@@ -1,9 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/generate_assigns_bts1290.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- */
-void main(void)
-{
- //@ loop assigns i;
- for (int i=0; i<10; ++i)
- ;
-}
diff --git a/src/plugins/aorai/tests/aorai/hoare_seq.i b/src/plugins/aorai/tests/aorai/hoare_seq.i
deleted file mode 100644
index 39e87b49e02..00000000000
--- a/src/plugins/aorai/tests/aorai/hoare_seq.i
+++ /dev/null
@@ -1,14 +0,0 @@
-/* run.config*
-OPT: -aorai-automata tests/aorai/hoare_seq.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-void f(void) { }
-
-/*@ behavior bhv:
- assumes c > 0;
- ensures \result == 0;
-*/
-int main(int c) {
- if (c <= 0) { f (); }
- return 0;
-}
diff --git a/src/plugins/aorai/tests/aorai/not_prm.i b/src/plugins/aorai/tests/aorai/not_prm.i
deleted file mode 100644
index 3eb7b631a64..00000000000
--- a/src/plugins/aorai/tests/aorai/not_prm.i
+++ /dev/null
@@ -1,7 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/not_prm.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int f(int x) {
- return x;
-}
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/monostate.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/monostate.res.oracle
deleted file mode 100644
index fcbb126e715..00000000000
--- a/src/plugins/aorai/tests/aorai/oracle_prove/monostate.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/aorai/monostate.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial2.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial2.res.oracle
deleted file mode 100644
index 78ecfbfbfa1..00000000000
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial2.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing tests/aorai/test_factorial2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial2_0.i (no preprocessing)
-[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/other.c b/src/plugins/aorai/tests/aorai/other.c
deleted file mode 100644
index 0d0eb41b0a1..00000000000
--- a/src/plugins/aorai/tests/aorai/other.c
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/other.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int x=0;
-
-void f (void) { x=3; }
-
-void g (void) { x=4; }
-
-int main () {
- f();
- g();
- f();
- g();
- return x;
-}
diff --git a/src/plugins/aorai/tests/aorai/result_prove/.empty b/src/plugins/aorai/tests/aorai/result_prove/.empty
deleted file mode 100644
index e69de29bb2d..00000000000
diff --git a/src/plugins/aorai/tests/aorai/seq.i b/src/plugins/aorai/tests/aorai/seq.i
deleted file mode 100644
index f05fcf7bbe9..00000000000
--- a/src/plugins/aorai/tests/aorai/seq.i
+++ /dev/null
@@ -1,14 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/seq.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- */
-
-void f() { }
-
-void g() { }
-
-int main(int c) {
- if (c) f();
- g();
- if (c) g();
- return 0;
-}
diff --git a/src/plugins/aorai/tests/aorai/single_call.i b/src/plugins/aorai/tests/aorai/single_call.i
deleted file mode 100644
index 03124cf5c97..00000000000
--- a/src/plugins/aorai/tests/aorai/single_call.i
+++ /dev/null
@@ -1,5 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/single_call.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int main () {}
diff --git a/src/plugins/aorai/tests/aorai/call_tree.c b/src/plugins/aorai/tests/aorai_ltl/call_tree.c
similarity index 100%
rename from src/plugins/aorai/tests/aorai/call_tree.c
rename to src/plugins/aorai/tests/aorai_ltl/call_tree.c
diff --git a/src/plugins/aorai/tests/aorai/call_tree.ltl b/src/plugins/aorai/tests/aorai_ltl/call_tree.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/call_tree.ltl
rename to src/plugins/aorai/tests/aorai_ltl/call_tree.ltl
diff --git a/src/plugins/aorai/tests/aorai/goto.c b/src/plugins/aorai/tests/aorai_ltl/goto.c
similarity index 72%
rename from src/plugins/aorai/tests/aorai/goto.c
rename to src/plugins/aorai/tests/aorai_ltl/goto.c
index 74c4a0c9ffc..ccd31e28dbe 100644
--- a/src/plugins/aorai/tests/aorai/goto.c
+++ b/src/plugins/aorai/tests/aorai_ltl/goto.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/goto.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/goto.ltl b/src/plugins/aorai/tests/aorai_ltl/goto.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/goto.ltl
rename to src/plugins/aorai/tests/aorai_ltl/goto.ltl
diff --git a/src/plugins/aorai/tests/aorai/oracle/goto.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/goto.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
index 4fbc7da4bc8..8b7b7b0a0d8 100644
--- a/src/plugins/aorai/tests/aorai/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/goto.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/goto.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/goto.c:28: Warning:
+[aorai] tests/aorai_ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_goto_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
index 9a56e505914..d75adfbc5e5 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
@@ -1,5 +1,5 @@
-[kernel] Parsing tests/aorai/test_boucle.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/aorai/test_boucle.c:16: Warning:
+[kernel] Parsing tests/aorai_ltl/test_boucle.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/aorai_ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
index df9bd42ac26..2bf7be9ad50 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle1.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle1.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle1_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
index 22b1adb03b4..ce25f46ed9e 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
index 8b3518d3db8..4e2b603ec58 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle3_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_factorial.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
index ceb7709726c..68238aef16a 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_factorial.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
index c2bd185f136..3c998970b02 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] Parsing tests/aorai/test_recursion1.c (with preprocessing)
-[kernel] tests/aorai/test_recursion1.c:21: Warning:
+[kernel] Parsing tests/aorai_ltl/test_recursion1.c (with preprocessing)
+[kernel] tests/aorai_ltl/test_recursion1.c:21: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:42: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:42: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:54: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion1_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
index 06415a77d5f..c022dfa8dca 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
index f7476480b9e..54106258b48 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_1.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
index 81a8063b0a8..cf8da9996a6 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
@@ -1,8 +1,8 @@
-[kernel] Parsing tests/aorai/test_switch2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch2.c:34: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:34: Warning:
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
-[aorai] tests/aorai/test_switch2.c:23: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing /tmp/aorai_test_switch2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
index d21f9f44bf7..231b350ca48 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3_et_recursion.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
index 14157f96c41..3675b0bbde0 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/test_switch3_et_recursion.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_et_recursion.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch3_et_recursion.c:26: Warning:
+[aorai] tests/aorai_ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_test_switch3_et_recursion_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3_if.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
index 9f10f0b8669..6c2693aa58d 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_if.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_if.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_if_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3_return.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
index 79aae782b2d..f3a55fc5f09 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_return.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_return.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_return_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/goto.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
similarity index 74%
rename from src/plugins/aorai/tests/aorai/oracle_prove/goto.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
index 90d513137af..616ce9f0055 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/goto.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/goto.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/goto.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/goto.c:28: Warning:
+[aorai] tests/aorai_ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_goto_0.i (no preprocessing)
[wp] /tmp/aorai_goto_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
similarity index 71%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
index 1e1cc8acb14..d43ee66898a 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
@@ -1,5 +1,5 @@
-[kernel] Parsing tests/aorai/test_boucle.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/aorai/test_boucle.c:16: Warning:
+[kernel] Parsing tests/aorai_ltl/test_boucle.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/aorai_ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
similarity index 83%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
index ea51c03c119..be9bc110e5e 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle1.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle1.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle1_0.i (no preprocessing)
[wp] /tmp/aorai_test_boucle1_0.i:3: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
index c92dd0a548e..68ab6eeb39b 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle2_0.i (no preprocessing)
[wp] /tmp/aorai_test_boucle2_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
index ecc13c24f91..0da9c1d93fa 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle3_0.i (no preprocessing)
[wp] /tmp/aorai_test_boucle3_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
new file mode 100644
index 00000000000..ccb09c7d5a6
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/aorai_ltl/test_factorial.c (with preprocessing)
+[aorai] Welcome to the Aorai plugin
+[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
+[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
similarity index 69%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
index d635246be99..bbd07a1eb1d 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] Parsing tests/aorai/test_recursion1.c (with preprocessing)
-[kernel] tests/aorai/test_recursion1.c:21: Warning:
+[kernel] Parsing tests/aorai_ltl/test_recursion1.c (with preprocessing)
+[kernel] tests/aorai_ltl/test_recursion1.c:21: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:42: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:42: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:54: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion1_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
similarity index 79%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
index 1bf5237ee0b..44eb148e42a 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_0.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
similarity index 79%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
index 6782e2af71e..e6b17cbbc0b 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_1.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
similarity index 69%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
index 93f710b0f1a..697d945d96f 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
@@ -1,8 +1,8 @@
-[kernel] Parsing tests/aorai/test_switch2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch2.c:34: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:34: Warning:
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
-[aorai] tests/aorai/test_switch2.c:23: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing /tmp/aorai_test_switch2_0.i (no preprocessing)
[wp] /tmp/aorai_test_switch2_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
index 18083a07f97..bf08eea3748 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
similarity index 61%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_et_recursion.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
index f8cb4d8f765..09beb110d3a 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/test_switch3_et_recursion.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_et_recursion.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch3_et_recursion.c:26: Warning:
+[aorai] tests/aorai_ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_test_switch3_et_recursion_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_if.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_if.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
index adfb3aca7b5..87f8f5e09ae 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_if.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_if.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_if_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_return.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
similarity index 64%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_return.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
index 68bbfec82cc..79655160142 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_return.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_return.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_return_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/test_boucle.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle.c
similarity index 69%
rename from src/plugins/aorai/tests/aorai/test_boucle.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle.c
index 5da0acccb4c..72cf5e78ac9 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/*@ requires \true;
diff --git a/src/plugins/aorai/tests/aorai/test_boucle.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_boucle1.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle1.c
similarity index 92%
rename from src/plugins/aorai/tests/aorai/test_boucle1.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle1.c
index a27cc689364..0245ffedcfd 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle1.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle1.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int cpt=3;
diff --git a/src/plugins/aorai/tests/aorai/test_boucle1.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle1.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle1.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle1.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_boucle2.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle2.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_boucle2.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle2.c
index 818bf517667..9d4cf3a9aff 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle2.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle2.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/test_boucle2.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle2.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle2.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle2.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_boucle3.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle3.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_boucle3.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle3.c
index 07a59e0f525..6c93a420264 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle3.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_boucle3.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle3.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle3.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle3.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_factorial.c b/src/plugins/aorai/tests/aorai_ltl/test_factorial.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_factorial.c
rename to src/plugins/aorai/tests/aorai_ltl/test_factorial.c
index da1305fee66..6a429a55e31 100644
--- a/src/plugins/aorai/tests/aorai/test_factorial.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_factorial.ltl -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_factorial.ltl b/src/plugins/aorai/tests/aorai_ltl/test_factorial.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_factorial.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_factorial.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_recursion1.c b/src/plugins/aorai/tests/aorai_ltl/test_recursion1.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_recursion1.c
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion1.c
index 64d448142d1..ee0968101b1 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion1.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_recursion1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_recursion1.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_recursion1.ltl b/src/plugins/aorai/tests/aorai_ltl/test_recursion1.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion1.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion1.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_recursion2.c b/src/plugins/aorai/tests/aorai_ltl/test_recursion2.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_recursion2.c
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion2.c
index dcbeddd090c..a13c39b9f88 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion2.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_recursion2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -aorai-buchi tests/aorai/test_recursion2.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-buchi tests/aorai/test_recursion3.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_recursion2.promela b/src/plugins/aorai/tests/aorai_ltl/test_recursion2.promela
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion2.promela
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion2.promela
diff --git a/src/plugins/aorai/tests/aorai/test_recursion3.promela b/src/plugins/aorai/tests/aorai_ltl/test_recursion3.promela
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion3.promela
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion3.promela
diff --git a/src/plugins/aorai/tests/aorai/test_switch2.c b/src/plugins/aorai/tests/aorai_ltl/test_switch2.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_switch2.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch2.c
index 39039890d9a..f411cec23dc 100644
--- a/src/plugins/aorai/tests/aorai/test_switch2.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch2.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/test_switch2.ltl b/src/plugins/aorai/tests/aorai_ltl/test_switch2.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_switch2.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_switch2.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_switch3.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_switch3.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3.c
index dee84adec79..42e5fc6ba9a 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_switch3.ltl b/src/plugins/aorai/tests/aorai_ltl/test_switch3.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_switch3.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_et_recursion.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.c
similarity index 80%
rename from src/plugins/aorai/tests/aorai/test_switch3_et_recursion.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.c
index 34335482134..00caa9826bb 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3_et_recursion.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3_et_recursion.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_et_recursion.ltl b/src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_switch3_et_recursion.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_if.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3_if.c
similarity index 90%
rename from src/plugins/aorai/tests/aorai/test_switch3_if.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_if.c
index e9dd534a3b0..f6375d4d859 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3_if.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3_if.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_return.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3_return.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_switch3_return.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_return.c
index 6c4583363a7..a105540b982 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3_return.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3_return.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/assigns.c b/src/plugins/aorai/tests/aorai_ya/assigns.c
similarity index 50%
rename from src/plugins/aorai/tests/aorai/assigns.c
rename to src/plugins/aorai/tests/aorai_ya/assigns.c
index 15e4e3c4b54..ce6fe159678 100644
--- a/src/plugins/aorai/tests/aorai/assigns.c
+++ b/src/plugins/aorai/tests/aorai_ya/assigns.c
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/assigns.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata tests/aorai/assigns_det.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
MODULE: @PTEST_DIR@/name_projects.cmxs
- OPT: -aorai-automata tests/aorai/assigns.ya -aorai-test 1 -then -print
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -then -print
*/
int X;
diff --git a/src/plugins/aorai/tests/aorai/assigns.ya b/src/plugins/aorai/tests/aorai_ya/assigns.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/assigns.ya
rename to src/plugins/aorai/tests/aorai_ya/assigns.ya
diff --git a/src/plugins/aorai/tests/aorai/assigns_det.ya b/src/plugins/aorai/tests/aorai_ya/assigns_det.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/assigns_det.ya
rename to src/plugins/aorai/tests/aorai_ya/assigns_det.ya
diff --git a/src/plugins/aorai/tests/aorai/bts1289-2.ya b/src/plugins/aorai/tests/aorai_ya/bts1289-2.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/bts1289-2.ya
rename to src/plugins/aorai/tests/aorai_ya/bts1289-2.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/bts1289.i b/src/plugins/aorai/tests/aorai_ya/bts1289.i
new file mode 100644
index 00000000000..2c6c8f9aa59
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/bts1289.i
@@ -0,0 +1,14 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ */
+
+void a(void) {}
+
+void main(void)
+{
+ //@ loop assigns i;
+ for (int i=0; i<10; ++i)
+ a();
+}
+
diff --git a/src/plugins/aorai/tests/aorai/bts1289.ya b/src/plugins/aorai/tests/aorai_ya/bts1289.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/bts1289.ya
rename to src/plugins/aorai/tests/aorai_ya/bts1289.ya
diff --git a/src/plugins/aorai/tests/aorai/declared_function.i b/src/plugins/aorai/tests/aorai_ya/declared_function.i
similarity index 100%
rename from src/plugins/aorai/tests/aorai/declared_function.i
rename to src/plugins/aorai/tests/aorai_ya/declared_function.i
diff --git a/src/plugins/aorai/tests/aorai/declared_function.ya b/src/plugins/aorai/tests/aorai_ya/declared_function.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/declared_function.ya
rename to src/plugins/aorai/tests/aorai_ya/declared_function.ya
diff --git a/src/plugins/aorai/tests/aorai/deterministic.i b/src/plugins/aorai/tests/aorai_ya/deterministic.i
similarity index 58%
rename from src/plugins/aorai/tests/aorai/deterministic.i
rename to src/plugins/aorai/tests/aorai_ya/deterministic.i
index f0171ca436a..b92271127e2 100644
--- a/src/plugins/aorai/tests/aorai/deterministic.i
+++ b/src/plugins/aorai/tests/aorai_ya/deterministic.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/deterministic.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int X;
diff --git a/src/plugins/aorai/tests/aorai/deterministic.ya b/src/plugins/aorai/tests/aorai_ya/deterministic.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/deterministic.ya
rename to src/plugins/aorai/tests/aorai_ya/deterministic.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/formals.i b/src/plugins/aorai/tests/aorai_ya/formals.i
new file mode 100644
index 00000000000..4a32df49b67
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/formals.i
@@ -0,0 +1,9 @@
+/* run.config*
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int f(int x) { return x; }
+
+int g(int y) { return y; }
+
+int main() { f(1); g(2); }
diff --git a/src/plugins/aorai/tests/aorai/formals.ya b/src/plugins/aorai/tests/aorai_ya/formals.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/formals.ya
rename to src/plugins/aorai/tests/aorai_ya/formals.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.i b/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.i
new file mode 100644
index 00000000000..2e92796ec06
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.i
@@ -0,0 +1,9 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ */
+void main(void)
+{
+ //@ loop assigns i;
+ for (int i=0; i<10; ++i)
+ ;
+}
diff --git a/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.ya b/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/generate_assigns_bts1290.ya
rename to src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/hoare_seq.i b/src/plugins/aorai/tests/aorai_ya/hoare_seq.i
new file mode 100644
index 00000000000..cc7e1484774
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/hoare_seq.i
@@ -0,0 +1,14 @@
+/* run.config*
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+void f(void) { }
+
+/*@ behavior bhv:
+ assumes c > 0;
+ ensures \result == 0;
+*/
+int main(int c) {
+ if (c <= 0) { f (); }
+ return 0;
+}
diff --git a/src/plugins/aorai/tests/aorai/hoare_seq.ya b/src/plugins/aorai/tests/aorai_ya/hoare_seq.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/hoare_seq.ya
rename to src/plugins/aorai/tests/aorai_ya/hoare_seq.ya
diff --git a/src/plugins/aorai/tests/aorai/incorrect.i b/src/plugins/aorai/tests/aorai_ya/incorrect.i
similarity index 100%
rename from src/plugins/aorai/tests/aorai/incorrect.i
rename to src/plugins/aorai/tests/aorai_ya/incorrect.i
diff --git a/src/plugins/aorai/tests/aorai/incorrect.ya b/src/plugins/aorai/tests/aorai_ya/incorrect.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/incorrect.ya
rename to src/plugins/aorai/tests/aorai_ya/incorrect.ya
diff --git a/src/plugins/aorai/tests/aorai/loop_bts1050.i b/src/plugins/aorai/tests/aorai_ya/loop_bts1050.i
similarity index 81%
rename from src/plugins/aorai/tests/aorai/loop_bts1050.i
rename to src/plugins/aorai/tests/aorai_ya/loop_bts1050.i
index 73fd922002a..fdec741b7b3 100644
--- a/src/plugins/aorai/tests/aorai/loop_bts1050.i
+++ b/src/plugins/aorai/tests/aorai_ya/loop_bts1050.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/loop_bts1050.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(){};
diff --git a/src/plugins/aorai/tests/aorai/loop_bts1050.ya b/src/plugins/aorai/tests/aorai_ya/loop_bts1050.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/loop_bts1050.ya
rename to src/plugins/aorai/tests/aorai_ya/loop_bts1050.ya
diff --git a/src/plugins/aorai/tests/aorai/monostate.i b/src/plugins/aorai/tests/aorai_ya/monostate.i
similarity index 100%
rename from src/plugins/aorai/tests/aorai/monostate.i
rename to src/plugins/aorai/tests/aorai_ya/monostate.i
diff --git a/src/plugins/aorai/tests/aorai/monostate.ya b/src/plugins/aorai/tests/aorai_ya/monostate.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/monostate.ya
rename to src/plugins/aorai/tests/aorai_ya/monostate.ya
diff --git a/src/plugins/aorai/tests/aorai/name_projects.ml b/src/plugins/aorai/tests/aorai_ya/name_projects.ml
similarity index 100%
rename from src/plugins/aorai/tests/aorai/name_projects.ml
rename to src/plugins/aorai/tests/aorai_ya/name_projects.ml
diff --git a/src/plugins/aorai/tests/aorai_ya/not_prm.i b/src/plugins/aorai/tests/aorai_ya/not_prm.i
new file mode 100644
index 00000000000..d96e123d6e6
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/not_prm.i
@@ -0,0 +1,7 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int f(int x) {
+ return x;
+}
diff --git a/src/plugins/aorai/tests/aorai/not_prm.ya b/src/plugins/aorai/tests/aorai_ya/not_prm.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/not_prm.ya
rename to src/plugins/aorai/tests/aorai_ya/not_prm.ya
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
index 587631cdbf4..5c7443d37ab 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
index c6501e5664e..01876080d5c 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_1.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.2.res.oracle
similarity index 83%
rename from src/plugins/aorai/tests/aorai/oracle_prove/assigns.2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/assigns.2.res.oracle
index a03928c6cad..a88a5548285 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
/* Generated by Frama-C */
int X;
diff --git a/src/plugins/aorai/tests/aorai/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/bts1289.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
index a313805caf4..3dea38d70a1 100644
--- a/src/plugins/aorai/tests/aorai/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/bts1289.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
index 0e1b58e415e..5f22740b638 100644
--- a/src/plugins/aorai/tests/aorai/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_bts1289_1.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
index 7b00c3f64fe..fbeda724d70 100644
--- a/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/declared_function.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/declared_function.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_declared_function_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
index 03ffe79dc58..c4a89c4951e 100644
--- a/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/deterministic.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/deterministic.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_deterministic_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
index 55923d34f28..c2bd9a6d566 100644
--- a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/formals.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/formals.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_formals_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
similarity index 96%
rename from src/plugins/aorai/tests/aorai/oracle/generate_assigns_bts1290.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
index f822ad621a1..3d7e763902c 100644
--- a/src/plugins/aorai/tests/aorai/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/generate_assigns_bts1290.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/generate_assigns_bts1290.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_generate_assigns_bts1290_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
index c420dac4bde..546c4e7d846 100644
--- a/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/hoare_seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/hoare_seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_hoare_seq_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
similarity index 96%
rename from src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
index 62b6e9a75cc..6a56d3e182e 100644
--- a/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/incorrect.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/incorrect.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_incorrect_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
index be1dc66d50a..c0ad530b635 100644
--- a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/loop_bts1050.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/loop_bts1050.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
index 678af350fd7..4e83e52e08b 100644
--- a/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/monostate.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/monostate.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] tests/aorai/monostate.i:8: Warning:
+[aorai] tests/aorai_ya/monostate.i:8: Warning:
Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing /tmp/aorai_monostate_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/not_prm.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
index f8d92a9b563..6455cd141e5 100644
--- a/src/plugins/aorai/tests/aorai/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/not_prm.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/not_prm.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_not_prm_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/other.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
index ad7f48504f1..1b70959421e 100644
--- a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/other.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/other.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_other_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
index a5cacc4f933..6d3bd0b4fd9 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
index ee365599dac..37a5942b8e5 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq_loop.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq_loop.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/single_call.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/single_call.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
index d93f86515a7..89cfcb8ea82 100644
--- a/src/plugins/aorai/tests/aorai/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/single_call.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/single_call.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_single_call_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_acces_params.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
index ad696afccfd..6920ad16262 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_acces_params2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
index 49f7c5b25ad..9899759571f 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle_rechercheTableau.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
index 49a1be8807f..c65e202d5f6 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_boucle_rechercheTableau.c (with preprocessing)
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:17: Warning:
+[kernel] Parsing tests/aorai_ya/test_boucle_rechercheTableau.c (with preprocessing)
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:17: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:7: Warning:
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_factorial2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_factorial2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
index 68c37c23c9c..2db6fe590f8 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_factorial2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/test_factorial2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial2_0.i (no preprocessing)
+[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_decode_int = 2,
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion4.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
index 3a5c6d38077..8a7f6b37521 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion4.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_recursion4.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion4_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion5.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
index 8bc2cd519af..f4f409b2231 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_recursion5.c (with preprocessing)
-[kernel] tests/aorai/test_recursion5.c:12: Warning:
+[kernel] Parsing tests/aorai_ya/test_recursion5.c (with preprocessing)
+[kernel] tests/aorai_ya/test_recursion5.c:12: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion5.c:28: Warning:
+[kernel] tests/aorai_ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion5_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_struct.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
index e03f8265240..48449b62e49 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_struct.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_struct.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_struct_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/assigns.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
index 5aec8b21daa..3bdcb7f459f 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/assigns.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
index 49feab1f711..64a6a02b043 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.2.res.oracle
similarity index 83%
rename from src/plugins/aorai/tests/aorai/oracle/assigns.2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.2.res.oracle
index a03928c6cad..a88a5548285 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
/* Generated by Frama-C */
int X;
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
similarity index 79%
rename from src/plugins/aorai/tests/aorai/oracle_prove/bts1289.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
index 43d8b12fc49..84559a6dd0e 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/bts1289.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
index f8cbd2cb00c..67505dcb5c5 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_bts1289_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
similarity index 81%
rename from src/plugins/aorai/tests/aorai/oracle_prove/declared_function.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
index a648f24de41..7b836a362ab 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/declared_function.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/declared_function.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_declared_function_0.i (no preprocessing)
[kernel:annot:missing-spec] /tmp/aorai_declared_function_0.i:48: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/deterministic.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/deterministic.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
index 24fb75961ac..40255d6fc4b 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/deterministic.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/deterministic.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_deterministic_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/formals.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/formals.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
index 909b386d342..b7c2460da5e 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/formals.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/formals.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_formals_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/generate_assigns_bts1290.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
index cbb069f8f76..e402347bb7f 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/generate_assigns_bts1290.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/generate_assigns_bts1290.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_generate_assigns_bts1290_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
index 2270c4bc398..fb6a559a080 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/hoare_seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/hoare_seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_hoare_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
similarity index 86%
rename from src/plugins/aorai/tests/aorai/oracle_prove/incorrect.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
index b981ababa88..5d37997bb66 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/incorrect.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/incorrect.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_incorrect_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
index 92104920d5c..2aa37b76715 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/loop_bts1050.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/loop_bts1050.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/monostate.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/monostate.res.oracle
new file mode 100644
index 00000000000..204c70d4860
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/monostate.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/aorai_ya/monostate.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/not_prm.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/not_prm.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
index 01011d01c1f..1b02aa00afd 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/not_prm.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/not_prm.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_not_prm_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/other.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/other.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
index 1d337862216..e0b3215a1bc 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/other.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/other.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_other_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
similarity index 68%
rename from src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
index ab5514b69d2..bb5f9ad8f3e 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
index 64b2e8b3540..c9b971ff32f 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq_loop.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq_loop.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/single_call.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/single_call.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
index 705c6f7085c..7e325174854 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/single_call.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/single_call.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/single_call.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_single_call_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
index 006ec0acdd2..eaa6a845adf 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params_0.i (no preprocessing)
[wp] /tmp/aorai_test_acces_params_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
index c5b2f97589b..dcd88018b20 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params2_0.i (no preprocessing)
[wp] /tmp/aorai_test_acces_params2_0.i:3: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
similarity index 63%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle_rechercheTableau.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
index 6a9fc826a87..c64d82f7057 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_boucle_rechercheTableau.c (with preprocessing)
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:17: Warning:
+[kernel] Parsing tests/aorai_ya/test_boucle_rechercheTableau.c (with preprocessing)
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:17: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:7: Warning:
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_factorial.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
index 999cb771ba7..4265d80c2eb 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_factorial.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion4.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion4.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
index 2cb6a23598f..6293804566c 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion4.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_recursion4.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion4_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion5.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion5.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
index d9337988b69..db107f75b48 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_recursion5.c (with preprocessing)
-[kernel] tests/aorai/test_recursion5.c:12: Warning:
+[kernel] Parsing tests/aorai_ya/test_recursion5.c (with preprocessing)
+[kernel] tests/aorai_ya/test_recursion5.c:12: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion5.c:28: Warning:
+[kernel] tests/aorai_ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion5_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_struct.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_struct.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
index 60ed3fef31e..6571fc60e01 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_struct.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_struct.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_struct_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/other.c b/src/plugins/aorai/tests/aorai_ya/other.c
new file mode 100644
index 00000000000..4e13872dbf2
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/other.c
@@ -0,0 +1,17 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int x=0;
+
+void f (void) { x=3; }
+
+void g (void) { x=4; }
+
+int main () {
+ f();
+ g();
+ f();
+ g();
+ return x;
+}
diff --git a/src/plugins/aorai/tests/aorai/other.ya b/src/plugins/aorai/tests/aorai_ya/other.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/other.ya
rename to src/plugins/aorai/tests/aorai_ya/other.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/seq.i b/src/plugins/aorai/tests/aorai_ya/seq.i
new file mode 100644
index 00000000000..f573a5491b3
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/seq.i
@@ -0,0 +1,14 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ */
+
+void f() { }
+
+void g() { }
+
+int main(int c) {
+ if (c) f();
+ g();
+ if (c) g();
+ return 0;
+}
diff --git a/src/plugins/aorai/tests/aorai/seq.ya b/src/plugins/aorai/tests/aorai_ya/seq.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/seq.ya
rename to src/plugins/aorai/tests/aorai_ya/seq.ya
diff --git a/src/plugins/aorai/tests/aorai/seq_loop.i b/src/plugins/aorai/tests/aorai_ya/seq_loop.i
similarity index 58%
rename from src/plugins/aorai/tests/aorai/seq_loop.i
rename to src/plugins/aorai/tests/aorai_ya/seq_loop.i
index 0d85eb80cc3..07cc7cf2a9b 100644
--- a/src/plugins/aorai/tests/aorai/seq_loop.i
+++ b/src/plugins/aorai/tests/aorai_ya/seq_loop.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/seq_loop.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() {}
diff --git a/src/plugins/aorai/tests/aorai/seq_loop.ya b/src/plugins/aorai/tests/aorai_ya/seq_loop.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/seq_loop.ya
rename to src/plugins/aorai/tests/aorai_ya/seq_loop.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/single_call.i b/src/plugins/aorai/tests/aorai_ya/single_call.i
new file mode 100644
index 00000000000..257ce2b2c7a
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/single_call.i
@@ -0,0 +1,5 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int main () {}
diff --git a/src/plugins/aorai/tests/aorai/single_call.ya b/src/plugins/aorai/tests/aorai_ya/single_call.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/single_call.ya
rename to src/plugins/aorai/tests/aorai_ya/single_call.ya
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params.c b/src/plugins/aorai/tests/aorai_ya/test_acces_params.c
similarity index 65%
rename from src/plugins/aorai/tests/aorai/test_acces_params.c
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params.c
index 3961685e428..884140ce9ca 100644
--- a/src/plugins/aorai/tests/aorai/test_acces_params.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_acces_params.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_acces_params.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params.ya b/src/plugins/aorai/tests/aorai_ya/test_acces_params.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_acces_params.ya
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params.ya
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params2.c b/src/plugins/aorai/tests/aorai_ya/test_acces_params2.c
similarity index 74%
rename from src/plugins/aorai/tests/aorai/test_acces_params2.c
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params2.c
index df66a09f957..86092179e3f 100644
--- a/src/plugins/aorai/tests/aorai/test_acces_params2.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_acces_params2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_acces_params2.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params2.ya b/src/plugins/aorai/tests/aorai_ya/test_acces_params2.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_acces_params2.ya
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params2.ya
diff --git a/src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.c b/src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.c
similarity index 79%
rename from src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.c
rename to src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.c
index 250ba9f88e3..7dcf436cfe3 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_boucle_rechercheTableau.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.ya b/src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.ya
rename to src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.ya
diff --git a/src/plugins/aorai/tests/aorai/test_factorial2.c b/src/plugins/aorai/tests/aorai_ya/test_factorial.c
similarity index 89%
rename from src/plugins/aorai/tests/aorai/test_factorial2.c
rename to src/plugins/aorai/tests/aorai_ya/test_factorial.c
index 691ac292312..9cb2213b68d 100644
--- a/src/plugins/aorai/tests/aorai/test_factorial2.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_factorial.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_factorial.ya b/src/plugins/aorai/tests/aorai_ya/test_factorial.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_factorial.ya
rename to src/plugins/aorai/tests/aorai_ya/test_factorial.ya
diff --git a/src/plugins/aorai/tests/aorai/test_recursion4.c b/src/plugins/aorai/tests/aorai_ya/test_recursion4.c
similarity index 78%
rename from src/plugins/aorai/tests/aorai/test_recursion4.c
rename to src/plugins/aorai/tests/aorai_ya/test_recursion4.c
index b04d4b88ab2..cf4c5d8523a 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion4.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_recursion4.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_recursion4.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
# pragma JessieIntegerModel(math)
diff --git a/src/plugins/aorai/tests/aorai/test_recursion4.ya b/src/plugins/aorai/tests/aorai_ya/test_recursion4.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion4.ya
rename to src/plugins/aorai/tests/aorai_ya/test_recursion4.ya
diff --git a/src/plugins/aorai/tests/aorai/test_recursion5.c b/src/plugins/aorai/tests/aorai_ya/test_recursion5.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_recursion5.c
rename to src/plugins/aorai/tests/aorai_ya/test_recursion5.c
index 00dc4c63e2e..241030e7112 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion5.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_recursion5.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_recursion5.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_recursion5.ya b/src/plugins/aorai/tests/aorai_ya/test_recursion5.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion5.ya
rename to src/plugins/aorai/tests/aorai_ya/test_recursion5.ya
diff --git a/src/plugins/aorai/tests/aorai/test_struct.c b/src/plugins/aorai/tests/aorai_ya/test_struct.c
similarity index 56%
rename from src/plugins/aorai/tests/aorai/test_struct.c
rename to src/plugins/aorai/tests/aorai_ya/test_struct.c
index 552c7cdb3ec..1b8ff3ec2ff 100644
--- a/src/plugins/aorai/tests/aorai/test_struct.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_struct.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_struct.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
struct People{
diff --git a/src/plugins/aorai/tests/aorai/test_struct.ya b/src/plugins/aorai/tests/aorai_ya/test_struct.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_struct.ya
rename to src/plugins/aorai/tests/aorai_ya/test_struct.ya
--
GitLab