From bf8e3faeb5fb4228115b1b2c8cb5c97dbb981432 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Mon, 28 Sep 2020 18:48:05 +0200
Subject: [PATCH] [aorai] make oracles robust to TMPDIR value
---
src/plugins/aorai/tests/Aorai_test.ml | 1 +
src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle | 2 +-
.../tests/aorai_ltl/oracle/test_recursion2.0.res.oracle | 2 +-
.../tests/aorai_ltl/oracle/test_recursion2.1.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle | 2 +-
.../aorai_ltl/oracle/test_switch3_et_recursion.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle | 2 +-
.../tests/aorai_ltl/oracle/test_switch3_return.res.oracle | 2 +-
.../aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle | 4 ++--
.../tests/aorai_ltl/oracle_prove/test_boucle.res.oracle | 4 ++--
.../tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle | 6 +++---
.../tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle | 4 ++--
.../tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle | 4 ++--
.../tests/aorai_ltl/oracle_prove/test_factorial.res.oracle | 2 +-
.../tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle | 2 +-
.../aorai_ltl/oracle_prove/test_recursion2.0.res.oracle | 2 +-
.../aorai_ltl/oracle_prove/test_recursion2.1.res.oracle | 2 +-
.../tests/aorai_ltl/oracle_prove/test_switch2.res.oracle | 4 ++--
.../tests/aorai_ltl/oracle_prove/test_switch3.res.oracle | 2 +-
.../oracle_prove/test_switch3_et_recursion.res.oracle | 2 +-
.../tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle | 2 +-
.../aorai_ltl/oracle_prove/test_switch3_return.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/assigns.0.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/assigns.1.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle | 2 +-
.../tests/aorai_ya/oracle/declared_function.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/deterministic.res.oracle | 2 +-
src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle | 2 +-
.../aorai_ya/oracle/generate_assigns_bts1290.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/incorrect.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/monostate.res.oracle | 2 +-
src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle | 2 +-
src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle | 2 +-
src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle | 2 +-
src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/single_call.res.oracle | 2 +-
.../tests/aorai_ya/oracle/test_acces_params.res.oracle | 2 +-
.../tests/aorai_ya/oracle/test_acces_params2.res.oracle | 2 +-
.../aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/test_factorial.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle/test_struct.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle | 2 +-
.../aorai_ya/oracle_prove/declared_function.res.oracle | 4 ++--
.../tests/aorai_ya/oracle_prove/deterministic.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/formals.res.oracle | 2 +-
.../oracle_prove/generate_assigns_bts1290.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle | 4 ++--
.../tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/other.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/seq.res.oracle | 2 +-
.../aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle | 2 +-
.../tests/aorai_ya/oracle_prove/single_call.res.oracle | 2 +-
.../aorai_ya/oracle_prove/test_acces_params.res.oracle | 4 ++--
.../aorai_ya/oracle_prove/test_acces_params2.res.oracle | 4 ++--
.../oracle_prove/test_boucle_rechercheTableau.res.oracle | 2 +-
.../tests/aorai_ya/oracle_prove/test_factorial.res.oracle | 2 +-
.../tests/aorai_ya/oracle_prove/test_recursion4.res.oracle | 2 +-
.../tests/aorai_ya/oracle_prove/test_recursion5.res.oracle | 2 +-
.../tests/aorai_ya/oracle_prove/test_struct.res.oracle | 2 +-
76 files changed, 87 insertions(+), 86 deletions(-)
diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index 75cc19b2aa9..b559eeb411c 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 8b7b7b0a0d8..fbe4ad9cdb9 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 d75adfbc5e5..aaec910bc89 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 2bf7be9ad50..00397dd0694 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 ce25f46ed9e..549c102c1e8 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 4e2b603ec58..a0bf80d2ad8 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 68238aef16a..83881fefc47 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 3c998970b02..17f30040448 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 c022dfa8dca..fa035fa7b39 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 54106258b48..c0b03d21e5a 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 cf8da9996a6..66e5ef7087c 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 231b350ca48..1a851742f86 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 3675b0bbde0..46e93cf5955 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 6c2693aa58d..cc22f6aeff9 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 f3a55fc5f09..e9a95b82add 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 616ce9f0055..532b90605c9 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 d43ee66898a..05c3feeaa60 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 be9bc110e5e..a2858313292 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 68ab6eeb39b..e97acf67cf5 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 0da9c1d93fa..89b1e115d16 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 ccb09c7d5a6..0d9d32a4a9d 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 bbd07a1eb1d..efec492524c 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 44eb148e42a..cfdff3b4783 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 e6b17cbbc0b..48747cb0bc3 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 697d945d96f..8be10ba231d 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 bf08eea3748..c16b5d9ac78 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 09beb110d3a..92f84ae74ee 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 87f8f5e09ae..b3d26740501 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 79655160142..eee329e90fc 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 5c7443d37ab..47f3267657e 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 01876080d5c..532ca3eb628 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 3dea38d70a1..98bf08db29a 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 5f22740b638..fd7d1101bb2 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 fbeda724d70..0df0a6971e9 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 c4a89c4951e..689baf5769f 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 c2bd9a6d566..78a84d59201 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 3d7e763902c..73a16e22e59 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 546c4e7d846..76562013bb8 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 6a56d3e182e..06cbb9c48bd 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 c0ad530b635..c05c6069a58 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 4e83e52e08b..d6178ca6da9 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 6455cd141e5..5fbef083f59 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 1b70959421e..4ce1155c6fc 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 6d3bd0b4fd9..2f50b76336f 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 37a5942b8e5..3fc1aa4b123 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 89cfcb8ea82..56c4ead7681 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 6920ad16262..66d9c0c8c91 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 9899759571f..a0a380750fa 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 c65e202d5f6..1c76b7f262d 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 2db6fe590f8..a740a1612fa 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 8a7f6b37521..c5ad4db6d6b 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 f4f409b2231..6374919dc68 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 48449b62e49..982fefc8d4b 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 3bdcb7f459f..06c8b4708f3 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 64a6a02b043..4f135df4cd3 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 84559a6dd0e..17783e40e74 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 67505dcb5c5..d279c36d638 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 7b836a362ab..e2246cea6b2 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 40255d6fc4b..2b066df7a37 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 b7c2460da5e..9dc7a88aaab 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 e402347bb7f..73ed0516b26 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 fb6a559a080..645bedb5c60 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 5d37997bb66..188fe594ffe 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 2aa37b76715..e76d3c058de 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 1b02aa00afd..e371f48937e 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 e0b3215a1bc..b1ee544dda1 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 bb5f9ad8f3e..dd13e947665 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 c9b971ff32f..dea6b22f244 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 7e325174854..8797931a06e 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 eaa6a845adf..1ebb2698f42 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 dcd88018b20..f384bf00de1 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 c64d82f7057..a6605ccc1e3 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 4265d80c2eb..545adc2369a 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 6293804566c..45cbb5e314d 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 db107f75b48..0c3bb1c4158 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 6571fc60e01..b0b68136917 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
--
GitLab