diff --git a/src/plugins/wp/tests/wp_gallery/find.i b/src/plugins/wp/tests/wp_gallery/find.i
new file mode 100644
index 0000000000000000000000000000000000000000..2f23fc18373c6a61a2982656ec97f0e33bc47aea
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/find.i
@@ -0,0 +1,103 @@
+/* run.config
+ OPT: -wp-no-print -wp-rte
+*/
+
+/* run.config_qualif
+ OPT: -then -wp-rte -wp
+*/
+
+/*@ predicate IsValueOk(integer u, integer v) = u == v;
+*/
+
+/*@ predicate InRange(integer start, integer k, integer last) =
+ start <= k <= last;
+*/
+/*@ predicate Found(int * p, integer n, integer v) =
+ \exists integer k;
+ InRange(0,k,n-1) && IsValueOk(p[k],v);
+*/
+
+/*@ requires Natural: 0 <= n;
+ @ requires Valid: \valid(p + (0 .. n-1));
+ @ ensures Range: InRange(0,\result,n);
+ @ ensures NoneBefore: !Found(p,\result,v);
+ @ behavior not_found:
+ assumes ! Found(p,n,v);
+ ensures \result == n ;
+ @ behavior found:
+ assumes Found(p,n,v);
+ ensures \result < n ;
+ ensures IsValueOk(p[\result],v) ;
+ @ disjoint behaviors found, not_found;
+ @ complete behaviors found, not_found;
+ */
+int find(int * p, int n, int v) {
+ int i = 0;
+ /*@ loop assigns i;
+ @ loop invariant Valid: \valid(p + (0 .. i-1));
+ @ loop invariant Range: InRange(0,i,n);
+ @ loop invariant NotFound: !Found(p,i,v);
+ @ loop variant Decrease: n - i;
+ */
+ for (; i < n ; i++)
+ if (p[i] == v)
+ break;
+ return i;
+}
+//----------------------------------------------------------
+/*@ predicate IsValueOk_ptr(int * p, integer v) = *p == v;
+*/
+
+/*@ predicate InRange_ptr(int * start, int * p, int * last) =
+ \base_addr(start) == \base_addr(last)
+ && \base_addr(start) == \base_addr(p)
+ && start <= p <= last ;
+*/
+
+/*@ predicate Found_ptr(int * start, int * last, integer v) =
+ \exists int* pk;
+ InRange_ptr(start, pk, last-1) && IsValueOk_ptr(pk,v);
+*/
+
+/*@ requires Ordered: p <= q && \base_addr(p) == \base_addr(q);
+ @ requires Valid: \valid(p + (0 .. (q-p)-1));
+ @ ensures Range: InRange_ptr(p,\result,q) ;
+ @ ensures NoneBefore: !Found_ptr(p,\result,v);
+ @ behavior not_found:
+ assumes !Found_ptr(p,q,v);
+ ensures \result == q;
+ @ behavior found:
+ assumes Found_ptr(p,q,v);
+ ensures \result < q ;
+ ensures IsValueOk_ptr(\result,v) ;
+ @ disjoint behaviors found, not_found;
+ @ complete behaviors found, not_found;
+ */
+int * find_ptr(int * p, int * q, int v) {
+ /*@ loop assigns p;
+ @ loop invariant Valid: \valid(\at(p,LoopEntry) + (0 .. (\at(p,LoopEntry)-p-1)));
+ @ loop invariant Range: InRange_ptr(\at(p,LoopEntry),p,q);
+ @ loop invariant NotFound: !Found_ptr(\at(p,LoopEntry),p,v);
+ @ loop variant Decrease: q - p;
+ */
+ for (; p < q; p++) {
+ if (*p == v)
+ //@ assert Hack: IsValueOk_ptr(p,v);
+ break;
+ }
+ return p;
+}
+//----------------------------------------------------------
+/*@ requires Ordered: p <= q && \base_addr(p) == \base_addr(q);
+ @ requires Valid: \valid(p + (0 .. (q-p)-1));
+ @ ensures Last: \result == q ;
+*/
+int * iter_ptr(int * p, int * q) {
+ /*@ loop assigns p;
+ @ loop invariant Valid: \valid(\at(p,LoopEntry) + (0 .. (\at(p,LoopEntry)-p-1)));
+ @ loop invariant Range: InRange_ptr(\at(p,LoopEntry),p,q);
+ @ loop variant Decrease: q - p;
+ */
+ for (; p < q ; p++);
+ return p;
+}
diff --git a/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..b4f4caaaf02b52cb3b93f4e6c14e4c309f6fa375
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle
@@ -0,0 +1,51 @@
+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_gallery/find.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[rte] annotating function find
+[rte] annotating function find_ptr
+[rte] annotating function iter_ptr
+[wp] Goal typed_find_complete_found_not_found : trivial
+[wp] Goal typed_find_disjoint_found_not_found : trivial
+[wp] Goal typed_find_ensures_Range : not tried
+[wp] Goal typed_find_ensures_NoneBefore : not tried
+[wp] Goal typed_find_loop_invariant_NotFound_preserved : not tried
+[wp] Goal typed_find_loop_invariant_NotFound_established : not tried
+[wp] Goal typed_find_loop_invariant_Range_preserved : not tried
+[wp] Goal typed_find_loop_invariant_Range_established : not tried
+[wp] Goal typed_find_loop_invariant_Valid_preserved : not tried
+[wp] Goal typed_find_loop_invariant_Valid_established : not tried
+[wp] Goal typed_find_assert_rte_mem_access : not tried
+[wp] Goal typed_find_assert_rte_signed_overflow : not tried
+[wp] Goal typed_find_loop_assigns : trivial
+[wp] Goal typed_find_loop_variant_decrease : not tried
+[wp] Goal typed_find_loop_variant_positive : not tried
+[wp] Goal typed_find_found_ensures : not tried
+[wp] Goal typed_find_found_ensures_2 : not tried
+[wp] Goal typed_find_not_found_ensures : not tried
+[wp] Goal typed_find_ptr_complete_found_not_found : trivial
+[wp] Goal typed_find_ptr_disjoint_found_not_found : trivial
+[wp] Goal typed_find_ptr_ensures_Range : not tried
+[wp] Goal typed_find_ptr_ensures_NoneBefore : not tried
+[wp] Goal typed_find_ptr_loop_invariant_NotFound_preserved : not tried
+[wp] Goal typed_find_ptr_loop_invariant_NotFound_established : not tried
+[wp] Goal typed_find_ptr_loop_invariant_Range_preserved : not tried
+[wp] Goal typed_find_ptr_loop_invariant_Range_established : not tried
+[wp] Goal typed_find_ptr_loop_invariant_Valid_preserved : not tried
+[wp] Goal typed_find_ptr_loop_invariant_Valid_established : not tried
+[wp] Goal typed_find_ptr_assert_rte_mem_access : not tried
+[wp] Goal typed_find_ptr_assert_Hack : not tried
+[wp] Goal typed_find_ptr_loop_assigns : trivial
+[wp] Goal typed_find_ptr_loop_variant_decrease : not tried
+[wp] Goal typed_find_ptr_loop_variant_positive : not tried
+[wp] Goal typed_find_ptr_found_ensures : not tried
+[wp] Goal typed_find_ptr_found_ensures_2 : not tried
+[wp] Goal typed_find_ptr_not_found_ensures : not tried
+[wp] Goal typed_iter_ptr_ensures_Last : not tried
+[wp] Goal typed_iter_ptr_loop_invariant_Range_preserved : not tried
+[wp] Goal typed_iter_ptr_loop_invariant_Range_established : not tried
+[wp] Goal typed_iter_ptr_loop_invariant_Valid_preserved : not tried
+[wp] Goal typed_iter_ptr_loop_invariant_Valid_established : not tried
+[wp] Goal typed_iter_ptr_loop_assigns : trivial
+[wp] Goal typed_iter_ptr_loop_variant_decrease : not tried
+[wp] Goal typed_iter_ptr_loop_variant_positive : not tried
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..8f59a81a8f93dddf21a3b224837935fd374d8993
--- /dev/null
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/find.res.oracle
@@ -0,0 +1,118 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_gallery/find.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 41 goals scheduled
+[wp] [Qed] Goal typed_find_complete_found_not_found : Valid
+[wp] [Qed] Goal typed_find_disjoint_found_not_found : Valid
+[wp] [Qed] Goal typed_find_ensures_Range : Valid
+[wp] [Qed] Goal typed_find_ensures_NoneBefore : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_NotFound_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_NotFound_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Range_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Range_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Valid_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Valid_established : Valid
+[wp] [Qed] Goal typed_find_loop_assigns : Valid
+[wp] [Qed] Goal typed_find_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_find_loop_variant_positive : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_found_ensures : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_found_ensures_2 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_not_found_ensures : Valid
+[wp] [Qed] Goal typed_find_ptr_complete_found_not_found : Valid
+[wp] [Qed] Goal typed_find_ptr_disjoint_found_not_found : Valid
+[wp] [Qed] Goal typed_find_ptr_ensures_Range : Valid
+[wp] [Qed] Goal typed_find_ptr_ensures_NoneBefore : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_NotFound_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_NotFound_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Range_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Range_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Valid_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Valid_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_assert_Hack : Valid
+[wp] [Qed] Goal typed_find_ptr_loop_assigns : Valid
+[wp] [Qed] Goal typed_find_ptr_loop_variant_decrease : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_variant_positive : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_found_ensures : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_found_ensures_2 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_not_found_ensures : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_ensures_Last : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Range_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Range_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Valid_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Valid_established : Valid
+[wp] [Qed] Goal typed_iter_ptr_loop_assigns : Valid
+[wp] [Qed] Goal typed_iter_ptr_loop_variant_decrease : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_variant_positive : Valid
+[wp] Proved goals: 41 / 41
+ Qed: 15
+ Alt-Ergo 2.0.0: 26
+[wp] Report in: 'tests/wp_gallery/oracle_qualif/find.0.report.json'
+[wp] Report out: 'tests/wp_gallery/result_qualif/find.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+find 7 9 (56..80) 16 100%
+find_ptr 6 11 (192..240) 17 100%
+iter_ptr 2 6 (72..96) 8 100%
+-------------------------------------------------------------
+[wp] Running WP plugin...
+[rte] annotating function find
+[rte] annotating function find_ptr
+[rte] annotating function iter_ptr
+[wp] 44 goals scheduled
+[wp] [Qed] Goal typed_find_complete_found_not_found : Valid
+[wp] [Qed] Goal typed_find_disjoint_found_not_found : Valid
+[wp] [Qed] Goal typed_find_ensures_Range : Valid
+[wp] [Qed] Goal typed_find_ensures_NoneBefore : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_NotFound_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_NotFound_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Range_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Range_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Valid_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_loop_invariant_Valid_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_assert_rte_mem_access : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_assert_rte_signed_overflow : Valid
+[wp] [Qed] Goal typed_find_loop_assigns : Valid
+[wp] [Qed] Goal typed_find_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_find_loop_variant_positive : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_found_ensures : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_found_ensures_2 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_not_found_ensures : Valid
+[wp] [Qed] Goal typed_find_ptr_complete_found_not_found : Valid
+[wp] [Qed] Goal typed_find_ptr_disjoint_found_not_found : Valid
+[wp] [Qed] Goal typed_find_ptr_ensures_Range : Valid
+[wp] [Qed] Goal typed_find_ptr_ensures_NoneBefore : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_NotFound_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_NotFound_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Range_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Range_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Valid_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_invariant_Valid_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_assert_rte_mem_access : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_assert_Hack : Valid
+[wp] [Qed] Goal typed_find_ptr_loop_assigns : Valid
+[wp] [Qed] Goal typed_find_ptr_loop_variant_decrease : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_loop_variant_positive : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_found_ensures : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_found_ensures_2 : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_find_ptr_not_found_ensures : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_ensures_Last : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Range_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Range_established : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Valid_preserved : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_invariant_Valid_established : Valid
+[wp] [Qed] Goal typed_iter_ptr_loop_assigns : Valid
+[wp] [Qed] Goal typed_iter_ptr_loop_variant_decrease : Valid
+[wp] [Alt-Ergo 2.0.0] Goal typed_iter_ptr_loop_variant_positive : Valid
+[wp] Proved goals: 29 / 44
+ Qed: 0
+ Alt-Ergo 2.0.0: 29
+[wp] Report in: 'tests/wp_gallery/oracle_qualif/find.0.report.json'
+[wp] Report out: 'tests/wp_gallery/result_qualif/find.0.report.json'
+-------------------------------------------------------------
+Functions WP Alt-Ergo Total Success
+find 7 11 (56..80) 18 100%
+find_ptr 6 12 (192..240) 18 100%
+iter_ptr 2 6 (72..96) 8 100%
+-------------------------------------------------------------