Skip to content
Snippets Groups Projects
Commit c866a933 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] updating qualif logs without driver

parent 4d463015
No related branches found
No related tags found
No related merge requests found
Showing
with 0 additions and 20 deletions
# 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
[wp] 15 goals scheduled
[wp] [Qed] Goal typed_loop_continue_loop_invariant_preserved : Valid
......
# 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
[wp] [Alt-Ergo] Goal typed_f_ensures : Valid
......
......@@ -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
[wp] 1 goal scheduled
[wp] [Qed] Goal typed_empty_assert : Valid
......
# frama-c -wp -wp-timeout 1 [...]
[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 -wp-steps 50 [...]
[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_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
[kernel] tests/wp/wp_call_pre.c:53: Warning:
......
# 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] [Alt-Ergo] Goal typed_f_ensures : Valid
......
......@@ -9,7 +9,6 @@
[rte] annotating function spec_if_cond
[rte] annotating function spec_if_not_cond
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] 25 goals scheduled
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko1 : Unsuccess
[wp] [Alt-Ergo] Goal hoare_bts0513_ensures_qed_ko_ko2 : Unsuccess
......
# 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
[wp] 24 goals scheduled
[wp] [Alt-Ergo] Goal typed_lemma_ASSOC_land_qed_ok : Valid
......
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/arith.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
......
# 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
[wp] 4 goals scheduled
[wp] [Qed] Goal typed_jobA_assigns_exit : Valid
......
# 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
[wp] 42 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
......
# 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
[wp] 22 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_CHECK : Valid
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memtyped.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_FAIL : Unsuccess
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigned_not_initialized_memvar.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 3 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_check_FAIL : Unsuccess
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigns_path.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 9 goals scheduled
[wp] [Qed] Goal typed_job_ensures_N : Valid
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 17 goals scheduled
[wp] [Qed] Goal typed_call_assigns_all_assigns_exit_part1 : Valid
......
# frama-c -wp -wp-steps 50 [...]
[kernel] Parsing tests/wp_acsl/assigns_range.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 6 goals scheduled
[wp] [Alt-Ergo] Goal typed_call_assigns_t1_assigns_exit : Unsuccess
......
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/axioms.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
[wp] 10 goals scheduled
[wp] [Alt-Ergo] Goal typed_f_ensures_P_todo : Unsuccess
......
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