[wp] fix test related to missing RTE alarm

src/plugins/wp/tests/wp_gallery/euclid.c

@@ -29,6 +29,7 @@ int euclid_gcd(int a, int b)
   int r;
   /*@
     loop assigns a, b, r;
+    loop invariant \abs(a) <= INT_MAX && \abs(b) <= INT_MAX ;
     loop invariant gcd(a,b) == \at( gcd(a,b), Pre );
     loop variant \abs(b);
   */

src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle

@@ -4,7 +4,7 @@
 [rte:annot] annotating function euclid_gcd
 [wp] [Valid] Goal euclid_gcd_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal euclid_gcd_terminates (Cfg) (Trivial)
-[wp] 16 goals scheduled
+[wp] 19 goals scheduled
 [wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
 [wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
 [wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
@@ -13,21 +13,24 @@
 [wp] [Valid] typed_euclid_euclid_gcd_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_established (Qed)
+[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_2_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_2_established (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assert_rte_division_by_zero (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assert_rte_signed_overflow (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_euclid_gcd_assert_rte_signed_overflow_2 (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_assigns (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assigns_part1 (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assigns_part2 (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assigns_part3 (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_variant_decrease (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_variant_positive (Qed)
-[wp] Proved goals:   18 / 18
+[wp] Proved goals:   21 / 21
   Terminating:     1
   Unreachable:     1
-  Qed:             7
-  Alt-Ergo:        9
+  Qed:             8
+  Alt-Ergo:       11
   Smoke Tests:     5 / 5
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  euclid_gcd                7        9       16       100%
+  euclid_gcd                8       11       19       100%
 ------------------------------------------------------------