binary_seaech regression test for loop contracts

Author: SaswatPadhi

regression/contracts/loop_contracts_binary_search/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+#include <stdlib.h>
+#include <stdbool.h>
+
+#define NOT_FOUND (-1)
+
+int binary_search(int val, int *buf, int size)
+{
+  if(size <= 0 || buf == NULL) return NOT_FOUND;
+
+  long lb = 0, ub = size - 1;
+  long mid = (lb + ub) / 2;
+
+  while(lb <= ub)
+  __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size)
+  __CPROVER_loop_invariant(mid == (lb + ub) / 2L)
+  __CPROVER_decreases(ub - lb)
+  {
+     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.