[wp] added euclid to gallery

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

+/*
+  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;
+}

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

+library Euclid:
+why3.import += "number.Gcd";
+logic integer gcd(integer, integer) = "Gcd.gcd" ;

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

+# 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%
+------------------------------------------------------------