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

7 files changed, 179 insertions, 0 deletions

diff --git a/test/CXX/ArrayNew.cpp b/test/CXX/ArrayNew.cpp
new file mode 100644
index 00000000..e6a41ddf
--- /dev/null
+++ b/test/CXX/ArrayNew.cpp
@@ -0,0 +1,38 @@
+// RUN: %llvmgxx %s --emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --no-output --exit-on-error --no-externals %t1.bc
+
+#include <cassert>
+
+static int decon = 0;
+
+class Test {
+  int x;
+
+public:
+  Test() {}
+  Test(int _x) : x(_x) { }
+  ~Test() { decon += x; }
+
+  int getX() { return x; }
+  void setX(int _x) { x = _x; }
+};
+
+int main(int argc) {
+  Test *rt = new Test[4];
+  int i;
+
+  for (i=0; i<4; i++)
+    rt[i].setX(i+1);
+
+  int sum = 0;
+  for (i=0; i<4; i++)
+    sum += rt[i].getX();
+  
+  assert(sum==10);
+
+  delete[] rt;
+
+  assert(decon==10);
+
+  return 0;
+}
diff --git a/test/CXX/New.cpp b/test/CXX/New.cpp
new file mode 100644
index 00000000..148dfed6
--- /dev/null
+++ b/test/CXX/New.cpp
@@ -0,0 +1,29 @@
+// RUN: %llvmgxx %s --emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --no-output --exit-on-error --no-externals %t1.bc
+
+#include <cassert>
+
+class Test {
+  int x;
+
+public:
+  Test(int _x) : x(_x) {
+  }
+  ~Test() {
+  }
+
+  int getX() { return x; }
+};
+
+// This doesn't do what I want because
+// it is being changed to alloca, but
+// it is also failing.
+int main(int argc) {
+  Test *rt = new Test(2);
+  
+  assert(rt->getX()==2);
+
+  delete rt;
+
+  return 0;
+}
diff --git a/test/CXX/SimpleVirtual.cpp b/test/CXX/SimpleVirtual.cpp
new file mode 100644
index 00000000..9dc2a0ac
--- /dev/null
+++ b/test/CXX/SimpleVirtual.cpp
@@ -0,0 +1,38 @@
+// RUN: %llvmgxx %s --emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --no-output --exit-on-error --no-externals %t1.bc
+
+#include <cassert>
+
+static int decon = 0;
+
+class Thing {
+public:
+  Thing() {}
+  virtual ~Thing() { decon += getX(); }
+
+  virtual int getX() { return 1; };
+};
+
+class Thing2 : public Thing {
+public:
+  virtual int getX() { return 2; };
+};
+
+Thing *getThing(bool which) { 
+  return which ? new Thing() : new Thing2();
+}
+
+int main(int argc) {
+  Thing *one = getThing(false);
+  Thing *two = getThing(true);
+
+  int x = one->getX() + two->getX();
+  assert(x==3);
+
+  delete two;
+  delete one;
+  
+  assert(decon==2);
+
+  return 0;
+}
diff --git a/test/CXX/StaticConstructor.cpp b/test/CXX/StaticConstructor.cpp
new file mode 100644
index 00000000..d4992ffe
--- /dev/null
+++ b/test/CXX/StaticConstructor.cpp
@@ -0,0 +1,25 @@
+// RUN: %llvmgxx %s --emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --libc=klee --no-output --exit-on-error %t1.bc
+
+#include <cassert>
+
+// to make sure globals are initialized
+int aGlobal = 21;
+
+class Test {
+  int x;
+
+public:
+  Test() : x(aGlobal + 1) {}
+  ~Test() {}
+
+  int getX() { return x; }
+};
+
+Test t;
+
+int main() {
+  assert(t.getX()==22);
+
+  return 0;
+}
diff --git a/test/CXX/StaticDestructor.cpp b/test/CXX/StaticDestructor.cpp
new file mode 100644
index 00000000..7a765a8f
--- /dev/null
+++ b/test/CXX/StaticDestructor.cpp
@@ -0,0 +1,24 @@
+// don't optimize this, llvm likes to turn the *p into unreachable
+
+// RUN: %llvmgxx %s --emit-llvm -g -O0 -c -o %t1.bc
+// RUN: %klee --libc=klee --no-output %t1.bc 2> %t1.log
+// RUN: grep ":16: memory error" %t1.log
+
+#include <cassert>
+
+class Test {
+  int *p;
+
+public:
+  Test() : p(0) {}
+  ~Test() { 
+    assert(!p); 
+    assert(*p == 10); // crash here
+  }
+};
+
+Test t;
+
+int main() {
+  return 0;
+}
diff --git a/test/CXX/Trivial.cpp b/test/CXX/Trivial.cpp
new file mode 100644
index 00000000..b50e82b2
--- /dev/null
+++ b/test/CXX/Trivial.cpp
@@ -0,0 +1,22 @@
+// RUN: %llvmgxx %s --emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --no-output --exit-on-error %t1.bc
+
+#include <cassert>
+
+class Test {
+  int x;
+
+public:
+  Test(int _x) : x(_x) {}
+  ~Test() {}
+
+  int getX() { return x; }
+};
+
+int main() {
+  Test rt(2);
+  
+  assert(rt.getX()==2);
+
+  return 0;
+}
diff --git a/test/CXX/dg.exp b/test/CXX/dg.exp
new file mode 100644
index 00000000..879685ca
--- /dev/null
+++ b/test/CXX/dg.exp
@@ -0,0 +1,3 @@
+load_lib llvm.exp
+
+RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{ll,llx,c,cpp,tr}]]