[wp/tests] adds find_ptr example

src/plugins/wp/tests/wp_gallery/find.i

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

src/plugins/wp/tests/wp_gallery/oracle/find.res.oracle

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

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

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