diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c
index 8cbd56c0842494483bbbf423b8f28eeb7853a751..2194b9d07f19720dc26a6c04cded5604ed96f594 100644
--- a/src/plugins/aorai/tests/ltl/goto.c
+++ b/src/plugins/aorai/tests/ltl/goto.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle.c b/src/plugins/aorai/tests/ltl/test_boucle.c
index db2f6bc0c3f18408ea163acbdaacffdaaeac8ac3..a56440535d6e6e93fc9accea8002742822e28c85 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/*@ requires \true;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle1.c b/src/plugins/aorai/tests/ltl/test_boucle1.c
index 7b091c51b7614a411c3afdb521561a4785ffcf16..b0777d84eef44897ac6fb39e07fa0891a484911d 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle1.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int cpt=3;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle2.c b/src/plugins/aorai/tests/ltl/test_boucle2.c
index 8aa77e6f8b0589e2f53869d76fb00adba6abd76a..3babc406ceb416fe250d5bd22ba8c9802ca6b885 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle2.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle3.c b/src/plugins/aorai/tests/ltl/test_boucle3.c
index 6da17de07b287db5befa2b3bcd350672f128f03d..70118bf9196129a005f73f79e2ffa9191202462e 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle3.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_factorial.c b/src/plugins/aorai/tests/ltl/test_factorial.c
index 0ad6476002658f8a1bedc42146f14f3229b42427..8957c6eaba34bfa772bfe7ba3d9ddb69aa7a31c9 100644
--- a/src/plugins/aorai/tests/ltl/test_factorial.c
+++ b/src/plugins/aorai/tests/ltl/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion1.c b/src/plugins/aorai/tests/ltl/test_recursion1.c
index 14be685a47bcdfbaf534712834e6a69acc2de9fb..a3d4218b6a75cbde51796d0cda3efb819223d258 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion1.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c
index 7d93ab3fa3a3e28e205517b56bc795ad2b427ebf..4053c83792c943b37a32bf67cd97331d0ff216ef 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion2.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-acceptance -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/ltl/test_switch2.c b/src/plugins/aorai/tests/ltl/test_switch2.c
index 2bb7284fbbd78e3c7d6455efbceaac54213338b6..a9d42339d7934d2c81006e4c284adf36de8b6c31 100644
--- a/src/plugins/aorai/tests/ltl/test_switch2.c
+++ b/src/plugins/aorai/tests/ltl/test_switch2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_switch3.c b/src/plugins/aorai/tests/ltl/test_switch3.c
index 5d9e8582f493e3d9d10f5343e8eeff8e4897b048..78866e16d205ef3a4438779a790c18f8d69a999d 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -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/ltl/test_switch3_et_recursion.c b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
index 352725ef98403e943292dd701851020dd9450331..4d3d0d7cd0c875938e365e08c25546516d926ee7 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -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/ltl/test_switch3_if.c b/src/plugins/aorai/tests/ltl/test_switch3_if.c
index 93dd122636eb69e79de4ed04781fa4528a261027..77e6d89fb0e13d46cb42dc53a4f350703aaa27e9 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_if.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_if.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -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/ltl/test_switch3_return.c b/src/plugins/aorai/tests/ltl/test_switch3_return.c
index 8df70979968ab549179cf70011105ac4083f0001..0835dfd7f17e661398f7f32544650cde2af8d012 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_return.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_return.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-acceptance -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/test_config b/src/plugins/aorai/tests/test_config
index c8feb6120b561b4eb45efc918a4a79b4f992de3d..2a1eb0b9ab01a34ec544c6bbee48aa0751367b68 100644
--- a/src/plugins/aorai/tests/test_config
+++ b/src/plugins/aorai/tests/test_config
@@ -1,5 +1,8 @@
PLUGIN: aorai eva,from,scope report wp,rtegen
+COMMENT: Path to the library from the test file
+LIBS: ../Aorai_test
+
COMMENT: work around to allow the loading of the aorai_test lib
MACRO: PTEST_DEFAULT_OPTIONS -check -journal-disable
diff --git a/src/plugins/aorai/tests/test_config_prove.in b/src/plugins/aorai/tests/test_config_prove.in
index 2e96488c0c4f976ca795877722a23d9fe8f139ef..6f7530d8bebfbaaa4868bd98cb086ce09d7d1c5d 100644
--- a/src/plugins/aorai/tests/test_config_prove.in
+++ b/src/plugins/aorai/tests/test_config_prove.in
@@ -1,5 +1,8 @@
PLUGIN: aorai eva,from,scope report wp,rtegen
+COMMENT: Path to the library from the test file
+LIBS: ../Aorai_test
+
COMMENT: work around to allow the loading of the aorai_test lib
MACRO: PTEST_DEFAULT_OPTIONS -check -journal-disable
diff --git a/src/plugins/aorai/tests/ya/aorai_ptr_field.i b/src/plugins/aorai/tests/ya/aorai_ptr_field.i
index 24c8ffc30a7231b26a8e6febc12d553b1c2a39f3..2d543c276252230fbac9b7f809c4f9a8a8088a65 100644
--- a/src/plugins/aorai/tests/ya/aorai_ptr_field.i
+++ b/src/plugins/aorai/tests/ya/aorai_ptr_field.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
struct S { int x; };
diff --git a/src/plugins/aorai/tests/ya/assigns.c b/src/plugins/aorai/tests/ya/assigns.c
index 0e1c52123e21895c27435d990845fc0d5bfb3cf1..0a7a6cf91977e1bcb753d88be504da18865fe491 100644
--- a/src/plugins/aorai/tests/ya/assigns.c
+++ b/src/plugins/aorai/tests/ya/assigns.c
@@ -1,10 +1,10 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
MODULE: name_projects
+ LIBS:
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -then -print
*/
-
int X;
void f(void) { X++; }
diff --git a/src/plugins/aorai/tests/ya/bts1289.i b/src/plugins/aorai/tests/ya/bts1289.i
index 93cf50233c6de580a502d09ec0ebb9e0710a3fd4..4275cbc2ed34efdfff5758ee51b3674f69db7cd9 100644
--- a/src/plugins/aorai/tests/ya/bts1289.i
+++ b/src/plugins/aorai/tests/ya/bts1289.i
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void a(void) {}
diff --git a/src/plugins/aorai/tests/ya/declared_function.i b/src/plugins/aorai/tests/ya/declared_function.i
index 12f50538eb389c40452004dcae442b80e72800c5..0ec1fc04fbd007eedb740b539bd9eba427e85b8c 100644
--- a/src/plugins/aorai/tests/ya/declared_function.i
+++ b/src/plugins/aorai/tests/ya/declared_function.i
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(void);
diff --git a/src/plugins/aorai/tests/ya/deterministic.i b/src/plugins/aorai/tests/ya/deterministic.i
index d892d8913785cf908250be51ee907aea92bd59fe..af544b32ecbded109571cc925fe12dbaf06ad12e 100644
--- a/src/plugins/aorai/tests/ya/deterministic.i
+++ b/src/plugins/aorai/tests/ya/deterministic.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int X;
diff --git a/src/plugins/aorai/tests/ya/formals.i b/src/plugins/aorai/tests/ya/formals.i
index a463e4f7d372e66081bacb8a83c6c1fbc799a62e..7339298dade9d1a44e608bd10f8cdb9810a761b1 100644
--- a/src/plugins/aorai/tests/ya/formals.i
+++ b/src/plugins/aorai/tests/ya/formals.i
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(int x) { return x; }
diff --git a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
index d9333d415f6a9e4a266b9b4e4ee0fffb0157aeec..698e1549a526e24aaf660de1269c53af83a58c8b 100644
--- a/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
+++ b/src/plugins/aorai/tests/ya/generate_assigns_bts1290.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(void)
{
diff --git a/src/plugins/aorai/tests/ya/hoare_seq.i b/src/plugins/aorai/tests/ya/hoare_seq.i
index b60ae6082da68af639a7419bd7b8fcc06c1dbfcc..be7428a41e3c3ef59275d627f79ab581289dcda1 100644
--- a/src/plugins/aorai/tests/ya/hoare_seq.i
+++ b/src/plugins/aorai/tests/ya/hoare_seq.i
@@ -1,5 +1,5 @@
/* run.config*
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(void) { }
diff --git a/src/plugins/aorai/tests/ya/incorrect.i b/src/plugins/aorai/tests/ya/incorrect.i
index 01f702808601302f85949d38f64b69b4f79c8ab7..36dc2f005ae4865a67a59bcd3da3afff58da9854 100644
--- a/src/plugins/aorai/tests/ya/incorrect.i
+++ b/src/plugins/aorai/tests/ya/incorrect.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(void);
diff --git a/src/plugins/aorai/tests/ya/logical_operators.i b/src/plugins/aorai/tests/ya/logical_operators.i
index 1dcbba59346f608a433691d0d549058a6d6a22f8..12b25974ec2567d526869ec71462f45b65052bc6 100644
--- a/src/plugins/aorai/tests/ya/logical_operators.i
+++ b/src/plugins/aorai/tests/ya/logical_operators.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
diff --git a/src/plugins/aorai/tests/ya/loop_bts1050.i b/src/plugins/aorai/tests/ya/loop_bts1050.i
index 86fe369e9f793b991fd0e3f4510b1ea5111b1c55..bb697cf3e49a862996f28a3d6169c19afc4d0b27 100644
--- a/src/plugins/aorai/tests/ya/loop_bts1050.i
+++ b/src/plugins/aorai/tests/ya/loop_bts1050.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(){};
diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
index ac025ee303230685e01374351f91c3365307ff76..56daa093e4eac7ecbd0e4526f4f5f2b78101d49a 100644
--- a/src/plugins/aorai/tests/ya/metavariables-incompatible.i
+++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
@@ -1,5 +1,5 @@
/* run.config*
EXIT: 1
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(void) {}
diff --git a/src/plugins/aorai/tests/ya/metavariables-right.i b/src/plugins/aorai/tests/ya/metavariables-right.i
index 9d88e67323f1579b8cb9ff96e0713ab2652fbb67..0be9f13ce1be8173b0ba9d32ffcb5bdf732bbce5 100644
--- a/src/plugins/aorai/tests/ya/metavariables-right.i
+++ b/src/plugins/aorai/tests/ya/metavariables-right.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.i b/src/plugins/aorai/tests/ya/metavariables-wrong.i
index febfd16cb34647a707de1a733cc9e0e9afd9fd5b..23c49ad215000fad152c304b543748fcb92e669a 100644
--- a/src/plugins/aorai/tests/ya/metavariables-wrong.i
+++ b/src/plugins/aorai/tests/ya/metavariables-wrong.i
@@ -1,6 +1,6 @@
/* run.config*
EXIT: 1
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(int x) {}
void g(void) {}
diff --git a/src/plugins/aorai/tests/ya/monostate.i b/src/plugins/aorai/tests/ya/monostate.i
index 0d72d9a431caaf166b2bcdbf4cdbceca3e231244..42e221ff638c60daf9e591c3673ad650368fe82e 100644
--- a/src/plugins/aorai/tests/ya/monostate.i
+++ b/src/plugins/aorai/tests/ya/monostate.i
@@ -1,5 +1,5 @@
/* run.config
-OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(void) {}
diff --git a/src/plugins/aorai/tests/ya/not_prm.i b/src/plugins/aorai/tests/ya/not_prm.i
index 8b5c4281608d86fbed207d2f056fcb22f6513953..e1133d9675a662c6c3841ccdb416808d8712e1c3 100644
--- a/src/plugins/aorai/tests/ya/not_prm.i
+++ b/src/plugins/aorai/tests/ya/not_prm.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int f(int x) {
diff --git a/src/plugins/aorai/tests/ya/other.c b/src/plugins/aorai/tests/ya/other.c
index c4977e2a37d1bd55cf58ded7ffe03019fe0d6f5e..f395044d9538be9ac80ec6a176fa47061422d23a 100644
--- a/src/plugins/aorai/tests/ya/other.c
+++ b/src/plugins/aorai/tests/ya/other.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int x=0;
diff --git a/src/plugins/aorai/tests/ya/saveload.i b/src/plugins/aorai/tests/ya/saveload.i
index 2ac81c70606919b6ed14b3588faf41d0cb926659..f7fc1cf0ab6f5e12b6ba406495a38facedd3d4ce 100644
--- a/src/plugins/aorai/tests/ya/saveload.i
+++ b/src/plugins/aorai/tests/ya/saveload.i
@@ -1,12 +1,12 @@
/* run.config
NOFRAMAC:
+LIBS:
EXECNOW: LOG @PTEST_NAME@.res.0.log.txt BIN @PTEST_NAME@.sav @frama-c@ -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya @PTEST_FILE@ -save @PTEST_DIR@/result/@PTEST_NAME@.sav > @PTEST_DIR@/result/@PTEST_NAME@.res.0.log.txt
EXECNOW: LOG @PTEST_NAME@.res.1.log.txt @frama-c@ -load @PTEST_DIR@/result/@PTEST_NAME@.sav -then-on aorai -eva > @PTEST_DIR@/result/@PTEST_NAME@.res.1.log.txt
*/
/* run.config_prove
DONTRUN:
*/
-
void f () { }
int main () {
diff --git a/src/plugins/aorai/tests/ya/seq.i b/src/plugins/aorai/tests/ya/seq.i
index 1ba54569e1265a39feb5116465e75c7547c1fb61..96c875ed9bd51bce7df936007eda10fed4d5e13e 100644
--- a/src/plugins/aorai/tests/ya/seq.i
+++ b/src/plugins/aorai/tests/ya/seq.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() { }
diff --git a/src/plugins/aorai/tests/ya/seq_loop.i b/src/plugins/aorai/tests/ya/seq_loop.i
index bee4d37d3cf6133cb65ca4bb52f1beb98e427bbb..ff634f0b1de6895ff941239f781d14e49c854771 100644
--- a/src/plugins/aorai/tests/ya/seq_loop.i
+++ b/src/plugins/aorai/tests/ya/seq_loop.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() {}
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 9efe13a270bb6d0f69b7ec73c1522c4daf3c465e..e1aa4af00491ad5f5772d62fe0ca43bb33ecb30b 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -1,8 +1,8 @@
/* run.config
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-smoke-tests -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-smoke-tests -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance -aorai-instrumentation-history 2 -aorai-no-generate-annotations -aorai-no-generate-deterministic-lemmas -then-last -eva -eva-partition-value n -eva-ilevel 256
*/
/* run.config_prove
-OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -load-module tests/Aorai_test.cmxs -aorai-smoke-tests -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
+OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata @PTEST_DIR@/@PTEST_NAME@_wp.ya -aorai-smoke-tests -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
*/
#include "__fc_builtin.h"
diff --git a/src/plugins/aorai/tests/ya/single_call.i b/src/plugins/aorai/tests/ya/single_call.i
index 51abf5a7ef33870f78f6a029de9e3ebbb3330e69..015593d0f1fd2982d3dac34fba5bf407e7557b44 100644
--- a/src/plugins/aorai/tests/ya/single_call.i
+++ b/src/plugins/aorai/tests/ya/single_call.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int main () {}
diff --git a/src/plugins/aorai/tests/ya/singleassignment-right.i b/src/plugins/aorai/tests/ya/singleassignment-right.i
index 4c5612f51075bcfe936814e8492beb88f67935c4..8d16f793ff23947bc17f2a975e0dbc168b645022 100644
--- a/src/plugins/aorai/tests/ya/singleassignment-right.i
+++ b/src/plugins/aorai/tests/ya/singleassignment-right.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void main(int *x, int *y)
diff --git a/src/plugins/aorai/tests/ya/singleassignment-wrong.i b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
index baa7b42e03eacd67ca4225cae17413023786a2e0..3c61f3cb9e5ffc128a6056c13adeaa05b8c249f6 100644
--- a/src/plugins/aorai/tests/ya/singleassignment-wrong.i
+++ b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
@@ -1,6 +1,6 @@
/* run.config*
EXIT: 1
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int main(int x)
{
diff --git a/src/plugins/aorai/tests/ya/stack.i b/src/plugins/aorai/tests/ya/stack.i
index d911301c6860deccbbf88ee8e2cecaf097232e3a..da30e1597e8d9232c7fad177f0bedcc4f24abec3 100644
--- a/src/plugins/aorai/tests/ya/stack.i
+++ b/src/plugins/aorai/tests/ya/stack.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_acces_params.c b/src/plugins/aorai/tests/ya/test_acces_params.c
index dc673f9bc593429faf4c8cadd396389fa5c115a7..3f7e08b1469bd631fea60bf591146e808e7099aa 100644
--- a/src/plugins/aorai/tests/ya/test_acces_params.c
+++ b/src/plugins/aorai/tests/ya/test_acces_params.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ya/test_acces_params2.c b/src/plugins/aorai/tests/ya/test_acces_params2.c
index 7f25f23facbb6f7de9782534fb2dc42e0e0515f0..597bd15931e8e0ab5ded73f9c40ab88a42592521 100644
--- a/src/plugins/aorai/tests/ya/test_acces_params2.c
+++ b/src/plugins/aorai/tests/ya/test_acces_params2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
index da220198440138b3924dddc99a92b9ea53794f5d..413b72d10ed4843d36ee08a6936a721e9d1e8b8e 100644
--- a/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
+++ b/src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_factorial.c b/src/plugins/aorai/tests/ya/test_factorial.c
index fbb9762854cd43b3ef4c17245f2919486f58d4b8..87864af429ec3a84d1ecf52243da37193f6a43c2 100644
--- a/src/plugins/aorai/tests/ya/test_factorial.c
+++ b/src/plugins/aorai/tests/ya/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_recursion4.c b/src/plugins/aorai/tests/ya/test_recursion4.c
index e88b8471fb74d57f267b879b89fe4b2c3bdc803a..679c02692264b35ca08fef9b478577cdf67e726e 100644
--- a/src/plugins/aorai/tests/ya/test_recursion4.c
+++ b/src/plugins/aorai/tests/ya/test_recursion4.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
# pragma JessieIntegerModel(math)
diff --git a/src/plugins/aorai/tests/ya/test_recursion5.c b/src/plugins/aorai/tests/ya/test_recursion5.c
index 0f902c0071f25495d236c849b770836a8b227ee4..b032ad61c1b7093e084727b1b3f9c11c00bf9cd3 100644
--- a/src/plugins/aorai/tests/ya/test_recursion5.c
+++ b/src/plugins/aorai/tests/ya/test_recursion5.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_struct.c b/src/plugins/aorai/tests/ya/test_struct.c
index d94c75970eb6a1897bc2cb560147174f73452bf3..d6476a3593a5e3d3afa76f5c2207747a39ae7d52 100644
--- a/src/plugins/aorai/tests/ya/test_struct.c
+++ b/src/plugins/aorai/tests/ya/test_struct.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
struct People{