binary_seaech regression test for loop contracts

Author: SaswatPadhi

regression/contracts/loop_contracts_binary_search/main.c

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+#define NOT_FOUND (-1)
+
+int binary_search(int val, int *buf, int size)
+{
+  if(size <= 0 || buf == NULL)
+    return NOT_FOUND;
+
+  long long lb = 0, ub = size - 1;
+  long long mid = (lb + ub) / 2;
+
+  while(lb <= ub)
+    // clang-format off
+    __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size)
+    __CPROVER_loop_invariant(mid == (lb + ub) / 2L)
+    __CPROVER_decreases(ub - lb)
+    // clang-format on
+    {
+      if(buf[mid] == val)
+        break;
+      if(buf[mid] < val)
+        lb = mid + 1;
+      else
+        ub = mid - 1;
+      mid = (lb + ub) / 2;
+    }
+  return lb > ub ? NOT_FOUND : mid;
+}
+
+int main()
+{
+  int val, size;
+  int *buf = size >= 0 ? malloc(size * sizeof(int)) : NULL;
+
+  int idx = binary_search(val, buf, size);
+  if(idx != NOT_FOUND)
+    assert(buf[idx] == val);
+}

regression/contracts/loop_contracts_binary_search/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--apply-loop-contracts _ --pointer-check --bounds-check --signed-overflow-check
+^EXIT=0$
+^SIGNAL=0$
+^\[binary_search.1\] .* Check loop invariant before entry: SUCCESS$
+^\[binary_search.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[binary_search.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.assertion.1\] .* assertion buf\[idx\] == val: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test case verifies memory safety and termination of a binary search implementation.