Commit bf8e3fae authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[aorai] make oracles robust to TMPDIR value

parent 0bcdfbdb
......@@ -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();
......
......@@ -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,
......
......@@ -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,
......
[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,
......
[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,
......
[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,
......
[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,
......
......@@ -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,
......
[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,
......
[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,
......
......@@ -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,
......
[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,
......
......@@ -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,
......
[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,
......
[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,
......
......@@ -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
......@@ -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
[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
[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
[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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment