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, 23 insertions, 0 deletions

diff --git a/test/Feature/CheckForImpliedValue.c.failing b/test/Feature/CheckForImpliedValue.c.failing
new file mode 100644
index 00000000..7a088354
--- /dev/null
+++ b/test/Feature/CheckForImpliedValue.c.failing
@@ -0,0 +1,23 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: rm -f %t1.log
+// RUN: %klee --log-file %t1.log --debug-check-for-implied-values %t1.bc
+// RUN: grep "= 0 (ok)" %t1.log
+// RUN: grep "= 2 (missed)" %t1.log
+
+#define swap(x) (((x)>>16) | (((x)&0xFFFF)<<16))
+int main() {
+  unsigned x, y;
+  
+  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&y, sizeof y);
+
+  if (!x) { // should give x = 0 hit by ivc
+    printf("ok\n");
+  } else {
+    if (swap(y) == 0x00020000) { // should give y = 2 missed by ivc
+      printf("ok\n");
+    }
+  }
+
+  return 0;
+}