From c16055ced9a804a5ec9910f7fde560fa6e5cec72 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 13 May 2024 14:55:48 +0200
Subject: [PATCH] [wp] fix oracle after cache update

---
 .../oracle_qualif/string-compare.res.oracle   | 22 +++++++------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
index 230f48f7150..8ed861ca537 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/string-compare.res.oracle
@@ -53,30 +53,28 @@
 [wp] [Valid] typed_stringLength_assigns_part4 (Qed)
 [wp] [Valid] typed_stringLength_assigns_part5 (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_assert (Qed)
 [wp] [Valid] typed_main_assigns_exit (Qed)
 [wp] [Valid] typed_main_assigns_normal_part1 (Qed)
 [wp] [Valid] typed_main_assigns_normal_part2 (Qed)
-[wp] [NoResult] typed_main_call_stringCompare_requires_validStrings (Qed)
-[wp] Proved goals:   55 / 57
+[wp] [Valid] typed_main_call_stringCompare_requires_validStrings (Alt-Ergo) (Cached)
+[wp] Proved goals:   57 / 57
   Unreachable:     2
   Qed:            36
-  Alt-Ergo:       17
-  Unsuccess:       2
-  Missing:         2
+  Alt-Ergo:       19
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   stringCompare            20       13       33       100%
   stringLength             10        4       14       100%
-  main                      6        -        8      75.0%
+  main                      6        2        8       100%
 ------------------------------------------------------------
 [wp] Running WP plugin...
 [rte:annot] annotating function main
 [rte:annot] annotating function stringCompare
 [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_2 (Alt-Ergo) (Cached)
 [wp] [Valid] typed_stringCompare_assert_rte_mem_access_3 (Qed)
@@ -85,16 +83,12 @@
 [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_stringLength_assert_rte_mem_access (Alt-Ergo) (Cached)
-[wp] [NoResult] typed_main_ensures (Qed)
-[wp] [NoResult] typed_main_call_stringCompare_requires_validStrings (Qed)
-[wp] Proved goals:    8 / 10
+[wp] Proved goals:    8 / 8
   Qed:             2
   Alt-Ergo:        6
-  Unsuccess:       2
-  Missing:         2
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   stringCompare            22       18       40       100%
   stringLength             10        5       15       100%
-  main                      6        -        8      75.0%
+  main                      6        2        8       100%
 ------------------------------------------------------------
-- 
GitLab