From 3e36a7e1cd3f05785e96e22c3c8f6cdfaf1a7d9c Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 3 Oct 2024 15:55:09 +0200
Subject: [PATCH] [wp] fix test related to missing RTE alarm
---
src/plugins/wp/tests/wp_gallery/euclid.c | 1 +
.../wp_gallery/oracle_qualif/euclid.res.oracle | 13 ++++++++-----
2 files changed, 9 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/tests/wp_gallery/euclid.c b/src/plugins/wp/tests/wp_gallery/euclid.c
index 130896edb86..a2edb06407a 100644
--- a/src/plugins/wp/tests/wp_gallery/euclid.c
+++ b/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);
*/
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
index 5de7d3a8e0a..42c40f083ce 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
+++ 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%
------------------------------------------------------------
--
GitLab