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
43
44
45
46
47
48
49
50
51
|
#include <assert.h>
#include <stdio.h>
#include <string.h>
void sort_items_by_criteria(int *item, int left, int right)
{
int lidx = left, ridx = (left + right) / 2 + 1,
lsize = (left + right) / 2 - left + 1;
int tmp;
if(right - left < 1)
return;
sort_items_by_criteria(item, left, (left + right) / 2);
sort_items_by_criteria(item, (left + right) / 2 + 1, right);
while(ridx <= right && lidx < ridx)
{
if(item[lidx] > item[ridx])
{
tmp = item[ridx];
memmove(item + lidx + 1, item + lidx, lsize * sizeof(int));
item[lidx] = tmp;
++ridx;
++lsize;
}
++lidx;
--lsize;
}
}
int main(int argc, char *argv[])
{
int a[7] = {0};
// CBMC in some past version reported wrong results for 256, -2147221455,
// -2147221455, -2147221455, 16, -2147483600, 16384
a[0] = 256;
a[1] = -2147221455;
a[2] = -2147221455;
a[3] = -2147221455;
a[4] = 16;
a[5] = -2147483600;
a[6] = 16384;
sort_items_by_criteria(a, 0, 6);
printf("%d %d %d %d %d %d %d\n", a[0], a[1], a[2], a[3], a[4], a[5], a[6]);
assert(a[0] == -2147483600);
return 0;
}
|
