From 20c14cdc6b23f39e620d50ca730648490e4e409a Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 11 Oct 2021 10:49:16 +0200
Subject: [PATCH] [Aorai] using LIBS directive of ptests
---
src/plugins/aorai/tests/ltl/goto.c | 2 +-
src/plugins/aorai/tests/ltl/test_boucle.c | 2 +-
src/plugins/aorai/tests/ltl/test_boucle1.c | 2 +-
src/plugins/aorai/tests/ltl/test_boucle2.c | 2 +-
src/plugins/aorai/tests/ltl/test_boucle3.c | 2 +-
src/plugins/aorai/tests/ltl/test_factorial.c | 2 +-
src/plugins/aorai/tests/ltl/test_recursion1.c | 2 +-
src/plugins/aorai/tests/ltl/test_recursion2.c | 4 ++--
src/plugins/aorai/tests/ltl/test_switch2.c | 2 +-
src/plugins/aorai/tests/ltl/test_switch3.c | 2 +-
src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c | 2 +-
src/plugins/aorai/tests/ltl/test_switch3_if.c | 2 +-
src/plugins/aorai/tests/ltl/test_switch3_return.c | 2 +-
src/plugins/aorai/tests/test_config | 3 +++
src/plugins/aorai/tests/test_config_prove.in | 3 +++
src/plugins/aorai/tests/ya/aorai_ptr_field.i | 2 +-
src/plugins/aorai/tests/ya/assigns.c | 6 +++---
src/plugins/aorai/tests/ya/bts1289.i | 4 ++--
src/plugins/aorai/tests/ya/declared_function.i | 2 +-
src/plugins/aorai/tests/ya/deterministic.i | 2 +-
src/plugins/aorai/tests/ya/formals.i | 2 +-
src/plugins/aorai/tests/ya/generate_assigns_bts1290.i | 2 +-
src/plugins/aorai/tests/ya/hoare_seq.i | 2 +-
src/plugins/aorai/tests/ya/incorrect.i | 2 +-
src/plugins/aorai/tests/ya/logical_operators.i | 2 +-
src/plugins/aorai/tests/ya/loop_bts1050.i | 2 +-
src/plugins/aorai/tests/ya/metavariables-incompatible.i | 2 +-
src/plugins/aorai/tests/ya/metavariables-right.i | 2 +-
src/plugins/aorai/tests/ya/metavariables-wrong.i | 2 +-
src/plugins/aorai/tests/ya/monostate.i | 2 +-
src/plugins/aorai/tests/ya/not_prm.i | 2 +-
src/plugins/aorai/tests/ya/other.c | 2 +-
src/plugins/aorai/tests/ya/saveload.i | 2 +-
src/plugins/aorai/tests/ya/seq.i | 2 +-
src/plugins/aorai/tests/ya/seq_loop.i | 2 +-
src/plugins/aorai/tests/ya/serial.c | 4 ++--
src/plugins/aorai/tests/ya/single_call.i | 2 +-
src/plugins/aorai/tests/ya/singleassignment-right.i | 2 +-
src/plugins/aorai/tests/ya/singleassignment-wrong.i | 2 +-
src/plugins/aorai/tests/ya/stack.i | 2 +-
src/plugins/aorai/tests/ya/test_acces_params.c | 2 +-
src/plugins/aorai/tests/ya/test_acces_params2.c | 2 +-
src/plugins/aorai/tests/ya/test_boucle_rechercheTableau.c | 2 +-
src/plugins/aorai/tests/ya/test_factorial.c | 2 +-
src/plugins/aorai/tests/ya/test_recursion4.c | 2 +-
src/plugins/aorai/tests/ya/test_recursion5.c | 2 +-
src/plugins/aorai/tests/ya/test_struct.c | 2 +-
47 files changed, 56 insertions(+), 50 deletions(-)
diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c
index 8cbd56c0842..2194b9d07f1 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 db2f6bc0c3f..a56440535d6 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 7b091c51b76..b0777d84eef 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 8aa77e6f8b0..3babc406ceb 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 6da17de07b2..70118bf9196 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 0ad64760026..8957c6eaba3 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 14be685a47b..a3d4218b6a7 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 7d93ab3fa3a..4053c83792c 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 2bb7284fbbd..a9d42339d79 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 5d9e8582f49..78866e16d20 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 352725ef984..4d3d0d7cd0c 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 93dd122636e..77e6d89fb0e 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 8df70979968..0835dfd7f17 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 c8feb6120b5..2a1eb0b9ab0 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 2e96488c0c4..6f7530d8beb 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 24c8ffc30a7..2d543c27625 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 0e1c52123e2..0a7a6cf9197 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 93cf50233c6..4275cbc2ed3 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 12f50538eb3..0ec1fc04fbd 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 d892d891378..af544b32ecb 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 a463e4f7d37..7339298dade 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 d9333d415f6..698e1549a52 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 b60ae6082da..be7428a41e3 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 01f70280860..36dc2f005ae 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 1dcbba59346..12b25974ec2 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 86fe369e9f7..bb697cf3e49 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 ac025ee3032..56daa093e4e 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 9d88e67323f..0be9f13ce1b 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 febfd16cb34..23c49ad2150 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 0d72d9a431c..42e221ff638 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 8b5c4281608..e1133d9675a 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 c4977e2a37d..f395044d953 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 2ac81c70606..f7fc1cf0ab6 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 1ba54569e12..96c875ed9bd 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 bee4d37d3cf..ff634f0b1de 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 9efe13a270b..e1aa4af0049 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 51abf5a7ef3..015593d0f1f 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 4c5612f5107..8d16f793ff2 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 baa7b42e03e..3c61f3cb9e5 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 d911301c686..da30e1597e8 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 dc673f9bc59..3f7e08b1469 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 7f25f23facb..597bd15931e 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 da220198440..413b72d10ed 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 fbb9762854c..87864af429e 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 e88b8471fb7..679c0269226 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 0f902c0071f..b032ad61c1b 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 d94c75970eb..d6476a3593a 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{
--
GitLab