1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
#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;
int lb = 0, ub = size - 1;
int mid = ((unsigned int)lb + (unsigned int)ub) >> 1;
while(lb <= ub)
// clang-format off
__CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size)
__CPROVER_loop_invariant(mid == ((unsigned int)lb + (unsigned int)ub) >> 1)
__CPROVER_decreases(ub - lb)
// clang-format on
{
if(buf[mid] == val)
break;
if(buf[mid] < val)
lb = mid + 1;
else
ub = mid - 1;
mid = ((unsigned int)lb + (unsigned int)ub) >> 1;
}
return lb > ub ? NOT_FOUND : mid;
}
int main()
{
int val;
char 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);
}
|
