diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index 75cc19b2aa94b4b2f35a4dee6942d3081ab4407b..b559eeb411ce69b62129d8bf7ba5beb05415ec3d 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -93,6 +93,7 @@ let extend () =
in
Project.copy ~selection my_project;
Project.set_current my_project;
+ Kernel.SymbolicPath.add ("TMPDIR:"^Filename.get_temp_dir_name());
Files.append_after [ Filepath.Normalized.of_string tmpfile ];
Constfold.off ();
Ast.compute();
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
index 8b7b7b0a0d808b69edc11ad02f4aefedf27e50b4..fbe4ad9cdb9a79546ad1edcf8509f96e5c777862 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
@@ -2,7 +2,7 @@
[aorai] Welcome to the Aorai plugin
[aorai] tests/aorai_ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_goto_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 3,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
index d75adfbc5e5adbdb6129a99284c5158c1df92e64..aaec910bc89e2fb8b25a2b916ba7c738358dc149 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
@@ -2,7 +2,7 @@
[kernel:typing:implicit-function-declaration] tests/aorai_ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_call_to_an_undefined_function = 3,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
index 2bf7be9ad507d609b9aba915153e8c40db855a7b..00397dd0694afd797ca244df4224ac59c5b09c44 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_boucle1.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle1_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_commit_trans = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
index ce25f46ed9e9ecbef85be7fe724af1ee488c5a9c..549c102c1e8e74a2905cd94c1abf6605570549a2 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_boucle2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
index 4e2b603ec5833b8091fc4ba8b1b30ea012cca67b..a0bf80d2ad89ff8aa7dab1243fb245f3963fa26a 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_boucle3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle3_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
index 68238aef16a83db606409ddf834c90d7a23bb28b..83881fefc479fbdb8762b6170366f5421fc3b4d0 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_decode_int = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
index 3c998970b026be782c5dee0a3d63d83a87e0f035..17f30040448211dfc78076ddad4b6d2611f71035 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
@@ -6,7 +6,7 @@
[kernel] tests/aorai_ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion1_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_count = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
index c022dfa8dcacf2851c6bb4a3722d48e9bedc8060..fa035fa7b393eab8155d400b0869c91294f94462 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_count = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
index 54106258b48bd381d9e66a9305e730782ca15216..c0b03d21e5a310ea71a59df7996b30454ca1a1b3 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion2_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_count = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
index cf8da9996a690b3628d39c46fbacbcb0f38f8895..66e5ef7087c2bf26929f175a909c26d2c0c5a020 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
@@ -4,7 +4,7 @@
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
[aorai] tests/aorai_ltl/test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
-[kernel] Parsing /tmp/aorai_test_switch2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch2_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 3,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
index 231b350ca48c16279500ec0d3bddba4572480690..1a851742f860e6eaccef14022d39336ea60d76cd 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_switch3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_switch3_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_count = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
index 3675b0bbde05fe61d8bddeb093e87c3ba9f01247..46e93cf5955dd8afa392e241e72b228174bd4dbd 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
@@ -2,7 +2,7 @@
[aorai] Welcome to the Aorai plugin
[aorai] tests/aorai_ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_test_switch3_et_recursion_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_count = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
index 6c2693aa58d0b260012100dca1b53d09bff68f02..cc22f6aeff9f99efd129a0077dab15029e0f395d 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_switch3_if.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_switch3_if_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_count = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
index f3a55fc5f091fd8ff0e6861695b5800bef91b4cc..e9a95b82add1b30272302f110d3a914eda76cfab 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_switch3_return.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_switch3_return_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_count = 2,
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
index 616ce9f00553b51ef6c8881e3f5165116e8e457a..532b90605c9e7fd2412f7acb7d14bf08001bb35e 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
@@ -2,7 +2,7 @@
[aorai] Welcome to the Aorai plugin
[aorai] tests/aorai_ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_goto_0.i (no preprocessing)
-[wp] /tmp/aorai_goto_0.i:4: Warning:
+[kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
+[wp] TMPDIR/aorai_goto_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
index d43ee66898a6a0870356373cd283d102024187a9..05c3feeaa60e3f1f92e0b8ba76eb6c6122439fb6 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
@@ -2,7 +2,7 @@
[kernel:typing:implicit-function-declaration] tests/aorai_ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] /tmp/aorai_test_boucle_0.i:81: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_test_boucle_0.i:81: 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/aorai_ltl/oracle_prove/test_boucle1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
index be9bc110e5eeb5962503050a78c8eea4c41440a2..a2858313292be7418e73a23b93af02f6629c247b 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/aorai_ltl/test_boucle1.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle1_0.i (no preprocessing)
-[wp] /tmp/aorai_test_boucle1_0.i:3: Warning:
+[kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
+[wp] TMPDIR/aorai_test_boucle1_0.i:3: Warning:
Global invariant not handled yet ('inv_cpt' ignored)
-[wp] /tmp/aorai_test_boucle1_0.i:6: Warning:
+[wp] TMPDIR/aorai_test_boucle1_0.i:6: Warning:
Global invariant not handled yet ('inv_status' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
index 68ab6eeb39b5e988d6299c772e0680d87fe9bf18..e97acf67cf59ba3e69a955b02201a474c4161328 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_boucle2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle2_0.i (no preprocessing)
-[wp] /tmp/aorai_test_boucle2_0.i:4: Warning:
+[kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
+[wp] TMPDIR/aorai_test_boucle2_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
index 0da9c1d93facae9b856c51349d11f136e5f56d3b..89b1e115d163fea98691a1f270525c3065798960 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_boucle3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle3_0.i (no preprocessing)
-[wp] /tmp/aorai_test_boucle3_0.i:4: Warning:
+[kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
+[wp] TMPDIR/aorai_test_boucle3_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
index ccb09c7d5a6177d9dd78b1d61563325e7de82611..0d9d32a4a9dad466774790e0329e94274b249816 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ltl/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
index bbd07a1eb1d3003bc8e907182be0a70aa4f635c0..efec492524c58eba9cde258c0ca253533cfdf79e 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
@@ -6,6 +6,6 @@
[kernel] tests/aorai_ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion1_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
index 44eb148e42acc40de7891e1de3e2f30c63ef84ee..cfdff3b4783727bb852f1f04ebf6334e4c44024d 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
index e6b17cbbc0bcf95c66ef24a36855489cc7d03a3e..48747cb0bc3b981f8f8933441f61b2524d7371d4 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion2_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
[wp] Warning: No definition for 'sum_tab' interpreted as reads nothing
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
index 697d945d96f427fa14aeaac9ee63d0596700a325..8be10ba231d366198b985de319ed75ec02f09c9e 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
@@ -4,7 +4,7 @@
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
[aorai] tests/aorai_ltl/test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
-[kernel] Parsing /tmp/aorai_test_switch2_0.i (no preprocessing)
-[wp] /tmp/aorai_test_switch2_0.i:4: Warning:
+[kernel] Parsing TMPDIR/aorai_test_switch2_0.i (no preprocessing)
+[wp] TMPDIR/aorai_test_switch2_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
index bf08eea3748c0b063dcb073dc3935ef15ab3f1ce..c16b5d9ac78fb1de1c3b068bc3131519a4ae7fe0 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ltl/test_switch3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_switch3_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
index 09beb110d3a22cad15eeeaf061f6d28ae9c69983..92f84ae74eed05d066fb4dcb249996d2cc4203b0 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
@@ -2,5 +2,5 @@
[aorai] Welcome to the Aorai plugin
[aorai] tests/aorai_ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_test_switch3_et_recursion_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
index 87f8f5e09ae03a0bf5f6eec2cbad8bea9110c8bb..b3d267405010542b538898c5c24a4684e7f17fc4 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ltl/test_switch3_if.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_switch3_if_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
index 79655160142ad3f1450763ed74c7720dcccae49a..eee329e90fcca428d303e33f1f27b06c1d34e87d 100644
--- a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ltl/test_switch3_return.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_switch3_return_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
index 5c7443d37ab4b68d8a950a2ddb5ef0c455aab032..47f3267657e928570e8e0991a2e78a4ecd7cf368 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 1,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
index 01876080d5c50d062d19b8d6c20f60cc1b5abb37..532ca3eb6287c8da0a43294c67a463a509763ab7 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_assigns_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
index 3dea38d70a1758d514c80e5bebfdd12241a774c9..98bf08db29a2cc860e07039e09a8d04fbe8f0e50 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_bts1289_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_a = 1,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
index 5f22740b63832b2c3709c3f672c8825a93836f61..fd7d1101bb2fb2121b3b22c4ece0497708f72b47 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_bts1289_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_a = 1,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
index fbeda724d7097f2cde8b8de75d6e58728dba4443..0df0a6971e9cc95955a62a32cc7c4ddce8fe1ea8 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/declared_function.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_declared_function_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
index c4a89c4951e49dd6d97a713c0904a4e9db62228e..689baf5769ff6744b39db6c6cc2ec6a5395aecdd 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/deterministic.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_deterministic_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
index c2bd9a6d56645f2ef6e3907fbaf3ec8b9e0ef476..78a84d592010a626fe4a3a7ad19537ed2bff899a 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/formals.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_formals_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
index 3d7e763902c3225e5a84ac081814ce057614a2eb..73a16e22e59b647871fdb2706992cce15062e8d7 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/generate_assigns_bts1290.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_generate_assigns_bts1290_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 0
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
index 546c4e7d846c246bf3f5083f02424d2db1110ced..76562013bb84c9425a3b90f38fc90a391d512e36 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/hoare_seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_hoare_seq_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_hoare_seq_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 1,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
index 6a56d3e182e0c035ee5381cd801f520ad7f4e5cc..06cbb9c48bd419965ab5379fc3bf994aa488fe0e 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/aorai_ya/incorrect.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_incorrect_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
index c0ad530b635d88c70687395a24eedf78959003ef..c05c6069a5880d03614ed6ed4794c5f9a93ce20c 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/loop_bts1050.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_loop_bts1050_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
index 4e83e52e08bab259fa97bfe3812b0f70e87f2625..d6178ca6da9a6e87cdb4995d0d032c4361e9440a 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
@@ -3,7 +3,7 @@
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[aorai] tests/aorai_ya/monostate.i:8: Warning:
Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
-[kernel] Parsing /tmp/aorai_monostate_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_monostate_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_States {
aorai_reject_state = -2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
index 6455cd141e580a4883d326c2a53bc531ba4752fc..5fbef083f59ebe46e152e5decda8af70067e030a 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/not_prm.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_not_prm_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_not_prm_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 0
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
index 1b70959421e89b5b3d9f3e2898a0c068a36c7696..4ce1155c6fc2190f1fe0e2c698053fffacb633b8 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/other.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_other_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_other_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
index 6d3bd0b4fd98b0ba42715b9b168313a037557a6d..2f50b76336fd275f57fa8892a1f7f607edd25f99 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
index 37a5942b8e57f96812af05d45bef498561273caa..3fc1aa4b123324c0f8a1a692209e81fc1747b0f9 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/seq_loop.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_loop_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_f = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
index 89cfcb8ea821190dc0cc3ea3870e2fe6dbd2ce62..56c4ead768158f924473f3ce443d46cd7786b87c 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/single_call.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_single_call_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_single_call_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 0
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
index 6920ad1626231603e42666fb549a8b29638eb6e1..66d9c0c8c916d43fc0ecc3c8cc68bb44a2f07de2 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/test_acces_params.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_acces_params_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
index 9899759571f86557d6b98dc26fffb020f53449e7..a0a380750fac0476fb65797459301c6873964733 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/test_acces_params2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_acces_params2_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_main = 3,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
index c65e202d5f674ce91226a5046aa89ee2729d7970..1c76b7f262dba9424bbe24b76e242b689724a57d 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -4,7 +4,7 @@
[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_foo = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
index 2db6fe590f82a8dfe1d0376ab13a987d8fe35aa4..a740a1612fa05b4cd47a5f570484276913ff7e46 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_decode_int = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
index 8a7f6b375212ee855fd0f4d271204ec492722401..c5ad4db6d6bf7b98443fe861e68e32495af6f923 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/test_recursion4.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion4_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion4_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_foo = 2,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
index f4f409b2231bf79236b0287a764b41e9a711eaa6..6374919dc68068980f2bae41a9417325054544de 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
@@ -4,7 +4,7 @@
[kernel] tests/aorai_ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion5_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion5_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_foo = 3,
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
index 48449b62e49d386fd111c2a150c6ab9990218630..982fefc8d4b58da149bd436d2353c6046fa0bd2e 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/test_struct.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_struct_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_struct_0.i (no preprocessing)
/* Generated by Frama-C */
struct People {
int Age ;
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
index 3bdcb7f459f7fb2a44ed44f1aa0aaee6ba7e272e..06c8b4708f3c12e44ecb6c364b112b24187accd1 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
index 64a6a02b04312590aa3e5ec95bb6490101f14a58..4f135df4cd3d93c6337725ed27c022d474025a77 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_assigns_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
index 84559a6dd0ebcc1b57577ce56e7faf127b7b5ea2..17783e40e74c2932ccc84f4b78dabfe7736e4d6d 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_bts1289_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
index 67505dcb5c5fe63cb83fcc65adc52c3a5bd19be0..d279c36d63806fb16b8d19fa0073cd79f9f48693 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_bts1289_1.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
index 7b836a362ab1163bacde49cb7e4253fadba3ae57..e2246cea6b23057621900301060013849a512f2c 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/declared_function.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_declared_function_0.i (no preprocessing)
-[kernel:annot:missing-spec] /tmp/aorai_declared_function_0.i:48: Warning:
+[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
+[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:48: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
index 40255d6fc4b460ffeae5c3d5ba8c673f9fc10a9f..2b066df7a37959600d91270d31f51876d2602f04 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/deterministic.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_deterministic_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_deterministic_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
index b7c2460da5ec97a7f2271f054e44d95a3dd6bb6c..9dc7a88aaabe365da0258fb03090d30c00743db3 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/formals.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_formals_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_formals_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
index e402347bb7fc056e82dd3e8504c6050e3590dda5..73ed0516b26166857ee35e562e3f5a2fcd6d561e 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/generate_assigns_bts1290.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_generate_assigns_bts1290_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_generate_assigns_bts1290_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
index fb6a559a080c3cde36d0d6f50f3904f680d036f2..645bedb5c60d8cfde08daf6bcfbe11cd4a6f05cd 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/hoare_seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_hoare_seq_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_hoare_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
index 5d37997bb66de5b2c67f367f052896246901a681..188fe594ffe49e9d08d3ccd484fd8a141995d697 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
@@ -1,7 +1,7 @@
[kernel] Parsing tests/aorai_ya/incorrect.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[kernel] Parsing /tmp/aorai_incorrect_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] /tmp/aorai_incorrect_0.i:61: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:61: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
index 2aa37b76715411cc4a93e8cc112216188223485d..e76d3c058de785292fc5d5c045492633951c7381 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/loop_bts1050.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_loop_bts1050_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
index 1b02aa00afdce03664c43bcfad7446b161d84efa..e371f48937ee69edc50da4c620eded9cfd920f10 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/not_prm.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_not_prm_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_not_prm_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
index e0b3215a1bc2fd6b7f741a66b2d397429f01b8b5..b1ee544dda19c9b81c9e3681f604496641db7516 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/other.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_other_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_other_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
index bb5f9ad8f3eb4a5a728b972b6a1f79269a6afdb6..dd13e947665826b87bae69ae061fa2be6c9b94a1 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
index c9b971ff32f785c699f1943afedef436ed421d0b..dea6b22f244d047db2bfb1c904091eab524203fa 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/seq_loop.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_seq_loop_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
index 7e3251748543b0c59732d52fe7cefbd879fab34d..8797931a06e76ca16fb55653b23a790658b22394 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/single_call.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_single_call_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_single_call_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
index eaa6a845adf8f0cecbbf57ddade5412f6d10e8a9..1ebb2698f42c894c6173177e010eccddb2d2ed8c 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/test_acces_params.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_acces_params_0.i (no preprocessing)
-[wp] /tmp/aorai_test_acces_params_0.i:4: Warning:
+[kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
+[wp] TMPDIR/aorai_test_acces_params_0.i:4: Warning:
Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
index dcd88018b2077a89a93a86987f9fb240be2e8cd4..f384bf00de177f7293d55b94403994f17564415a 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing tests/aorai_ya/test_acces_params2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_acces_params2_0.i (no preprocessing)
-[wp] /tmp/aorai_test_acces_params2_0.i:3: Warning:
+[kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
+[wp] TMPDIR/aorai_test_acces_params2_0.i:3: Warning:
Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
index c64d82f705727818e5737df5d9ee6ca3fc415864..a6605ccc1e3019efd298d25c53288009733da319 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
@@ -4,5 +4,5 @@
[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
index 4265d80c2eb5313a270a3c2918b056caed21c1fb..545adc2369a3ab86b66a0f503ecd6f91701042ea 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
index 6293804566c02aca053629caed4f6f2e462f0051..45cbb5e314dee2d80e9f83c2a95cbbd1af97acf0 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/test_recursion4.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion4_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion4_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
index db107f75b48196c402efe5dd5e659a4671124ae2..0c3bb1c41588c9c44de797b281ee70c187bcd6a1 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
@@ -4,5 +4,5 @@
[kernel] tests/aorai_ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_recursion5_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_recursion5_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
index 6571fc60e01366ccb49c3c043d5d571161517658..b0b68136917325352f72391cd991cdec4acca2d0 100644
--- a/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
@@ -1,4 +1,4 @@
[kernel] Parsing tests/aorai_ya/test_struct.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_struct_0.i (no preprocessing)
+[kernel] Parsing TMPDIR/aorai_test_struct_0.i (no preprocessing)
[wp] Warning: Missing RTE guards