From d94344bce8a21e741ec72947da27cc5bd91a1d13 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 8 Mar 2021 15:11:55 +0100
Subject: [PATCH] [wp] added euclid to gallery
---
src/plugins/wp/tests/wp_gallery/euclid.c | 41 +++++++++++++++++++
src/plugins/wp/tests/wp_gallery/euclid.wp | 3 ++
.../oracle_qualif/euclid.res.oracle | 28 +++++++++++++
3 files changed, 72 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_gallery/euclid.c
create mode 100644 src/plugins/wp/tests/wp_gallery/euclid.wp
create mode 100644 src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
diff --git a/src/plugins/wp/tests/wp_gallery/euclid.c b/src/plugins/wp/tests/wp_gallery/euclid.c
new file mode 100644
index 00000000000..257d8c9ba2f
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/euclid.c
@@ -0,0 +1,41 @@
+/*
+ run.config
+ DONTRUN:
+ */
+
+/*
+ run.config_qualif
+ OPT: -wp-rte -wp-smoke-tests -wp-driver tests/wp_gallery/euclid.wp
+*/
+
+/*@
+ axiomatic Euclid {
+ logic integer gcd(integer a, integer b);
+ }
+*/
+
+
+#include <limits.h>
+
+/*@
+ requires \abs(a) <= INT_MAX ;
+ requires \abs(b) <= INT_MAX ;
+ assigns \nothing;
+ ensures \result == gcd(a,b);
+*/
+
+int euclid_gcd(int a, int b)
+{
+ int r;
+ /*@
+ loop assigns a, b, r;
+ loop invariant gcd(a,b) == \at( gcd(a,b), Pre );
+ loop variant \abs(b);
+ */
+ while( b != 0 ) {
+ r = b ;
+ b = a % b ;
+ a = r ;
+ }
+ return a < 0 ? -a : a;
+}
diff --git a/src/plugins/wp/tests/wp_gallery/euclid.wp b/src/plugins/wp/tests/wp_gallery/euclid.wp
new file mode 100644
index 00000000000..e25b8d00adb
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/euclid.wp
@@ -0,0 +1,3 @@
+library Euclid:
+why3.import += "number.Gcd";
+logic integer gcd(integer, integer) = "Gcd.gcd" ;
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
new file mode 100644
index 00000000000..47d45d1b0ed
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
@@ -0,0 +1,28 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_gallery/euclid.c (with preprocessing)
+[wp] Running WP plugin...
+[rte] annotating function euclid_gcd
+[wp] 16 goals scheduled
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_default_requires
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_code_s6
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_code_s11
+[wp] [Passed] Smoke-test typed_euclid_euclid_gcd_wp_smoke_dead_code_s12
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_ensures : Valid
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assert_rte_division_by_zero : Valid
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_loop_assigns : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assigns_part1 : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assigns_part2 : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_assigns_part3 : Valid
+[wp] [Alt-Ergo] Goal typed_euclid_euclid_gcd_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_euclid_euclid_gcd_loop_variant_positive : Valid
+[wp] Proved goals: 16 / 16
+ Qed: 7
+ Alt-Ergo: 9
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ euclid_gcd 7 9 16 100%
+------------------------------------------------------------
--
GitLab