diff --git a/doc/developer/tutorial/hello/Makefile b/doc/developer/tutorial/hello/Makefile
index 97d6a65afab8dbba4c43b9e0db587fcd5d842fd8..75acfacf88cae594c544236c35bf2a2d3c04505a 100644
--- a/doc/developer/tutorial/hello/Makefile
+++ b/doc/developer/tutorial/hello/Makefile
@@ -30,17 +30,17 @@ all: clean $(FINAL_PLUGINS) $(MLIS)
generated/src/Makefile%: src/Makefile%
mkdir -p $(dir $@)
cp $< $@
- headache -r $<
+ headache -r $@
generated/src/%.ml: src/%.ml
mkdir -p $(dir $@)
cp $< $@
- headache -r $<
+ headache -r $@
generated/src/tests/hello/%.c: src/%.c
mkdir -p $(dir $@)
cp $< $@
- headache -r $<
+ headache -r $@
generated/src/tests/hello/oracle/%.oracle: src/%.oracle
mkdir -p $(dir $@)
@@ -49,7 +49,7 @@ generated/src/tests/hello/oracle/%.oracle: src/%.oracle
generated/%/Hello.mli: src/Hello.mli
mkdir -p $(dir $@)
cp $< $@
- headache -r $<
+ headache -r $@
generated/script: generated/src/run_print_to_file.ml \
generated/src/extend_run.ml
diff --git a/doc/developer/tutorial/viewcfg/Makefile b/doc/developer/tutorial/viewcfg/Makefile
index 67918576782a6915848671cabc6c6808eebba8d5..dc208cd5b0b03a25eab2e5a8a75861418b9c3e23 100644
--- a/doc/developer/tutorial/viewcfg/Makefile
+++ b/doc/developer/tutorial/viewcfg/Makefile
@@ -31,16 +31,16 @@ MLIS=$(addsuffix /ViewCfg.mli,$(filter-out generated, $(DIRS)))
dirs: $(DIRS) $(MLIS)
-$(DIRS):
+$(DIRS):
mkdir -p $@
generated/src/%: src/%
cp $< $@
- headache -r $<
+ headache -r $@
generated/%/ViewCfg.mli: src/ViewCfg.mli
cp $< $@
- headache -r $<
+ headache -r $@
generated/intermediary/print_cfg_novalue.ml: generated/src/print_cfg_begin.ml\
generated/src/print_cfg_vfile.ml\
@@ -61,7 +61,7 @@ generated/intermediary/print_cfg_value.ml: generated/src/print_cfg_begin.ml\
generated/intermediary/dump_function_memo_no_clear_cache_and_deps.ml:\
generated/src/register_cfg_graph_state.ml\
generated/src/dump_to_string_memoized.ml\
- generated/src/dump_function_memo_no_clear_cache.ml
+ generated/src/dump_function_memo_no_clear_cache.ml
rm -f $@
for i in $^; do cat $$i >> $@; echo "" >> $@; done
@@ -69,7 +69,7 @@ generated/intermediary/dump_function_memo_clear_cache_and_deps.ml:\
generated/src/register_cfg_graph_state.ml\
generated/src/dump_to_string_memoized.ml\
generated/src/register_value_computed_state.ml\
- generated/src/dump_function_memo_clear_cache.ml
+ generated/src/dump_function_memo_clear_cache.ml
rm -f $@
for i in $^; do cat $$i >> $@; echo "" >> $@; done
@@ -91,7 +91,7 @@ generated/value/cfg_print.ml: generated/src/print_stmt.ml\
generated/value_with_gui/cfg_print.ml: generated/value/cfg_print.ml\
generated/src/dump_function.ml\
- generated/src/gui.ml
+ generated/src/gui.ml
rm -f $@
for i in $^; do cat $$i >> $@; echo "" >> $@; done
@@ -147,8 +147,9 @@ generated/split/cfg_gui.ml: generated/src/gui.ml
generated/split/Makefile: src/Makefile.split
cp $^ $@
+ headache -r $@
-pdfs/modules.pdf:
+pdfs/modules.pdf:
cd generated/split && make doc
cd pdfs && dot -Tpdf ../generated/split/doc/code/modules.dot -o modules.pdf
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index 397ae1e9f09f6236806909308121e29296101e7a..709483f25f90e116088c9d64cafd0e9a724c01ca 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -11,12 +11,13 @@ module P = Plugin.Register
let help = "utility script for aorai regtests"
end)
-module TestNumber =
- P.Zero
+module TestID =
+ P.String
(struct
- let option_name = "-aorai-test-number"
+ let option_name = "-aorai-test-id"
let help = "test number when multiple tests are run over the same file"
let arg_name = "n"
+ let default = "0"
end)
module InternalWpShare =
@@ -81,7 +82,7 @@ let extend () =
tmpdir ^ "/aorai_" ^
Filename.(
chop_extension (basename (List.hd (Kernel.Files.get()):>string))) ^
- "_" ^ (string_of_int (TestNumber.get ())) ^ ".i"
+ "_" ^ (TestID.get ()) ^ ".i"
in
let () =
Extlib.safe_at_exit
diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c
index 2194b9d07f19720dc26a6c04cded5604ed96f594..4051a1c7461bebeccbc938ee835d02f08dcf42e6 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
index 83e2a27b7b3b7f3733cd450ecd4a3f5de84a494a..75727cb763df1f513bf7577e101ac67f357eb51a 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/goto.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing goto.c (with preprocessing)
[aorai] goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_goto_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
index e7de1c204b12e9a1fbe846ccf05d4d5b4c65e7e6..688297dcb4ef5b8edbbc2a2b0e55413f218616b5 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing test_boucle.c (with preprocessing)
[kernel:typing:implicit-function-declaration] test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
-[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:88: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0_prove.i:88: Warning:
Neither code nor specification for function call_to_an_undefined_function, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
index ec65f1cd8ba228c4a8707b1cd04d9c40bb4d7882..7677d61f6e186f9feb94a26d454fded1af587f16 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle1.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_boucle1.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle1_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
index 695e2cd411d96821d1698322904a24eb87b5ce26..cbcc62814203d5778b7a285ea79ec7626f6b669a 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle2.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_boucle2.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle2_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
index 996d6f250a2d45bf6ae7c586ae60bbde138bc487..e4521ba5507b74d4631eb3b753ae66ab7c9fd983 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_boucle3.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_boucle3.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle3_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
index 5c41476e0fcbb5a60147cb344fb0478177d44df1..5f6d6d70fb61adac5bb677e9d0c150feba9ec974 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_factorial.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_factorial.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_factorial_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
index 99194bb1afdd17f27497e8a87632619792a632df..f42663514d202a90e86f445199dcfe3c4e87fb02 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion1.res.oracle
@@ -5,6 +5,6 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion1_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
index 46a80cf5271b93fe9675b3c085f4892d58401cdb..27d2076bcfa8e9ab3ab98bb5e6a0d28fa1048dc1 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing test_recursion2.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion2_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
index e8dd8946e8e2c9e6dd22293a47a3dd767315f9b7..5a6f4195d29acd65be002efbabd0656ad1f22f45 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_recursion2.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing test_recursion2.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion2_1_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
index e9db79281a7fed579f6189323608622e02357ca2..cf121000fcc79c8b6f1904a163ed7f11067a29f2 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch2.res.oracle
@@ -3,5 +3,5 @@
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
[aorai] test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
-[kernel] Parsing TMPDIR/aorai_test_switch2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch2_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
index 34dad3748ba28f4256ee3d1323753640ebfc8b6a..5d5aaa7031a99ca6f97ea5bcbeb7799529122405 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_switch3.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
index 9953b206f82403e0ece741cec752b101977d4d35..303f5bb7833133883211eb999f85f9e51cfb4d04 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_et_recursion.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing test_switch3_et_recursion.c (with preprocessing)
[aorai] 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 TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_et_recursion_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
index a2b92bf014992963064c153c8e73deb0017e649d..83e57ce33af44afd76f8b7a27ef0f3303b118db3 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_if.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_switch3_if.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_if_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
index 131d5766526add903f7fa0c2660b29ade31319ec..192efed268857fca46bc8fd49975b27f5fbc7e5f 100644
--- a/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle_prove/test_switch3_return.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_switch3_return.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_return_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ltl/test_boucle.c b/src/plugins/aorai/tests/ltl/test_boucle.c
index a56440535d6e6e93fc9accea8002742822e28c85..47794157e8d1c20902db348db6355a853dd3b29c 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 b0777d84eef44897ac6fb39e07fa0891a484911d..5aa255651392ad16af77e6accd80803e74a6e101 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 3babc406ceb416fe250d5bd22ba8c9802ca6b885..4145427d820836707432eaca4eba6999d714c69c 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 70118bf9196129a005f73f79e2ffa9191202462e..013fc8878c153ebe299d2f12c8b99fa9b0e0a209 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_factorial.c b/src/plugins/aorai/tests/ltl/test_factorial.c
index 8957c6eaba34bfa772bfe7ba3d9ddb69aa7a31c9..3a47201d2f6459ece6a01d9809ce9da7f1fa21a8 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion1.c b/src/plugins/aorai/tests/ltl/test_recursion1.c
index a3d4218b6a75cbde51796d0cda3efb819223d258..781af6b7a8e4dd537958d298e11616822fb82004 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c
index 5fcb6f0c3ebf0907f6bf7e0c50b030beef2ce9e1..53277aac6823f3c0d423616c3017312483749fc6 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 a9d42339d7934d2c81006e4c284adf36de8b6c31..b489cf8ac42af7cf66e06fc8de4a9265f36d7a66 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 78866e16d205ef3a4438779a790c18f8d69a999d..6954b71bb89ef6d2358260465765c77d74764065 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 4d3d0d7cd0c875938e365e08c25546516d926ee7..7315eb493f479f40b2ed17aa210dab9493388e88 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 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 7411887a0f2a1140d5ef3ec56bb949db7c1349e4..9fd6094996fa13fe4b773afe5c58b4bdab8ba52f 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 %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 f2b2c98efc5833cfe28fc5810531ada97f216fc9..06dbc5fbcd6602de1aa867e5c19d10440548251b 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 %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl %{dep:@PTEST_DIR@/test_switch3.ltl} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ya/aorai_ptr_field.i b/src/plugins/aorai/tests/ya/aorai_ptr_field.i
index e8027df1368135e512015b0ae005748bf6a9911f..6d48d76cff3d1a9322c5639f04b27776a24fd456 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 2278fd5437c5daba126b9f9489bd8be909f467e3..40f4cb8e76945fe8ddd102ae7d48d632990f4218 100644
--- a/src/plugins/aorai/tests/ya/assigns.c
+++ b/src/plugins/aorai/tests/ya/assigns.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata %{dep:@PTEST_DIR@/assigns_det.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/assigns_det.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
MODULE: name_projects
LIBS:
OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -then -print
diff --git a/src/plugins/aorai/tests/ya/bts1289.i b/src/plugins/aorai/tests/ya/bts1289.i
index bfeffbded20b93980a36e8a3d1c23e3c53ce3847..9b018dd840ebb0ffa9fdde3eeb3befeed4408b5b 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@-2.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@-2.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 ffedbdef46601dc010287d2f383b37510a9411d9..2cd6b702ca4e74c7d101bb1d6320639bed89482f 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
int f(void);
diff --git a/src/plugins/aorai/tests/ya/deterministic.i b/src/plugins/aorai/tests/ya/deterministic.i
index 17876336fef74716073ba4e2472e47476c0bbf3f..91db6c9ba342ceea82dbc1e1a66bfd3e9690a1c7 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
int X;
diff --git a/src/plugins/aorai/tests/ya/formals.i b/src/plugins/aorai/tests/ya/formals.i
index e97c64c11e7d035e7905e10f9bd46e110ee552a0..7cd6e26c65e12719a3ddd1dfe4e8e1370369d4a7 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 87b0c3dbbd5dd4b42c312adb4c04d2710a531835..cd8ec32a8440120cc27fc69d41712bdcd4f0eb97 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 4b8bf45a3e23a51be90717114945323d8d2d1673..213f469ea1acaaf6c6478d4b987feec89a919cd0 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
void f(void) { }
diff --git a/src/plugins/aorai/tests/ya/incorrect.i b/src/plugins/aorai/tests/ya/incorrect.i
index 50f7b06c4143b892c532db3cf64adc7457fc661c..fad205dde2be66a2dbfddee5473ba46dd140ff87 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 c5284ed4423860f21cef346f4cfa26d866cc48e9..e70aa15ac821e50fdee3bfb33d49684350c735a2 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 c2d0d1c6523c6cfb2182dcc652cf913d017e6bd7..7ee8431f8e46826c223b7f9df8c60ae7dc81a2a1 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 6f41f2d43aba8f2ad19686cbed2f209e05daa35f..0654e388f0d77060f17d6a6a69c47d20383e9744 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 0ff8e12047ef50595f6ea275e5f13f752ded68c6..2d51676f37c310c85389194d485329208781f581 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 bfe546815b766c05c869c6ca92fb2a43b6f27bd8..86c3fea665572e8e103d04f2e91bdcb1474b0dd8 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 554efa0a432a36bf02bc45d58475145a16294566..306c7473dc11a52b88dabe8fcbb6d5607c4448a3 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 193f1d40a58814631991795b61431f968aab4475..e633a78721bae2a0234a8b38fc944165afdda96d 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -main f -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
int f(int x) {
diff --git a/src/plugins/aorai/tests/ya/observed.i b/src/plugins/aorai/tests/ya/observed.i
index 05b843f0fdaa6229fe48204c27a53b820c10d405..0e289248335e13dc700fdd49bd628a8b7b5d295f 100644
--- a/src/plugins/aorai/tests/ya/observed.i
+++ b/src/plugins/aorai/tests/ya/observed.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
void f(void) {}
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
index db606c584c2f7599fd50686931670bbca4fb80fd..3e07a09e3ed877eca0151cdc812e2bc4e90c84da 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/aorai_ptr_field.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing aorai_ptr_field.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_aorai_ptr_field_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_aorai_ptr_field_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
index 9444bf13b16ac3ca729ea62c30f6831a8cf7c71e..bda6f08d05ac4dcbccbe86524c0f9b1a94b4b450 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.0.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing assigns.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_assigns_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
index 2a6330eb8a63cb5c8660c3013508b85c7ee472a7..7b35992fa3cc6b848655c7c1994fe85b7134e2ed 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/assigns.1.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing assigns.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_assigns_1_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
index 66d034091f8b24148f25362d46cd1ebc6c210b0e..e5a428587624cf17c517ad88943e2b981562b9f9 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.0.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing bts1289.i (no preprocessing)
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing TMPDIR/aorai_bts1289_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_bts1289_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
index c9060e0b526e4086638d1896cdb98ab0e4332728..0d6e0f8661db209afd6d05d3229a3d9d4284c909 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/bts1289.1.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing bts1289.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_bts1289_1_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
index d747fe5882fadaa4a01a6ce702ad622f82f9f4c7..3a6d4d2a8b0618d67ccd678b53713208d7e14939 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing declared_function.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_declared_function_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:105: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0_prove.i:105: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
index 08e3269722c66263b4f76d9d3b54debcda516dd1..d98b5d90f19d672d5bde54230047eceabb04de08 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/deterministic.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing deterministic.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_deterministic_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
index edac608e2ac06efa4966744dc9e9ccfc8fe755c0..cd0f79132b6dcdea93e7e0d1b967c8bf8832fbf7 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/formals.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing formals.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_formals_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
index 301ac8916a29687b04560f5f1773e4508b024c33..903e1117ebd6bc2f7be5f73565d1bbe774bb2f66 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/generate_assigns_bts1290.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing generate_assigns_bts1290.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
index 99cb781b03b272bcfe721dc053b8a4b78860d79e..89597d3968538555d42ce1d229bbea994d479314 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/hoare_seq.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing hoare_seq.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_hoare_seq_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_hoare_seq_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index c4645a8443912f0be5f5733812d7bc52722ee382..9978b066020d6e29a93eb1d579a286b6d5fcbebe 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing incorrect.i (no preprocessing)
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_incorrect_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:70: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0_prove.i:70: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
index 076ca1b8c7b813c494dc0c5b3f7ebf0afbea54c0..29aecc93cd5aa3b3e4be7d231cf93ee5d9d6412a 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/logical_operators.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing logical_operators.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_logical_operators_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_logical_operators_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
index 9a19d3640e3ac7b51bf610e9c1b807d0453c2af3..c514a80e2bc833f301b96bf2703a46e7cff35d09 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/loop_bts1050.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing loop_bts1050.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_loop_bts1050_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_loop_bts1050_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
index 4546d97a79fb29d2afe58f2419811c141a4379f7..2e2e484eb88c1a943bc8e1f4b204b7bf64282fc5 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/metavariables-right.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing metavariables-right.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_metavariables-right_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_metavariables-right_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
index e3ab2c38cddfb9a4e714d874556ba290e2750216..0235b9052e6da7cac06e78b7aeafd32cb0289c60 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/not_prm.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing not_prm.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_not_prm_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_not_prm_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/observed.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/observed.res.oracle
index 8f9b2717129ea34944eae366ef99e4c62c58490f..7b8488f86fd459a03846114d464cf331b236b81b 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/observed.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/observed.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing observed.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_observed_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_observed_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
index f3e375c42bb88adb8f3a552756de0403daf76e30..a30f9365ecb978c41272aab4bf63f85305cb2737 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/other.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing other.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_other_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_other_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
index 7fe8c4257736f950a754f3b248e9e39c6e3dcc99..1b1c328f2d74bb3ccf97c8c9db81ad22f2c19527 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing seq.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_seq_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
index f3181cabba43ed4b2730e10fd72225ea0196da7c..39c42327a8c99ef8b1aea48fdf170615a50ea689 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/seq_loop.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing seq_loop.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_seq_loop_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_loop_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index 8a3f68f41062cd3e51d5f89c9ad23f8d0f5bbf73..3ee9ca8546d798ee44c5cbfa373696758859ae75 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing serial.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_serial_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:1450: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0_prove.i:1450: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
index da028f5987681139cb5f459446f5909e0c23d5cc..5b61e414f05b4a6533697113790bc1578e4cd9aa 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/single_call.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing single_call.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_single_call_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_single_call_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
index 68648d50b091af312d19acd93d37a1b028637b53..873687622c228cfad879bd0ef31a52f8f78cc7f7 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/singleassignment-right.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing singleassignment-right.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_singleassignment-right_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_singleassignment-right_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
index db03c158b218cb76f7c9c9d24e15edcf127bdcdd..db559cc0cd0b7b91e97007de210595536bae1b92 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/stack.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing stack.i (no preprocessing)
-[kernel] Parsing TMPDIR/aorai_stack_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_stack_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
index 5d9c6908b9d0f0cce05042ddb6ca49684eacefed..00d74abbd01fc747e6f40e6561f5be853558602f 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_acces_params.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_acces_params_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
index 340123dd3fb0400a03c41bbb32255c4f3d38ff1a..a5d86c4a79b4346c4c1854571edde923d91b214d 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_acces_params2.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_acces_params2_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
index b61d21acb0b2a42c23be4d5b2990b04618e9c1de..78aef78c448813b014f05c6bebf391a38a127f29 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
@@ -3,5 +3,5 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
index 5c41476e0fcbb5a60147cb344fb0478177d44df1..5f6d6d70fb61adac5bb677e9d0c150feba9ec974 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_factorial.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_factorial.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_factorial_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
index 609b93ca7201d1d76de8e6956a7bf9fe00211507..a641bba4b4341d5dea7d13a56401df27115dafde 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion4.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_recursion4.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_recursion4_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion4_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
index 1826b662a98051fec901f78351a46922a1a92ba5..f0a04a4c78c08fc214b9e1b753c51ea1880f934c 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_recursion5.res.oracle
@@ -3,5 +3,5 @@
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] Parsing TMPDIR/aorai_test_recursion5_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion5_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
index 74d9ac3e6d00efb5cc58286dd04a6892da4226e7..e2a7b951f52c56ae61118effbf64592f8dda56c2 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_struct.res.oracle
@@ -1,3 +1,3 @@
[kernel] Parsing test_struct.c (with preprocessing)
-[kernel] Parsing TMPDIR/aorai_test_struct_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_struct_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/other.c b/src/plugins/aorai/tests/ya/other.c
index 31cbfb850314dee02b289ff26e43c2ba89fe798d..8362960d7563ce2ed5566a52ec3278bdfb20d262 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
int x=0;
diff --git a/src/plugins/aorai/tests/ya/seq.i b/src/plugins/aorai/tests/ya/seq.i
index edee6f64841cd2adba02259e646b709d60566ef0..24ad34ad46684603c1efdfc844515d42debd44a4 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 5ea16e8dad7b9215efdb5ed5776ba26fd472f9c8..7c6dd8e7f027bbb113ddab4b4c7dd829904cd555 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
void f() {}
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 039225c0ee0d954692b44a836773e9f8c15ca256..52bdcce277f31da80de99ac0ce33ba67734364b1 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 %{dep:@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
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-smoke-tests -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ -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 %{dep:@PTEST_DIR@/@PTEST_NAME@_wp.ya} -aorai-smoke-tests -aorai-test-number @PTEST_NUMBER@ -aorai-no-acceptance @PROVE_OPTIONS@
+OPT: -cpp-extra-args="-DFOR_WP" -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@_wp.ya} -aorai-smoke-tests -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ -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 b705b3eaa487ea2107cef31356102331dd9b76bc..cf46f34cf511be0300f8485c9b997fdfd282dcb3 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 8d35fbd55759bdbb1283b9e8a09b192c1dc05526..049a066fa4a53e6ee736731e8844445127eb1c3c 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 ea86f81ff969798b7918ef0713dcc60ad545e6ad..945ecd965c27ee7fbe4481867f39bf2ed93af29d 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 dbf9123b19db33bb210c845953aeb5e69e9d7e9e..1e54c03921d948971878f9204d9b22cb4bb02054 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 c6bcf688213aeff1c2ecc32fee6fb977d2147726..cf25d86e35dc068e4c801de1c5a65730268bb61f 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 d37cb41f7a238d13ecc0df8d7ba9be1164e9d0a2..220cfe50c1eec403cbd72b214b4d6580d8adfd64 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 07a1a808088774d892278326cdc066ff08cde802..3adf3ad465a27d19e498b17dc82bd8710cd31fb4 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_factorial.c b/src/plugins/aorai/tests/ya/test_factorial.c
index 904cd3c8674657f5d470f44b2f2c7a4e3ddec5bc..a132cdd62ddc2de84a3257fd7e186e7f13c31e0f 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_recursion4.c b/src/plugins/aorai/tests/ya/test_recursion4.c
index a6c468a723f10cd74880f6a43c0a65d8b478ed4a..d07f4ba8ce6f6f36ffc103bf9c96f6b6c9636d4e 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @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 7033403bcafb788fc64beebccc4ccff73b6a05c4..f8eb2402586c7093fe9a87bafe08506f55995e08 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/ya/test_struct.c b/src/plugins/aorai/tests/ya/test_struct.c
index ecbdfe9fbff77cfe423148b7c8935ef888249f58..4566f8296cc71900c3ce3d487970f7c493c4b1a1 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 %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata %{dep:@PTEST_DIR@/@PTEST_NAME@.ya} -aorai-acceptance -aorai-test-id @PTEST_NUMBER@@PTEST_CONFIG@ @PROVE_OPTIONS@
*/
struct People{