[wp] added bsearch to gallery

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

+/* run.config
+   DONTRUN:
+*/
+
+/* run.config_qualif
+   OPT: -wp-rte -wp-smoke-tests
+ */
+
+
+/*@
+  requires size >= 0;
+  requires \valid(t + (0 .. size-1));
+  requires ∀ integer i, integer j; 0 <= i <= j < size ==> t[i] <= t[j];
+  ensures Result: -1 <= \result < size;
+  ensures Found: \result >= 0 ==> t[\result] == key;
+  ensures NotFound: \result == -1 ==> ∀ integer i; 0 <= i < size ==> t[i] != key;
+*/
+int binary_search(int * t, int size, int key)
+{
+  int lo, hi, mid;
+  lo = 0; hi = size - 1;
+  /*@
+    loop assigns lo, hi, mid;
+    loop invariant Range: 0 <= lo && hi < size;
+    loop invariant Left: ∀ integer i; 0 <= i < lo ==> t[i] < key;
+    loop invariant Right: ∀ integer i; hi < i < size ==> t[i] > key;
+    loop variant hi - lo;
+   */
+  while (lo <= hi) {
+    mid = lo + (hi - lo) / 2;
+    if (key == t[mid]) return mid;
+    if (key < t[mid]) hi = mid - 1; else lo = mid + 1;
+  }
+  return -1;
+}

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

+# frama-c -wp -wp-rte [...]
+[kernel] Parsing tests/wp_gallery/bsearch.c (with preprocessing)
+[wp] Running WP plugin...
+[rte] annotating function binary_search
+[wp] 28 goals scheduled
+[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_default_requires
+[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_loop_s3
+[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_code_s8
+[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_code_s12
+[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_code_s16
+[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_code_s17
+[wp] [Passed] Smoke-test typed_binary_search_wp_smoke_dead_code_s18
+[wp] [Alt-Ergo] Goal typed_binary_search_ensures_Result : Valid
+[wp] [Qed] Goal typed_binary_search_ensures_Found : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_ensures_NotFound : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_loop_invariant_Left_preserved : Valid
+[wp] [Qed] Goal typed_binary_search_loop_invariant_Left_established : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_loop_invariant_Range_preserved : Valid
+[wp] [Qed] Goal typed_binary_search_loop_invariant_Range_established : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_loop_invariant_Right_preserved : Valid
+[wp] [Qed] Goal typed_binary_search_loop_invariant_Right_established : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow_2 : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow_3 : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow_4 : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow_5 : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_mem_access : Valid
+[wp] [Qed] Goal typed_binary_search_assert_rte_mem_access_2 : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow_6 : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_assert_rte_signed_overflow_7 : Valid
+[wp] [Qed] Goal typed_binary_search_loop_assigns : Valid
+[wp] [Alt-Ergo] Goal typed_binary_search_loop_variant_decrease : Valid
+[wp] [Qed] Goal typed_binary_search_loop_variant_positive : Valid
+[wp] Proved goals:   28 / 28
+  Qed:             7 
+  Alt-Ergo:       21
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  binary_search             7       21       28       100%
+------------------------------------------------------------