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

[tests-wp] update oracles following message change

parent 65215e22
No related branches found
No related tags found
No related merge requests found
Showing
with 0 additions and 20 deletions
# frama-c -wp -wp-rte [...]
[kernel] Parsing tests/wp/bug_rte.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[rte] annotating function bug
------------------------------------------------------------
Function bug
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/cfg_loop.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function loop_continue
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/sharing.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
---------------------------------------------
......
......@@ -3,7 +3,6 @@
[kernel] tests/wp/stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/stmtcompiler_test.i:145: Warning:
No code nor implicit assigns clause for function behavior1, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/stmtcompiler_test_rela.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function empty
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_behav.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] tests/wp/wp_behav.c:172: Warning:
Ignored specification 'for b1' (generalize to all behavior)
[wp] Warning: Missing RTE guards
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_behavior.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function behaviors
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_behavior.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function behaviors
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function g, generating default assigns from the prototype
[kernel] tests/wp/wp_call_pre.c:53: Warning:
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function g, generating default assigns from the prototype
[kernel] tests/wp/wp_call_pre.c:53: Warning:
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[kernel] tests/wp/wp_call_pre.c:53: Warning:
No code nor implicit assigns clause for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
Goal Pre-condition 'qed_ok,Rstmt' at instruction (file tests/wp/wp_call_pre.c, line 47):
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_eqb.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp:print-generated]
......
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing tests/wp/wp_strategy.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function bts0513
......
# frama-c -wp [...]
[kernel] Parsing tests/wp/wp_strategy.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function default_behaviors with behavior default_for_stmt_54
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Global
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assign_array.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function jobA
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function array
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function array
......
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