Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 16 insertions, 0 deletions

diff --git a/test/Concrete/ackermann.c b/test/Concrete/ackermann.c
new file mode 100644
index 00000000..0f21a3ab
--- /dev/null
+++ b/test/Concrete/ackermann.c
@@ -0,0 +1,16 @@
+// llvm-gcc -O2 --emit-llvm -c ackermann.c && ../../Debug/bin/klee ackermann.o 2 2
+
+#include <stdio.h>
+
+int ackermann(int m, int n) {
+   if (m == 0)
+     return n+1;
+   else
+     return ackermann(m-1, (n==0) ? 1 : ackermann(m, n-1));
+ }
+
+int main() {
+  printf("ackerman(%d, %d) = %d\n", 2, 2, ackermann(2, 2));
+
+  return 0;
+}