1 files changed, 78 insertions, 0 deletions
diff --git a/examples/sort/sort.c b/examples/sort/sort.c
new file mode 100644
index 00000000..a1629c6b
--- /dev/null
+++ b/examples/sort/sort.c
@@ -0,0 +1,78 @@
+#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]);
+}
+
+int main() {
+  int input[4] = { 4, 3, 2, 1};
+
+  klee_make_symbolic(&input, sizeof(input));
+  test(input, 4);
+
+  return 0;
+}