Skip to content
Snippets Groups Projects
Commit bf3fcc8e authored by Allan Blanchard's avatar Allan Blanchard
Browse files

[wp] update oracles

parent 14293eab
No related branches found
No related tags found
No related merge requests found
[kernel] Parsing hoare_seq.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_hoare_seq_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
[kernel:annot:missing-spec] TMPDIR/aorai_hoare_seq_0_prove.i:358: Warning:
Neither code nor explicit exits and terminates for function main_bhv_bhv,
generating default clauses. See -generated-spec-* options for more info
......@@ -3,11 +3,15 @@
[kernel:annot-error] classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_f_ensures (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] Proved goals: 2 / 2
[wp] Proved goals: 4 / 4
Terminating: 1
Unreachable: 1
Qed: 2
[report] Classification
[report] Output classified.0.json
......
......@@ -4,11 +4,15 @@
[kernel:annot-error] classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_f_ensures (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] Proved goals: 2 / 2
[wp] Proved goals: 4 / 4
Terminating: 1
Unreachable: 1
Qed: 2
[report] Classification
[report] Output classified.1.json
......
......@@ -4,11 +4,15 @@
[kernel:annot-error] classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_f_ensures (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] Proved goals: 2 / 2
[wp] Proved goals: 4 / 4
Terminating: 1
Unreachable: 1
Qed: 2
[report] Classification
[report] Output classified.2.json
......
......@@ -5,11 +5,15 @@
[kernel:annot-error] classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_f_ensures (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] Proved goals: 2 / 2
[wp] Proved goals: 4 / 4
Terminating: 1
Unreachable: 1
Qed: 2
[report] Classification
[report] Output classified.3.json
......
......@@ -5,11 +5,15 @@
[kernel:annot-error] classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_f_ensures (Qed)
[wp] [Valid] typed_f_assigns (Qed)
[wp] Proved goals: 2 / 2
[wp] Proved goals: 4 / 4
Terminating: 1
Unreachable: 1
Qed: 2
[report] Classification
[report] Output classified.4.json
......
......@@ -5,6 +5,8 @@
[kernel:annot-error] classify.c:28: Warning:
unbound logic variable ignored. Ignoring code annotation
[wp] Running WP plugin...
[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
[wp] Warning: Missing RTE guards
[wp] Goal typed_f_ensures : not tried
[wp] Goal typed_f_assigns : trivial
......
......@@ -63,10 +63,10 @@
------------------------------------------------------------
[wp] Running WP plugin...
[rte:annot] annotating function find
[wp] [Valid] Goal find_terminates (Cfg) (Trivial)
[rte:annot] annotating function find_ptr
[wp] [Valid] Goal find_ptr_terminates (Cfg) (Trivial)
[rte:annot] annotating function iter_ptr
[wp] [Valid] Goal find_terminates (Cfg) (Trivial)
[wp] [Valid] Goal find_ptr_terminates (Cfg) (Trivial)
[wp] [Valid] Goal iter_ptr_terminates (Cfg) (Trivial)
[wp] 3 goals scheduled
[wp] [Valid] typed_find_assert_rte_mem_access (Alt-Ergo) (Cached)
......
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