Skip to content
Snippets Groups Projects
Commit 1e6c5176 authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[tests] update prove config for Aorai's tests

parent 247f8158
No related branches found
No related tags found
No related merge requests found
Showing
with 28 additions and 28 deletions
[kernel] Parsing tests/aorai_ltl/goto.c (with preprocessing)
[kernel] Parsing tests/ltl/goto.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] tests/aorai_ltl/goto.c:28: Warning:
[aorai] tests/ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_goto_0.i (no preprocessing)
[wp] TMPDIR/aorai_goto_0.i:4: Warning:
......
[kernel] Parsing tests/aorai_ltl/test_boucle.c (with preprocessing)
[kernel:typing:implicit-function-declaration] tests/aorai_ltl/test_boucle.c:16: Warning:
[kernel] Parsing tests/ltl/test_boucle.c (with preprocessing)
[kernel:typing:implicit-function-declaration] tests/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 TMPDIR/aorai_test_boucle_0.i (no preprocessing)
......
[kernel] Parsing tests/aorai_ltl/test_boucle1.c (with preprocessing)
[kernel] Parsing tests/ltl/test_boucle1.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle1_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_boucle1_0.i:3: Warning:
......
[kernel] Parsing tests/aorai_ltl/test_boucle2.c (with preprocessing)
[kernel] Parsing tests/ltl/test_boucle2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle2_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_boucle2_0.i:4: Warning:
......
[kernel] Parsing tests/aorai_ltl/test_boucle3.c (with preprocessing)
[kernel] Parsing tests/ltl/test_boucle3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_boucle3_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_boucle3_0.i:4: Warning:
......
[kernel] Parsing tests/aorai_ltl/test_factorial.c (with preprocessing)
[kernel] Parsing tests/ltl/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_factorial_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ltl/test_recursion1.c (with preprocessing)
[kernel] tests/aorai_ltl/test_recursion1.c:21: Warning:
[kernel] Parsing tests/ltl/test_recursion1.c (with preprocessing)
[kernel] tests/ltl/test_recursion1.c:21: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/aorai_ltl/test_recursion1.c:42: Warning:
[kernel] tests/ltl/test_recursion1.c:42: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[kernel] tests/aorai_ltl/test_recursion1.c:54: Warning:
[kernel] tests/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 TMPDIR/aorai_test_recursion1_0.i (no preprocessing)
......
[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion2_0.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
......
[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[kernel] Parsing tests/ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_recursion2_1.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
......
[kernel] Parsing tests/aorai_ltl/test_switch2.c (with preprocessing)
[kernel] Parsing tests/ltl/test_switch2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] tests/aorai_ltl/test_switch2.c:34: Warning:
[aorai] tests/ltl/test_switch2.c:34: Warning:
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:
[aorai] tests/ltl/test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing TMPDIR/aorai_test_switch2_0.i (no preprocessing)
[wp] TMPDIR/aorai_test_switch2_0.i:4: Warning:
......
[kernel] Parsing tests/aorai_ltl/test_switch3.c (with preprocessing)
[kernel] Parsing tests/ltl/test_switch3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ltl/test_switch3_et_recursion.c (with preprocessing)
[kernel] Parsing tests/ltl/test_switch3_et_recursion.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] tests/aorai_ltl/test_switch3_et_recursion.c:26: Warning:
[aorai] tests/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 TMPDIR/aorai_test_switch3_et_recursion_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ltl/test_switch3_if.c (with preprocessing)
[kernel] Parsing tests/ltl/test_switch3_if.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_if_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ltl/test_switch3_return.c (with preprocessing)
[kernel] Parsing tests/ltl/test_switch3_return.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_test_switch3_return_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_assigns_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_assigns_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[kernel] Parsing tests/ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
/* Generated by Frama-C */
int X;
......
[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[kernel] Parsing tests/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 TMPDIR/aorai_bts1289_0.i (no preprocessing)
......
[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[kernel] Parsing tests/ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_bts1289_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel] Parsing tests/aorai_ya/declared_function.i (no preprocessing)
[kernel] Parsing tests/ya/declared_function.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:48: Warning:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment