1void __VERIFIER_assert(int cond) {
2 if (!(cond)) {
3 ERROR: goto ERROR;
4 }
5 return;
6}
7
8
9
10
11void bubblesort(int size, int item[])
12{
13 int a, b, t;
14
15 for(a = 1; a < size; ++a)
16 {
17 for(b = size-1; b >= a; --b)
18 {
19
20 if (b-1 < size && b < size)
21 {
22 if(item[ b - 1] > item[ b ])
23 {
24 t = item[ b - 1];
25 item[ b - 1] = item[ b ];
26 item[ b ] = t;
27 }
28 }
29 }
30 }
31}
32
33void bubblesort1(int size, int item[])
34{
35 int j, i, pivot;
36
37 for(j = 1; j < size; ++j)
38 {
39 pivot = item[j];
40 i = j - 1;
41
42 while(i >= 0 && item[i] > pivot)
43 {
44 item[i+1] = item[i];
45 i--;
46 }
47 item[i+1] = pivot;
48 }
49}
50int __VERIFIER_nondet_int();
51void q1(int argc, char* argv[])
52{
53 if(argc < 2)
54 return;
55 int N = __VERIFIER_nondet_int();
56 int a[N];
57 int i;
58 switch(2)
59 {
60 case 0:
61 for(i=0; i < N; ++i) a[i] = i;
62 break;
63 case 1:
64 for(i=(N-1); i >= 0; --i) a[i] = N-1-i;
65 break;
66 case 2:
67 for(i=0; i < N; ++i) a[i] = i;
68 for (i=0; i<N; i++) {
69 int r = i + (__VERIFIER_nondet_int() % (N-i));
70 int temp = a[i];
71 a[i] = a[r];
72 a[r] = temp;
73 }
74 break;
75 }
76 bubblesort(N, a);
77}
78int main (int argc, char* argv[])
79{
80 q1(argc, argv);
81 return 0;
82}