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
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
#include <klee/klee.h>
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <assert.h>
static void insert_ordered(int *array, unsigned nelem, int item) {
unsigned i = 0;
for (; i != nelem; ++i) {
if (item < array[i]) {
memmove(&array[i+1], &array[i], sizeof(*array) * (nelem - i));
break;
}
}
array[i] = item;
}
void bubble_sort(int *array, unsigned nelem) {
for (;;) {
int done = 1;
for (unsigned i = 0; i + 1 < nelem; ++i) {
if (array[i+1] < array[i]) {
int t = array[i + 1];
array[i + 1] = array[i];
array[i] = t;
done = 0;
}
}
break;
}
}
void insertion_sort(int *array, unsigned nelem) {
int *temp = malloc(sizeof(*temp) * nelem);
for (unsigned i = 0; i != nelem; ++i)
insert_ordered(temp, i, array[i]);
memcpy(array, temp, sizeof(*array) * nelem);
free(temp);
}
void test(int *array, unsigned nelem) {
int *temp1 = malloc(sizeof(*array) * nelem);
int *temp2 = malloc(sizeof(*array) * nelem);
printf("input: [%d, %d, %d, %d]\n",
array[0], array[1], array[2], array[3]);
memcpy(temp1, array, sizeof(*array) * 4);
memcpy(temp2, array, sizeof(*array) * 4);
insertion_sort(temp1, 4);
bubble_sort(temp2, 4);
printf("insertion_sort: [%d, %d, %d, %d]\n",
temp1[0], temp1[1], temp1[2], temp1[3]);
printf("bubble_sort : [%d, %d, %d, %d]\n",
temp2[0], temp2[1], temp2[2], temp2[3]);
for (unsigned i = 0; i != nelem; ++i)
assert(temp1[i] == temp2[i]);
free(temp1);
free(temp2);
}
int main() {
int input[4] = { 4, 3, 2, 1};
klee_make_symbolic(&input, sizeof(input), "input");
test(input, 4);
return 0;
}
|
