Skip to content
Snippets Groups Projects
Commit c16055ce authored by Allan Blanchard's avatar Allan Blanchard Committed by Andre Maroneze
Browse files

[wp] fix oracle after cache update

parent ffffa4fe
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
+ 8
− 14
View file @ c16055ce
...@@ -53,30 +53,28 @@ ...@@ -53,30 +53,28 @@
[wp] [Valid] typed_stringLength_assigns_part4 (Qed) [wp] [Valid] typed_stringLength_assigns_part4 (Qed)
[wp] [Valid] typed_stringLength_assigns_part5 (Qed) [wp] [Valid] typed_stringLength_assigns_part5 (Qed)
[wp] [Valid] typed_main_terminates (Qed) [wp] [Valid] typed_main_terminates (Qed)
[wp] [NoResult] typed_main_ensures (Qed) [wp] [Valid] typed_main_ensures (Alt-Ergo) (Cached)
[wp] [Valid] typed_main_exits_never (Qed) [wp] [Valid] typed_main_exits_never (Qed)
[wp] [Valid] typed_main_assert (Qed) [wp] [Valid] typed_main_assert (Qed)
[wp] [Valid] typed_main_assigns_exit (Qed) [wp] [Valid] typed_main_assigns_exit (Qed)
[wp] [Valid] typed_main_assigns_normal_part1 (Qed) [wp] [Valid] typed_main_assigns_normal_part1 (Qed)
[wp] [Valid] typed_main_assigns_normal_part2 (Qed) [wp] [Valid] typed_main_assigns_normal_part2 (Qed)
[wp] [NoResult] typed_main_call_stringCompare_requires_validStrings (Qed) [wp] [Valid] typed_main_call_stringCompare_requires_validStrings (Alt-Ergo) (Cached)
[wp] Proved goals: 55 / 57 [wp] Proved goals: 57 / 57
Unreachable: 2 Unreachable: 2
Qed: 36 Qed: 36
Alt-Ergo: 17 Alt-Ergo: 19
Unsuccess: 2
Missing: 2
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
stringCompare 20 13 33 100% stringCompare 20 13 33 100%
stringLength 10 4 14 100% stringLength 10 4 14 100%
main 6 - 8 75.0% main 6 2 8 100%
------------------------------------------------------------ ------------------------------------------------------------
[wp] Running WP plugin... [wp] Running WP plugin...
[rte:annot] annotating function main [rte:annot] annotating function main
[rte:annot] annotating function stringCompare [rte:annot] annotating function stringCompare
[rte:annot] annotating function stringLength [rte:annot] annotating function stringLength
[wp] 10 goals scheduled [wp] 8 goals scheduled
[wp] [Valid] typed_stringCompare_assert_rte_mem_access (Alt-Ergo) (Cached) [wp] [Valid] typed_stringCompare_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [Valid] typed_stringCompare_assert_rte_mem_access_2 (Alt-Ergo) (Cached) [wp] [Valid] typed_stringCompare_assert_rte_mem_access_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_stringCompare_assert_rte_mem_access_3 (Qed) [wp] [Valid] typed_stringCompare_assert_rte_mem_access_3 (Qed)
...@@ -85,16 +83,12 @@ ...@@ -85,16 +83,12 @@
[wp] [Valid] typed_stringCompare_assert_rte_signed_overflow (Alt-Ergo) (Cached) [wp] [Valid] typed_stringCompare_assert_rte_signed_overflow (Alt-Ergo) (Cached)
[wp] [Valid] typed_stringCompare_assert_rte_signed_overflow_2 (Alt-Ergo) (Cached) [wp] [Valid] typed_stringCompare_assert_rte_signed_overflow_2 (Alt-Ergo) (Cached)
[wp] [Valid] typed_stringLength_assert_rte_mem_access (Alt-Ergo) (Cached) [wp] [Valid] typed_stringLength_assert_rte_mem_access (Alt-Ergo) (Cached)
[wp] [NoResult] typed_main_ensures (Qed) [wp] Proved goals: 8 / 8
[wp] [NoResult] typed_main_call_stringCompare_requires_validStrings (Qed)
[wp] Proved goals: 8 / 10
Qed: 2 Qed: 2
Alt-Ergo: 6 Alt-Ergo: 6
Unsuccess: 2
Missing: 2
------------------------------------------------------------ ------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
stringCompare 22 18 40 100% stringCompare 22 18 40 100%
stringLength 10 5 15 100% stringLength 10 5 15 100%
main 6 - 8 75.0% main 6 2 8 100%
------------------------------------------------------------ ------------------------------------------------------------
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