Merge branch 'feature/patrick/wp-find-ptr-example' into 'master'

[wp/tests] adds find_ptr example

See merge request frama-c/frama-c!2505

src/plugins/wp/tests/README.md

+# How to add a new test
+
+```
+cd src/plugins/wp
+git add tests/wp_gallery/find.i
+```
+
+## Update oracle for default configuration
+
+1. generate oracle files
+```
+ptests.opt tests/wp_gallery/find.i -show
+ptests.opt tests/wp_gallery/find.i -update
+```
+
+2. check again (for a final validation) before adding the oracle files
+```
+ptests.opt tests/wp_gallery/find.i
+git add tests/wp_gallery/oracle/find.*
+```
+
+## Update oracle for 'qualif' configuration (if there is such)
+
+1. generate oracle files and updated cache files
+```
+FRAMAC_WP_CACHE=update ptests.opt -config qualif tests/wp_gallery/find.i -show
+ptests.opt -config qualif tests/wp_gallery/find.i -update
+```
+
+Note: cleaning the cache is _not_ recommanded when updating or modifying an
+existing test; actually it might introduce git merge conflicts that are
+annoying to resolve. But the cleaning can be usefull when adding a new test.
+It can be done using the command (before those of the step 1):
+```
+rm -rf tests/wp_gallery/oracle_qualif/find.[0-9]*.session/cache/
+```
+
+2. check again (for a final validation) before adding the oracle and cache files
+```
+ptests.opt -config qualif tests/wp_gallery/find.i
+git add tests/wp_gallery/oracle_qualif/find.*
+```

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.0.session/cache/081f176e0fb3514fde320ca30f2ed032.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0233,
+  "steps": 69 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/18d8398601f0b7f85e551f1c1d9137df.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0126,
+  "steps": 29 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/257633c0e6e4c90dbbb56430d547f891.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0125,
+  "steps": 58 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2ba9be92a508348223e7c319004017c5.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0812,
+  "steps": 221 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/2c3c7fa586fc9ecea4bbf0fb98aa925f.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0062,
+  "steps": 25 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/34f0cce3d0a30b5a3b6408ef7e1f66dd.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0108,
+  "steps": 29 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3974383ae185871e55bfcf7246735ec2.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0194,
+  "steps": 61 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/3adced65475fd2200b005fdcdd713dc3.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0102,
+  "steps": 41 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/51b6e40bd79f42701fd59c85017e8c67.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0278,
+  "steps": 106 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/5ac49d42d9ca3323758823bcf455a64a.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0084,
+  "steps": 20 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/76c334c73d313cc80db5f546c34b680a.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0237,
+  "steps": 79 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/78d3c10c9f4d515da47f9cfa8cd5f089.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0055,
+  "steps": 13 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/7d831c16cfa87e08b115470eafa6f297.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0094,
+  "steps": 45 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/8b7a4ef053798c5fe79c2441519c622c.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0103,
+  "steps": 47 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/90c73ba96bd8257920ff21223c812125.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0088,
+  "steps": 17 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/98854ec13622e5ec44ff5b7522d9f26f.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.03,
+  "steps": 120 }

src/plugins/wp/tests/wp_gallery/oracle_qualif/find.0.session/cache/9c5eb1b10b9b274dd4fbf3d5e8df3d69.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.009,
+  "steps": 36 }