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

diff --git a/test/regression/2007-08-16-valid-write-to-freed-object.c b/test/regression/2007-08-16-valid-write-to-freed-object.c
new file mode 100644
index 00000000..472b7de8
--- /dev/null
+++ b/test/regression/2007-08-16-valid-write-to-freed-object.c
@@ -0,0 +1,24 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+
+unsigned sym() {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+  return x;
+}
+
+int main() {
+  unsigned x, y;
+
+  // sym returns a symbolic object, but because it is
+  // alloca'd it is freed on sym()s return. thats fine,
+  // but the problem is that IVC is going to try to write
+  // into the object right here.
+  //
+  // to support this we need to have a facility for making
+  // state local copies of a freed object.
+  if (sym() == 0) 
+    printf("ok\n");
+
+  return 0;
+}