From 38986ffc03c40da2ab32972d0b87684b00d0a7c1 Mon Sep 17 00:00:00 2001
From: Kilyan Le Gallic <kilyan.legallic@cea.fr>
Date: Wed, 31 Jul 2024 16:29:20 +0200
Subject: [PATCH] [wp] Added tests for Why3 integration, oracles missing
---
src/plugins/wp/tests/wp_gallery/euclid3.c | 43 +++++++++++++++++++
.../wp/tests/wp_gallery/external-import.c | 23 ++++++++++
2 files changed, 66 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_gallery/euclid3.c
create mode 100644 src/plugins/wp/tests/wp_gallery/external-import.c
diff --git a/src/plugins/wp/tests/wp_gallery/euclid3.c b/src/plugins/wp/tests/wp_gallery/euclid3.c
new file mode 100644
index 00000000000..8276d9682a6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/euclid3.c
@@ -0,0 +1,43 @@
+#include <limits.h>
+
+//@ import why3: number::Gcd;
+
+//@ import why3: int::MinMax;
+
+/*@
+ requires \abs(a) <= INT_MAX ;
+ requires \abs(b) <= INT_MAX ;
+ assigns \nothing;
+ ensures \result == Gcd::gcd(a,b);
+*/
+
+int euclid_gcd(int a, int b)
+{
+ int r;
+ /*@
+ loop assigns a, b, r;
+ loop invariant Gcd::gcd(a,b) == \at( Gcd::gcd(a,b), Pre );
+ loop variant \abs(b);
+ */
+ while( b != 0 ) {
+ r = b ;
+ b = a % b ;
+ a = r ;
+ }
+ return a < 0 ? -a : a;
+}
+
+/*@
+ requires \abs(a) <= INT_MAX;
+ requires \abs(b) <= INT_MAX;
+ requires \abs(c) <= INT_MAX;
+ requires \abs(d) <= INT_MAX;
+ assigns \nothing;
+ ensures \result == Gcd::gcd(MinMax::min(a,b), MinMax::max(c,d) );
+*/
+int minmax_gcd(int a, int b, int c, int d)
+{
+ int x = (a > b) ? b : a;
+ int y = (c > d) ? c : d;
+ return euclid_gcd(x,y);
+}
diff --git a/src/plugins/wp/tests/wp_gallery/external-import.c b/src/plugins/wp/tests/wp_gallery/external-import.c
new file mode 100644
index 00000000000..1751fa49264
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/external-import.c
@@ -0,0 +1,23 @@
+#include <limits.h>
+
+//@ import why3: summodule::Sum;
+
+/*@
+ requires \abs(a) <= INT_MAX ;
+ requires \abs(b) <= INT_MAX ;
+ assigns \nothing;
+ ensures \result == Sum::sum(a,b);
+*/
+int sum (int a, int b) {
+
+ /*@
+ loop assigns a, b;
+ loop invariant a <= a + b;
+ loop variant b;
+ */
+ while( b != 0){
+ a+=1;
+ b-=1;
+ }
+ return a;
+}
--
GitLab