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

52 files changed, 1498 insertions, 0 deletions

diff --git a/test/Feature/Alias.c b/test/Feature/Alias.c
new file mode 100644
index 00000000..9300e2c7
--- /dev/null
+++ b/test/Feature/Alias.c
@@ -0,0 +1,25 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+
+// Darwin does not have strong aliases.
+// XFAIL: darwin
+
+#include <assert.h>
+
+// alias for global
+int b = 52;
+extern int a __attribute__((alias("b")));
+
+// alias for function
+int __foo() { return 52; }
+extern int foo() __attribute__((alias("__foo")));
+
+int *c = &a;
+
+int main() { 
+  assert(a == 52);
+  assert(foo() == 52);
+  assert(*c == 52);
+  
+  return 0;
+}
diff --git a/test/Feature/AliasFunction.c b/test/Feature/AliasFunction.c
new file mode 100644
index 00000000..e7acfc19
--- /dev/null
+++ b/test/Feature/AliasFunction.c
@@ -0,0 +1,33 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc > %t1.log
+// RUN: grep -c foo %t1.log | grep 5
+// RUN: grep -c bar %t1.log | grep 3
+
+#include <stdio.h>
+#include <stdlib.h>
+
+void foo() { printf("  foo()\n"); }
+void bar() { printf("  bar()\n"); }
+
+int main() {
+  int x;
+  klee_make_symbolic_name(&x, sizeof(x), "x");
+
+  // no aliases
+  foo();
+
+  if (x > 10)
+  {
+    // foo -> bar
+    klee_alias_function("foo", "bar");    
+
+    if (x > 20)
+      foo();
+  }
+  
+  foo();
+
+  // undo
+  klee_alias_function("foo", "foo");
+  foo();
+}
diff --git a/test/Feature/AliasFunctionExit.c b/test/Feature/AliasFunctionExit.c
new file mode 100644
index 00000000..fcaf7e6c
--- /dev/null
+++ b/test/Feature/AliasFunctionExit.c
@@ -0,0 +1,30 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc > %t1.log
+// RUN: grep -c START %t1.log | grep 1
+// RUN: grep -c END %t1.log | grep 2
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <unistd.h>
+
+void start(int x) {
+  printf("START\n");
+  if (x == 53)
+    exit(1);
+}
+
+void end(int status) {
+  klee_alias_function("exit", "exit");
+  printf("END: status = %d\n", status);
+  exit(status);
+}
+
+
+int main() {
+  int x;
+  klee_make_symbolic_name(&x, sizeof(x), "x");
+
+  klee_alias_function("exit", "end");
+  start(x);
+  end(0);
+}
diff --git a/test/Feature/AsmAddresses.c b/test/Feature/AsmAddresses.c
new file mode 100644
index 00000000..a58fc059
--- /dev/null
+++ b/test/Feature/AsmAddresses.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc -g -c -o %t.bc %s
+// RUN: %klee --exit-on-error --use-asm-addresses %t.bc
+// RUN: %llvmgcc -DOVERLAP -g -c -o %t.bc %s
+// RUN: not %klee --exit-on-error --use-asm-addresses %t.bc
+
+#include <assert.h>
+
+
+volatile unsigned char x0 __asm ("0x0021");
+volatile unsigned char whee __asm ("0x0WHEE");
+
+#ifdef OVERLAP
+volatile unsigned int y0 __asm ("0x0030");
+volatile unsigned int y1 __asm ("0x0032");
+#endif
+
+int main() {
+  assert(&x0 == (void*) 0x0021);
+  assert(&whee != (void*) 0x0);
+
+  return 0;
+}
diff --git a/test/Feature/ByteSwap.c b/test/Feature/ByteSwap.c
new file mode 100644
index 00000000..f85ac3b1
--- /dev/null
+++ b/test/Feature/ByteSwap.c
@@ -0,0 +1,16 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --libc=klee --exit-on-error %t1.bc
+
+#include <arpa/inet.h>
+#include <assert.h>
+
+int main() {
+  
+  uint32_t n = 0;
+  klee_make_symbolic(&n, sizeof(n));
+  
+  uint32_t h = ntohl(n);
+  assert(htonl(h) == n);
+  
+  return 0;
+}
diff --git a/test/Feature/CallToUndefinedExternal.cpp b/test/Feature/CallToUndefinedExternal.cpp
new file mode 100644
index 00000000..2f11f29d
--- /dev/null
+++ b/test/Feature/CallToUndefinedExternal.cpp
@@ -0,0 +1,11 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: test -f klee-last/test000001.external.err
+
+extern "C" void poof(void);
+
+int main() {
+  poof();
+
+  return 0;
+}
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;
+}
diff --git a/test/Feature/CheckMemoryAccess.c b/test/Feature/CheckMemoryAccess.c
new file mode 100644
index 00000000..dd6e8745
--- /dev/null
+++ b/test/Feature/CheckMemoryAccess.c
@@ -0,0 +1,26 @@
+// RUN: %llvmgcc -g -c %s -o %t.bc
+// RUN: %klee %t.bc > %t.log
+// RUN: grep -q "good" %t.log
+// RUN: not grep -q "bad" %t.log
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+  char buf[4];
+
+  klee_check_memory_access(&buf, 1);
+  printf("good\n");
+  if (klee_range(0, 2, "range1")) {
+    klee_check_memory_access(0, 1);
+    printf("null pointer deref: bad\n");
+  }
+
+  if (klee_range(0, 2, "range2")) {
+    klee_check_memory_access(buf, 5);
+    printf("oversize access: bad\n");
+  }
+
+  return 0;
+}
diff --git a/test/Feature/CopyOnWrite.c b/test/Feature/CopyOnWrite.c
new file mode 100644
index 00000000..ee3ea15e
--- /dev/null
+++ b/test/Feature/CopyOnWrite.c
@@ -0,0 +1,26 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --use-random-search --exit-on-error %t1.bc
+
+#include <assert.h>
+
+#define N 5
+
+unsigned branches = 0;
+
+void explode(int *ap, int i, int *result) {
+  if (i<N) {
+    (*result)++;
+    if (ap[i]) // just cause a fork
+      branches++; 
+    return explode(ap, i+1, result);
+  }
+}
+
+int main() {
+  int result = 0;
+  int a[N];
+  klee_make_symbolic(a, sizeof a);
+  explode(a,0,&result);
+  assert(result==N);
+  return 0;
+}
diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c
new file mode 100644
index 00000000..1bf44c3f
--- /dev/null
+++ b/test/Feature/DanglingConcreteReadExpr.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: grep "total queries = 2" klee-last/info
+
+#include <assert.h>
+
+int main() {
+  unsigned char x, y;
+
+  klee_make_symbolic(&x, sizeof x);
+  
+  y = x;
+
+  // should be exactly two queries (prove x is/is not 10)
+  // eventually should be 0 when we have fast solver
+  if (x==10) {
+    assert(y==10);
+  }
+
+  klee_silent_exit(0);
+  return 0;
+}
diff --git a/test/Feature/DefineFixedObject.c b/test/Feature/DefineFixedObject.c
new file mode 100644
index 00000000..36822434
--- /dev/null
+++ b/test/Feature/DefineFixedObject.c
@@ -0,0 +1,17 @@
+// RUN: %llvmgcc -c -o %t1.bc %s
+// RUN: %klee --exit-on-error %t1.bc
+
+#include <stdio.h>
+
+#define ADDRESS ((int*) 0x0080)
+
+int main() {
+  klee_define_fixed_object(ADDRESS, 4);
+  
+  int *p = ADDRESS;
+
+  *p = 10;
+  printf("*p: %d\n", *p);
+
+  return 0;
+}
diff --git a/test/Feature/DoubleFree.c b/test/Feature/DoubleFree.c
new file mode 100644
index 00000000..3727ef2b
--- /dev/null
+++ b/test/Feature/DoubleFree.c
@@ -0,0 +1,10 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: test -f klee-last/test000001.ptr.err
+
+int main() {
+  int *x = malloc(4);
+  free(x);
+  free(x);
+  return 0;
+}
diff --git a/test/Feature/DumpStatesOnHalt.c b/test/Feature/DumpStatesOnHalt.c
new file mode 100644
index 00000000..7e9cf46a
--- /dev/null
+++ b/test/Feature/DumpStatesOnHalt.c
@@ -0,0 +1,8 @@
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --stop-after-n-instructions=1 --dump-states-on-halt=true %t1.bc
+// RUN: test -f klee-last/test000001.bout
+
+int main() {
+  int x = 10;
+  return x;
+}
diff --git a/test/Feature/Envp.c b/test/Feature/Envp.c
new file mode 100644
index 00000000..f1f62a72
--- /dev/null
+++ b/test/Feature/Envp.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+
+#include <assert.h>
+
+int main(int argc, char **argv, char **envp) {
+  unsigned i;
+  assert(argv[argc] == 0);
+  printf("argc: %d, argv: %p, envp: %p\n", argc, argv, envp);
+  printf("--environ--\n");
+  int haspwd = 0;
+  for (i=0; envp[i]; i++) {
+    printf("%d: %s\n", i, envp[i]);
+    haspwd |= strncmp(envp[i], "PWD=", 4)==0;
+  }
+  assert(haspwd);
+  return 0;
+}
diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c
new file mode 100644
index 00000000..2abf0070
--- /dev/null
+++ b/test/Feature/ExprLogging.c
@@ -0,0 +1,43 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
+// RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log
+// RUN: %kleaver -print-ast klee-last/test000001.pc
+
+// FIXME: Ideally we would verify a roundtrip that we parsed the pc
+// file and can dump it back out as the same file.
+
+#include <assert.h>
+
+int constantArr[16 ] = {
+  1 <<  0, 1 <<  1, 1 <<  2, 1 <<  3,
+  1 <<  4, 1 <<  5, 1 <<  6, 1 <<  7,
+  1 <<  8, 1 <<  9, 1 << 10, 1 << 11,
+  1 << 12, 1 << 13, 1 << 14, 1 << 15
+};
+
+
+int main() {
+  char buf[4];
+  klee_make_symbolic(buf, sizeof buf);
+
+  buf[1] = 'a';
+
+  constantArr[klee_range(0, 16, "idx.0")] = buf[0];
+
+  // Use this to trigger an interior update list usage.
+  int y = constantArr[klee_range(0, 16, "idx.1")];  
+
+  constantArr[klee_range(0, 16, "idx.2")] = buf[3];
+  
+  buf[klee_range(0, 4, "idx.3")] = 0;
+  klee_assume(buf[0] == 'h');
+  
+  int x = *((int*) buf);
+  klee_assume(x > 2);
+  klee_assume(x == constantArr[12]);
+
+  klee_assume(y != (1 << 5));
+
+  assert(0);
+
+  return 0;
+}
diff --git a/test/Feature/ExternalWeakLinkage.c b/test/Feature/ExternalWeakLinkage.c
new file mode 100644
index 00000000..c2008136
--- /dev/null
+++ b/test/Feature/ExternalWeakLinkage.c
@@ -0,0 +1,11 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+
+#include <assert.h>
+
+void __attribute__((weak)) IAmSoWeak(int);
+
+int main() {
+  assert(IAmSoWeak==0);
+  return 0;
+}
diff --git a/test/Feature/FunctionPointer.c b/test/Feature/FunctionPointer.c
new file mode 100644
index 00000000..e1ae1e37
--- /dev/null
+++ b/test/Feature/FunctionPointer.c
@@ -0,0 +1,36 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --no-output --exit-on-error %t1.bc
+
+#include <stdio.h>
+
+void foo(const char *msg) { printf("foo: %s\n", msg); }
+void baz(const char *msg) { printf("baz: %s\n", msg); }
+
+void (*xx)(const char *) = foo;
+
+void bar(void (*fp)(const char *)) { fp("called via bar"); }
+
+int main(int argc, char **argv) {
+  void (*fp)(const char *) = foo;
+
+  printf("going to call through fp\n");
+  fp("called via fp");
+
+  printf("calling via pass through\n");
+  bar(foo);
+        
+  fp = baz;
+  fp("called via fp");
+
+  xx("called via xx");
+
+#if 0
+  klee_make_symbolic(&fp, sizeof fp);
+  if(fp == baz) {
+    printf("fp = %p, baz = %p\n", fp, baz);
+    fp("calling via symbolic!");
+  }
+#endif
+
+  return 0;
+}
diff --git a/test/Feature/GetValue.c b/test/Feature/GetValue.c
new file mode 100644
index 00000000..391b68e3
--- /dev/null
+++ b/test/Feature/GetValue.c
@@ -0,0 +1,17 @@
+// RUN: %llvmgcc -c -o %t1.bc %s
+// RUN: %klee --exit-on-error %t1.bc
+
+#include <stdio.h>
+#include <assert.h>
+
+int main() {
+  int x = klee_int("x");
+  klee_assume(x > 10);
+  klee_assume(x < 20);
+
+  assert(!klee_is_symbolic(klee_get_value(x)));
+  assert(klee_get_value(x) > 10);
+  assert(klee_get_value(x) < 20);
+
+  return 0;
+}
diff --git a/test/Feature/ImpliedValue.c.failing b/test/Feature/ImpliedValue.c.failing
new file mode 100644
index 00000000..2f169970
--- /dev/null
+++ b/test/Feature/ImpliedValue.c.failing
@@ -0,0 +1,147 @@
+// RUN: rm -f %t4.out %t4.err %t4.log
+// RUN: %llvmgcc %s -emit-llvm -O2 -c -o %t1.bc
+// RUN: llvm-as -f ../_utils._ll -o %t2.bc
+// RUN: llvm-ld -disable-opt -link-as-library %t1.bc %t2.bc -o %t3.bc
+// RUN: %klee --log-file %t4.log --debug-check-for-implied-values %t3.bc > %t4.out 2> %t4.err
+// RUN: ls klee-last | not grep .err
+// RUN: not grep "(missed)" %t4.log
+
+#include <assert.h>
+
+#include "utils.h"
+
+int main() {
+  unsigned char which;
+  volatile unsigned char a,b,c,d,e,f,g,h;
+
+  klee_make_symbolic(&which, sizeof which);
+  klee_make_symbolic(&a, sizeof a);
+  klee_make_symbolic(&b, sizeof b);
+  klee_make_symbolic(&c, sizeof c);
+  klee_make_symbolic(&d, sizeof d);
+  klee_make_symbolic(&e, sizeof e);
+  klee_make_symbolic(&f, sizeof f);
+  klee_make_symbolic(&g, sizeof g);
+  klee_make_symbolic(&h, sizeof h);
+
+  switch (which) {
+// RUN: grep "simple read(2) = value case" %t4.out
+  case 0:
+    if (a == 2) {
+      assert(!klee_is_symbolic(a));
+      printf("simple read(%d) = value case\n", a);
+    }
+    break;
+
+// RUN: grep "select(0) has distinct constant result case (false)" %t4.out
+  case 1:
+    if (util_make_select(a, 12, 14) == 14) {
+      assert(!klee_is_symbolic(a));
+      printf("select(%d) has distinct constant result case (false)\n", a);
+    }
+    break;
+
+// RUN: grep "select(0) has distinct constant result case (true)" %t4.out
+  case 2:
+    if (util_make_select(!a, 12, 14) == 12) {
+      assert(!klee_is_symbolic(a));
+      printf("select(%d) has distinct constant result case (true)\n", a);
+    }
+    break;
+
+// RUN: grep "concat2(0xBE,0xEF) = value case" %t4.out
+  case 3:
+    if (util_make_concat2(a,b) == 0xBEEF) {
+      assert(!klee_is_symbolic(a));
+      assert(!klee_is_symbolic(b));
+      printf("concat2(0x%X,0x%X) = value case\n",
+             a, b);
+    }
+    break;
+
+// RUN: grep "concat4(0xDE,0xAD,0xBE,0xEF) = value case" %t4.out
+  case 4:
+    if (util_make_concat4(a,b,c,d) == 0xDEADBEEF) {
+      assert(!klee_is_symbolic(a));
+      assert(!klee_is_symbolic(b));
+      assert(!klee_is_symbolic(c));
+      assert(!klee_is_symbolic(d));
+      printf("concat4(0x%X,0x%X,0x%X,0x%X) = value case\n",
+             a, b, c, d);
+    }
+    break;
+
+// RUN: grep "concat8(0xDE,0xAD,0xBE,0xEF,0xAB,0xCD,0xAB,0xCD) = value case" %t4.out
+  case 5:
+    if (util_make_concat8(a,b,c,d,e,f,g,h) == 0xDEADBEEFABCDABCDLL) {
+      assert(!klee_is_symbolic(a));
+      assert(!klee_is_symbolic(b));
+      assert(!klee_is_symbolic(c));
+      assert(!klee_is_symbolic(d));
+      assert(!klee_is_symbolic(e));
+      assert(!klee_is_symbolic(f));
+      assert(!klee_is_symbolic(g));
+      assert(!klee_is_symbolic(h));
+      printf("concat8(0x%X,0x%X,0x%X,0x%X,0x%X,0x%X,0x%X,0x%X) = value case\n",
+             a, b, c, d, e, f, g, h);
+    }
+    break;
+
+// RUN: grep "and(0,0) = true case" %t4.out
+  case 6:
+    if (util_make_and_i1(!a, !b)) {
+      assert(!klee_is_symbolic(a));
+      assert(!klee_is_symbolic(b));      
+      printf("and(%d,%d) = true case\n", a, b);
+    }
+    break;
+
+// RUN: grep "or(0,0) = false case" %t4.out
+  case 7:
+    if (!util_make_or_i1(a, b)) {
+      assert(!klee_is_symbolic(a));
+      assert(!klee_is_symbolic(b));      
+      printf("or(%d,%d) = false case\n", a, b);
+    }
+    break;
+
+    // we use concat to prevent folding, will need to fix if that gets
+    // partial evaluated
+// RUN: grep "add constant case: 0xDE" %t4.out
+  case 8:
+    if (util_make_concat2(a+0xCD,0xCD) == 0xABCD) { 
+      assert(!klee_is_symbolic(a));
+      printf("add constant case: 0x%X\n", a);
+    }
+    break;
+
+// RUN: grep "sub constant case: 0x60" %t4.out
+  case 9:
+    if (util_make_concat2(0x0B-a,0xCD) == 0xABCD) { 
+      assert(!klee_is_symbolic(a));
+      printf("sub constant case: 0x%X\n", a);
+    }
+    break;
+
+// RUN: grep "xor constant case: 0xA0" %t4.out
+  case 10:
+    if (util_make_concat2(0x0B ^ a,0xCD) == 0xABCD) { 
+      assert(!klee_is_symbolic(a));
+      printf("xor constant case: 0x%X\n", a);
+    }
+    break;
+
+// RUN: grep "sext constant case: 244" %t4.out
+  case 11:
+    if (! util_make_or_i1(((short) (signed char) a) + 12,b)) {
+      assert(!klee_is_symbolic(a));
+      printf("sext constant case: %d\n", a);
+    }
+    break;
+
+  default:
+    break;
+  }
+
+  return 0;
+}
diff --git a/test/Feature/InAndOutOfBounds.c b/test/Feature/InAndOutOfBounds.c
new file mode 100644
index 00000000..18e5d2b2
--- /dev/null
+++ b/test/Feature/InAndOutOfBounds.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: test -f klee-last/test000001.ptr.err -o -f klee-last/test000002.ptr.err 
+// RUN: test ! -f klee-last/test000001.ptr.err -o ! -f klee-last/test000002.ptr.err 
+// RUN: test ! -f klee-last/test000003.bout
+
+unsigned klee_urange(unsigned start, unsigned end) {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+  if (x-start>=end-start) klee_silent_exit(0);
+  return x;
+}
+
+int main() {
+  int *x = malloc(4);
+  x[klee_urange(0,2)] = 1;
+  free(x);
+  return 0;
+}
diff --git a/test/Feature/IndirectCallToBuiltin.c b/test/Feature/IndirectCallToBuiltin.c
new file mode 100644
index 00000000..591a5601
--- /dev/null
+++ b/test/Feature/IndirectCallToBuiltin.c
@@ -0,0 +1,15 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee %t1.bc
+
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+  void *(*allocator)(size_t) = malloc;
+  int *mem = allocator(10);
+
+  printf("mem: %p\n", mem);
+  printf("mem[0]: %d\n", mem[0]);
+
+  return 0;
+}
diff --git a/test/Feature/IndirectCallToExternal.c b/test/Feature/IndirectCallToExternal.c
new file mode 100644
index 00000000..4603213b
--- /dev/null
+++ b/test/Feature/IndirectCallToExternal.c
@@ -0,0 +1,15 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee %t1.bc
+
+#include <stdlib.h>
+#include <stdio.h>
+#include <string.h>
+#include <assert.h>
+
+int main() {
+  int (*scmp)(char*,char*) = strcmp;
+
+  assert(scmp("hello","hi") < 0);
+
+  return 0;
+}
diff --git a/test/Feature/InvalidBitfieldAccess.c.failing b/test/Feature/InvalidBitfieldAccess.c.failing
new file mode 100644
index 00000000..ae8bfe5e
--- /dev/null
+++ b/test/Feature/InvalidBitfieldAccess.c.failing
@@ -0,0 +1,28 @@
+// RUN: %llvmgcc -c -o %t1.bc %s
+// RUN: %klee --exit-on-error %t1.bc
+
+// This is a bug in llvm-gcc4.0 but seems to be fixed in llvm-gcc4.2,
+// its included here mostly as a reminder. 
+
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+struct foo {
+  unsigned int a : 5;
+  unsigned int b : 10;
+  unsigned int c : 1;
+} __attribute__((packed));
+
+int main() {
+  struct foo *a = malloc(sizeof *a);
+
+  a->b = 12; // problem here is that llvm-gcc emits a 4 byte access
+             // which is out of bounds.
+
+  int x = a->b;
+
+  assert(x == 12);
+
+  return 0;
+}
diff --git a/test/Feature/IsSymbolic.c b/test/Feature/IsSymbolic.c
new file mode 100644
index 00000000..4a86368a
--- /dev/null
+++ b/test/Feature/IsSymbolic.c
@@ -0,0 +1,16 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+
+#include <assert.h>
+
+int main() {
+  int x, y, z = 0;
+  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&y, sizeof y);
+  if (x) {
+    assert(klee_is_symbolic(y));
+  } else {
+    assert(!klee_is_symbolic(z));
+  }
+  return 0;
+}
diff --git a/test/Feature/KleeReportError.c b/test/Feature/KleeReportError.c
new file mode 100644
index 00000000..dda72fd0
--- /dev/null
+++ b/test/Feature/KleeReportError.c
@@ -0,0 +1,23 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --emit-all-errors %t2.bc > %t3.log
+// RUN: ls klee-last/ | grep .my.err | wc -l | grep 2
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  int x, y, *p = 0;
+  
+  klee_make_symbolic(&x, sizeof x);
+  klee_make_symbolic(&y, sizeof y);
+
+  if (x)
+    fprintf(stderr, "x\n");
+  else fprintf(stderr, "!x\n");
+
+  if (y) {
+    fprintf(stderr, "My error\n");
+    klee_report_error(__FILE__, __LINE__, "My error", "my.err");
+  }
+
+  return 0;
+}
diff --git a/test/Feature/LongDoubleSupport.c b/test/Feature/LongDoubleSupport.c
new file mode 100644
index 00000000..b4631832
--- /dev/null
+++ b/test/Feature/LongDoubleSupport.c
@@ -0,0 +1,20 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc > %t2.out
+
+#include <stdio.h>
+#include <float.h>
+
+// FIXME: This doesn't really work at all, it just doesn't
+// crash. Until we have wide constant support, that is all we care
+// about; the only reason this comes up is in initialization of
+// constants, we don't actually end up seeing much code which uses long
+// double.
+int main() {
+  long double a = LDBL_MAX;
+  long double b = -1;
+  long double c = a + b;
+  printf("a = %Lg\n", a);
+  printf("b = %Lg\n", b);
+  printf("c = %Lg\n", c);
+  return 0;
+}
diff --git a/test/Feature/LowerSwitch.c b/test/Feature/LowerSwitch.c
new file mode 100644
index 00000000..c4d9644a
--- /dev/null
+++ b/test/Feature/LowerSwitch.c
@@ -0,0 +1,30 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t.bc
+// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=internal %t.bc
+// RUN: not test -f klee-last/test000010.bout
+// RUN: %klee --exit-on-error --allow-external-sym-calls --switch-type=simple %t.bc
+// RUN: test -f klee-last/test000010.bout
+
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+  int c = klee_range(0, 256, "range");
+  
+  switch(c) {
+  case 0: printf("0\n"); break;
+  case 10: printf("10\n"); break;
+  case 16: printf("16\n"); break;
+  case 17: printf("17\n"); break;
+  case 18: printf("18\n"); break;
+  case 19: printf("19\n"); break;
+#define C(x) case x: case x+1: case x+2: case x+3
+#define C2(x) C(x): C(x+4): C(x+8): C(x+12)
+#define C3(x) C2(x): C2(x+16): C2(x+32): C2(x+48)
+  C3(128):
+    printf("bignums: %d\n", c); break;
+  default: 
+    printf("default\n");
+    break;
+  }
+
+  return 0;
+}
diff --git a/test/Feature/MakeConcreteSymbolic.c b/test/Feature/MakeConcreteSymbolic.c
new file mode 100644
index 00000000..29b43a04
--- /dev/null
+++ b/test/Feature/MakeConcreteSymbolic.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+// RUN: grep "done: total queries = 0" klee-last/info
+// RUN: %klee --make-concrete-symbolic=1 --exit-on-error %t1.bc
+// RUN: grep "done: total queries = 2" klee-last/info
+
+
+#include <assert.h>
+
+#define N 2
+int main() {
+  int i;
+  char a;
+  
+  a = 10;
+  assert(a == 10);
+
+  return 0;
+}
diff --git a/test/Feature/MakeSymbolicName.c b/test/Feature/MakeSymbolicName.c
new file mode 100644
index 00000000..c1f11424
--- /dev/null
+++ b/test/Feature/MakeSymbolicName.c
@@ -0,0 +1,17 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t1.bc
+// RUN: %klee --use-random-search --exit-on-error %t1.bc
+
+#include <assert.h>
+
+int main() {
+  int a[4] = {1, 2, 3, 4};
+  unsigned i;
+
+  klee_make_symbolic_name(&i, sizeof(i), "index");  
+  if (i > 3)
+    klee_silent_exit(0);
+
+  assert(a[i] << 1 != 5);
+  if (a[i] << 1 == 6)
+    assert(i == 2);
+}
diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c
new file mode 100644
index 00000000..3b1bacaf
--- /dev/null
+++ b/test/Feature/MemoryLimit.c
@@ -0,0 +1,37 @@
+// RUN: %llvmgcc -DLITTLE_ALLOC -g -c %s -o %t.little.bc
+// RUN: %llvmgcc -g -c %s -o %t.big.bc
+// RUN: %klee --max-memory=20 %t.little.bc > %t.little.log
+// RUN: %klee --max-memory=20 %t.big.bc > %t.big.log
+// RUN: not grep -q "DONE" %t.little.log
+// RUN: not grep -q "DONE" %t.big.log
+
+#include <stdlib.h>
+
+int main() {
+  int i, j, x=0;
+  
+#ifdef LITTLE_ALLOC
+  printf("IN LITTLE ALLOC\n");
+    
+  // 200 MBs total (in 32 byte chunks)
+  for (i=0; i<100; i++) {
+    for (j=0; j<(1<<16); j++)
+      malloc(1<<5);
+  }
+#else
+  printf("IN BIG ALLOC\n");
+  
+  // 200 MBs total
+  for (i=0; i<100; i++) {
+    malloc(1<<21);
+    
+    // Ensure we hit the periodic check
+    for (j=0; j<10000; j++)
+      x++;
+  }
+#endif
+
+  printf("DONE!\n");
+
+  return x;
+}
diff --git a/test/Feature/MultipleFreeResolution.c b/test/Feature/MultipleFreeResolution.c
new file mode 100644
index 00000000..872d6856
--- /dev/null
+++ b/test/Feature/MultipleFreeResolution.c
@@ -0,0 +1,39 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --emit-all-errors %t1.bc
+// RUN: ls klee-last/ | grep .out | wc -l | grep 4
+// RUN: ls klee-last/ | grep .err | wc -l | grep 3
+
+#include <stdlib.h>
+#include <stdio.h>
+
+unsigned klee_urange(unsigned start, unsigned end) {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+  if (x-start>=end-start) klee_silent_exit(0);
+  return x;
+}
+
+int *make_int(int i) {
+  int *x = malloc(sizeof(*x));
+  *x = i;
+  return x;
+}
+
+int main() {
+  int *buf[4];
+  int i,s;
+
+  for (i=0; i<3; i++)
+    buf[i] = make_int(i);
+  buf[3] = 0;
+
+  s = klee_urange(0,4);
+
+  free(buf[s]);
+
+  for (i=0; i<3; i++) {
+    printf("*buf[%d] = %d\n", i, *buf[i]);
+  }
+
+  return 0;
+}
diff --git a/test/Feature/MultipleReadResolution.c b/test/Feature/MultipleReadResolution.c
new file mode 100644
index 00000000..9297cf8d
--- /dev/null
+++ b/test/Feature/MultipleReadResolution.c
@@ -0,0 +1,43 @@
+// RUN: echo "x" > %t1.res
+// RUN: echo "x" >> %t1.res
+// RUN: echo "x" >> %t1.res
+// RUN: echo "x" >> %t1.res
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc > %t1.log
+// RUN: diff %t1.res %t1.log
+
+#include <stdio.h>
+
+unsigned klee_urange(unsigned start, unsigned end) {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+  if (x-start>=end-start) klee_silent_exit(0);
+  return x;
+}
+
+int *make_int(int i) {
+  int *x = malloc(sizeof(*x));
+  *x = i;
+  return x;
+}
+
+int main() {
+  int *buf[4];
+  int i,s,t;
+
+  for (i=0; i<4; i++)
+    buf[i] = make_int((i+1)*2);
+
+  s = klee_urange(0,4);
+
+  int x = *buf[s];
+
+  if (x == 4)
+    if (s!=1)
+      abort();
+
+  printf("x\n");
+  fflush(stdout);
+
+  return 0;
+}
diff --git a/test/Feature/MultipleReallocResolution.c b/test/Feature/MultipleReallocResolution.c
new file mode 100644
index 00000000..b1a14ace
--- /dev/null
+++ b/test/Feature/MultipleReallocResolution.c
@@ -0,0 +1,63 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: ls klee-last/ | grep .err | wc -l | grep 2
+// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+unsigned klee_urange(unsigned start, unsigned end) {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+  if (x-start>=end-start) klee_silent_exit(0);
+  return x;
+}
+
+int *make_int(int i, int N) {
+  int *x = malloc(sizeof(*x) * N);
+  *x = i;
+  return x;
+}
+
+int main() {
+  int *buf[4];
+
+  buf[0] = malloc(sizeof(int)*4);
+  buf[1] = malloc(sizeof(int));
+  buf[2] = 0; // gets malloc'd
+  buf[3] = (int*) 0xdeadbeef; // boom
+
+  buf[0][0] = 10;
+  buf[0][1] = 42;
+  buf[1][0] = 20;
+
+  int i = klee_urange(0,4);
+  int new_size = 2 * sizeof(int) * klee_urange(0,2); // 0 or 8
+
+  // whee, party time, needs to:
+  // Fork if size == 0, in which case all buffers get free'd and
+  // we will crash in prints below.
+  // Fork if buf[s] == 0, in which case the buffer gets malloc'd (for s==2)
+  // Fork on other buffers (s in [0,1]) and do realloc
+  //   for s==0 this is shrinking
+  //   for s==1 this is growing
+  buf[i] = realloc(buf[i], new_size);
+
+  if (new_size == 0) {
+    assert(!buf[2]); // free(0) is a no-op
+    if (i==0) assert(!buf[0] && buf[1]);
+    if (i==1) assert(buf[0] && !buf[1]);
+    assert(i != 3); // we should have crashed on free of invalid
+  } else {
+    assert(new_size == sizeof(int)*2);
+    assert(buf[0][0] == 10);
+    assert(buf[0][1] == 42); // make sure copied
+    assert(buf[1][0] == 20);
+    if (i==1) { int x = buf[1][1]; } // should be safe
+    if (i==2) { int x = buf[2][0]; } // should be safe
+    assert(i != 3); // we should have crashed on realloc of invalid
+  }
+
+  return 0;
+}
diff --git a/test/Feature/MultipleWriteResolution.c b/test/Feature/MultipleWriteResolution.c
new file mode 100644
index 00000000..f07b9710
--- /dev/null
+++ b/test/Feature/MultipleWriteResolution.c
@@ -0,0 +1,43 @@
+// RUN: echo "x" > %t1.res
+// RUN: echo "x" >> %t1.res
+// RUN: echo "x" >> %t1.res
+// RUN: echo "x" >> %t1.res
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc > %t1.log
+// RUN: diff %t1.res %t1.log
+
+#include <stdio.h>
+
+unsigned klee_urange(unsigned start, unsigned end) {
+  unsigned x;
+  klee_make_symbolic(&x, sizeof x);
+  if (x-start>=end-start) klee_silent_exit(0);
+  return x;
+}
+
+int *make_int(int i) {
+  int *x = malloc(sizeof(*x));
+  *x = i;
+  return x;
+}
+
+int main() {
+  int *buf[4];
+  int i,s,t;
+
+  for (i=0; i<4; i++)
+    buf[i] = make_int((i+1)*2);
+
+  s = klee_urange(0,4);
+
+  *buf[s] = 5;
+
+  if ((*buf[0] + *buf[1] + *buf[2] + *buf[3]) == 17)
+    if (s!=3)
+      abort();
+
+  printf("x\n");
+  fflush(stdout);
+
+  return 0;
+}
diff --git a/test/Feature/NamedSeedMatching.c b/test/Feature/NamedSeedMatching.c
new file mode 100644
index 00000000..6d52e7a4
--- /dev/null
+++ b/test/Feature/NamedSeedMatching.c
@@ -0,0 +1,41 @@
+// RUN: %llvmgcc -c -g %s -o %t.bc
+// RUN: rm -rf %t.out
+// RUN: %klee --output-dir=%t.out %t.bc "initial"
+// RUN: test -f %t.out/test000001.bout
+// RUN: not test -f %t.out/test000002.bout
+// RUN: %klee --only-replay-seeds --named-seed-matching --seed-out %t.out/test000001.bout %t.bc > %t.log
+// RUN: grep -q "a==3" %t.log
+// RUN: grep -q "b==4" %t.log
+// RUN: grep -q "c==5" %t.log
+// RUN: grep -q "x==6" %t.log
+
+#include <string.h>
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+  int a, b, c, x;
+
+  if (argc==2 && strcmp(argv[1], "initial") == 0) {
+    klee_make_symbolic_name(&a, sizeof a, "a");
+    klee_make_symbolic_name(&b, sizeof b, "b");
+    klee_make_symbolic_name(&c, sizeof c, "c");
+    klee_make_symbolic_name(&x, sizeof x, "a");
+
+    klee_assume(a == 3);
+    klee_assume(b == 4);
+    klee_assume(c == 5);
+    klee_assume(x == 6);
+  } else {
+    klee_make_symbolic_name(&a, sizeof a, "a");
+    klee_make_symbolic_name(&c, sizeof c, "c");
+    klee_make_symbolic_name(&b, sizeof b, "b");
+    klee_make_symbolic_name(&x, sizeof x, "a");
+  }
+
+  if (a==3) printf("a==3\n");
+  if (b==4) printf("b==4\n");
+  if (c==5) printf("c==5\n");
+  if (x==6) printf("x==6\n");
+
+  return 0;
+}
diff --git a/test/Feature/OneFreeError.c b/test/Feature/OneFreeError.c
new file mode 100644
index 00000000..8eb13298
--- /dev/null
+++ b/test/Feature/OneFreeError.c
@@ -0,0 +1,10 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: test -f klee-last/test000001.ptr.err
+
+int main() {
+  int *x = malloc(4);
+  free(x);
+  x[0] = 1;
+  return 0;
+}
diff --git a/test/Feature/OneOutOfBounds.c b/test/Feature/OneOutOfBounds.c
new file mode 100644
index 00000000..11a9eecb
--- /dev/null
+++ b/test/Feature/OneOutOfBounds.c
@@ -0,0 +1,10 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: test -f klee-last/test000001.ptr.err
+
+int main() {
+  int *x = malloc(4);
+  x[1] = 1;
+  free(x);
+  return 0;
+}
diff --git a/test/Feature/Optimize.c b/test/Feature/Optimize.c
new file mode 100644
index 00000000..3c9159c7
--- /dev/null
+++ b/test/Feature/Optimize.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc %s --emit-llvm -O0 -c -o %t2.bc
+// RUN: rm -f %t2.log
+// RUN: %klee --stop-after-n-instructions=100 --optimize %t2.bc > %t3.log
+// RUN: echo "good" > %t3.good
+// RUN: diff %t3.log %t3.good
+
+// should complete by 100 instructions if opt is on
+
+int main() {
+  int i, res = 0;
+
+  for (i=1; i<=1000; i++)
+    res += i;
+
+  if (res == (1000*1001)/2) {
+    printf("good\n");
+  } else {
+    printf("bad\n");
+  }
+  
+  return 0;
+}
diff --git a/test/Feature/OverlappedError.c b/test/Feature/OverlappedError.c
new file mode 100644
index 00000000..3c79380c
--- /dev/null
+++ b/test/Feature/OverlappedError.c
@@ -0,0 +1,19 @@
+// RUN: %llvmgcc %s -g -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc
+// RUN: ls klee-last/ | grep .out | wc -l | grep 4
+// RUN: ls klee-last/ | grep .ptr.err | wc -l | grep 2
+
+#include <stdlib.h>
+
+int main() {
+  if (klee_range(0,2, "range")) {
+    char *x = malloc(8);
+    *((int*) &x[klee_range(0,6, "range")]) = 1;
+    free(x);
+  } else {
+    char *x = malloc(8);
+    *((int*) &x[klee_range(-1,5, "range")]) = 1;
+        free(x);
+  }
+  return 0;
+}
diff --git a/test/Feature/PreferCex.c b/test/Feature/PreferCex.c
new file mode 100644
index 00000000..d73b6076
--- /dev/null
+++ b/test/Feature/PreferCex.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+// RUN: klee-bout-tool klee-last/test000001.bout | grep -F 'Hi\x00\x00'
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+  char buf[4];
+
+  klee_make_symbolic(buf, sizeof buf);
+  klee_prefer_cex(buf, buf[0]=='H');
+  klee_prefer_cex(buf, buf[1]=='i');
+  klee_prefer_cex(buf, buf[2]=='\0');
+
+  return 0;
+}
diff --git a/test/Feature/RaiseAsm.c b/test/Feature/RaiseAsm.c
new file mode 100644
index 00000000..5b8acab4
--- /dev/null
+++ b/test/Feature/RaiseAsm.c
@@ -0,0 +1,39 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+
+#include <assert.h>
+
+typedef unsigned short uint16;
+typedef unsigned int   uint32;
+
+uint16 byteswap_uint16(uint16 x) {
+  return (x << 8) | (x >> 8);
+}
+uint32 byteswap_uint32(uint32 x) {
+  return ((byteswap_uint16(x) << 16) |
+          (byteswap_uint16(x >> 16)));
+}
+
+uint16 byteswap_uint16_asm(uint16 x) {
+  uint16 res;
+  __asm__("rorw $8, %w0" : "=r" (res) : "0" (x) : "cc");
+  return res;
+}
+
+uint32 byteswap_uint32_asm(uint32 x) {
+  uint32 res;
+  __asm__("rorw $8, %w0;"
+          "rorl $16, %0;"
+          "rorw $8, %w0" : "=r" (res) : "0" (x) : "cc");
+  return res;
+}
+
+int main() {
+  uint16 ui16 = klee_int("ui16");
+  uint32 ui32 = klee_int("ui32");
+
+  assert(ui16 == byteswap_uint16(byteswap_uint16_asm(ui16)));
+  assert(ui32 == byteswap_uint32(byteswap_uint32_asm(ui32)));
+
+  return 0;
+}
diff --git a/test/Feature/ReallocFailure.c b/test/Feature/ReallocFailure.c
new file mode 100644
index 00000000..e5105c33
--- /dev/null
+++ b/test/Feature/ReallocFailure.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --exit-on-error %t1.bc
+
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+int main() {
+  int *p = malloc(sizeof(int)*2);
+  assert(p);
+  p[1] = 52;
+
+  int *p2 = realloc(p, 1<<30);
+  assert(p2 == 0);
+  assert(p[1] == 52);
+
+  return 0;
+}
diff --git a/test/Feature/ReplayPath.c b/test/Feature/ReplayPath.c
new file mode 100644
index 00000000..3f01fa80
--- /dev/null
+++ b/test/Feature/ReplayPath.c
@@ -0,0 +1,27 @@
+// RUN: echo "1" > %t1.path
+// RUN: echo "0" >> %t1.path
+// RUN: echo "1" >> %t1.path
+// RUN: echo "0" >> %t1.path
+// RUN: echo "1" >> %t1.path
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --replay-path %t1.path %t2.bc > %t3.log
+// RUN: echo "res: 110" > %t3.good
+// RUN: diff %t3.log %t3.good
+
+int main() {
+  int res = 1;
+  int x;
+
+  klee_make_symbolic(&x, sizeof x);
+
+  if (x&1) res *= 2;
+  if (x&2) res *= 3;
+  if (x&4) res *= 5;
+
+  // get forced branch coverage
+  if (x&2) res *= 7;
+  if (!(x&2)) res *= 11;
+  printf("res: %d\n", res);
+ 
+  return 0;
+}
diff --git a/test/Feature/Searchers.c b/test/Feature/Searchers.c
new file mode 100644
index 00000000..95ebddf2
--- /dev/null
+++ b/test/Feature/Searchers.c
@@ -0,0 +1,52 @@
+// RUN: %llvmgcc %s --emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee %t2.bc
+// RUN: %klee --use-random-search %t2.bc
+// RUN: %klee --use-non-uniform-random-search %t2.bc
+// RUN: %klee --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-batching-search %t2.bc
+// RUN: %klee --use-batching-search --use-random-search %t2.bc
+// RUN: %klee --use-batching-search --use-non-uniform-random-search %t2.bc
+// RUN: %klee --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-merge --debug-log-merge --debug-log-state-merge %t2.bc
+// RUN: %klee --use-merge --use-batching-search %t2.bc
+// RUN: %klee --use-merge --use-batching-search --use-random-search %t2.bc
+// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search %t2.bc
+// RUN: %klee --use-merge --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-random-search %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search %t2.bc
+// RUN: %klee --use-iterative-deepening-time-search --use-batching-search --use-non-uniform-random-search --weight-type=query-cost %t2.bc
+
+
+/* this test is basically just for coverage and doesn't really do any
+   correctness check (aside from testing that the various combinations
+   don't crash) */
+
+int validate(char *buf, int N) {
+
+  int i;
+
+  for (i=0; i<N; i++) {
+    if (buf[i]==0) {
+      klee_merge();
+      return 0;
+    }
+  }
+  
+  klee_merge();
+  return 1;
+}
+
+#ifndef SYMBOLIC_SIZE
+#define SYMBOLIC_SIZE 15
+#endif
+int main(int argc, char **argv) {
+  int N = SYMBOLIC_SIZE;
+  unsigned char *buf = malloc(N);
+  int i;
+  
+  klee_make_symbolic(buf, N);
+  if (validate(buf, N))
+    return buf[0];
+  return 0;
+}
diff --git a/test/Feature/SetForking.c b/test/Feature/SetForking.c
new file mode 100644
index 00000000..8620110d
--- /dev/null
+++ b/test/Feature/SetForking.c
@@ -0,0 +1,28 @@
+// RUN: %llvmgcc -g -c %s -o %t.bc
+// RUN: %klee %t.bc > %t.log
+// RUN: sort %t.log | uniq -c > %t.uniq.log
+// RUN: grep "1 A" %t.uniq.log
+// RUN: grep "1 B" %t.uniq.log
+// RUN: grep "1 C" %t.uniq.log
+
+#include <stdio.h>
+
+int main() {
+  klee_set_forking(0);
+  
+  if (klee_range(0, 2, "range")) {
+    printf("A\n");
+  } else {
+    printf("A\n");
+  }
+
+  klee_set_forking(1);
+
+  if (klee_range(0, 2, "range")) {
+    printf("B\n");
+  } else {
+    printf("C\n");
+  }
+
+  return 0;
+}
diff --git a/test/Feature/Vararg.c b/test/Feature/Vararg.c
new file mode 100644
index 00000000..f782c15e
--- /dev/null
+++ b/test/Feature/Vararg.c
@@ -0,0 +1,82 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee %t1.bc > %t2.out
+// RUN: grep "types: (52, 37, 2.00, (9,12,15))" %t2.out
+// RUN: test -f klee-last/test000001.ptr.err
+
+#include <stdarg.h>
+#include <assert.h>
+#include <stdio.h>
+
+struct triple {
+  int first, second, third;
+};
+
+int test1(int x, ...) {
+  va_list ap;
+  va_start(ap, x);
+  int i32 = va_arg(ap, int);
+  long long i64 = va_arg(ap, long long);
+  double d = va_arg(ap, double);
+  struct triple p = va_arg(ap, struct triple);
+  printf("types: (%d, %lld, %.2f, (%d,%d,%d))\n", i32, i64, d, p.first, p.second, p.third);
+  va_end(ap);
+}
+
+int sum(int N, ...) {
+  int i, res = 0;
+  va_list ap,ap2;
+  
+  va_start(ap, N);
+  for (i=0; i<N; i++) {
+    if (i==1)
+      va_copy(ap2, ap);
+    res += va_arg(ap, int);
+  }
+  for (i=0; i<N-1; i++)
+    res += va_arg(ap2, int);
+  va_end(ap);
+
+  return res;
+}
+
+// test using aps in an array (no multiple resolution
+// testing, though)
+int va_array(int N, ...) {
+  va_list aps[2];
+  unsigned i;
+  unsigned sum1 = 0, sum2 = 0;
+
+  for (i=0; i<2; i++)
+    va_start(aps[i], N);
+  
+  for (i=0; i<N; i++) {
+    unsigned cmd = va_arg(aps[0], int);
+
+    if (cmd==0) {
+      sum1 += va_arg(aps[0],int);
+    } else if (cmd==1) {
+      sum2 += va_arg(aps[1],int);
+    } else if (cmd==2) {
+      va_copy(aps[1], aps[0]);
+    }
+  }
+
+  for (i=0; i<2; i++)
+    va_end(aps[i]);
+
+  return 3*sum1 + 5*sum2;
+}
+
+int main() {
+  struct triple p = { 9, 12, 15 };
+  test1(-1, 52, 37ll, 2.0, p);
+
+  assert(sum(2, 3, 4) == 11);
+  assert(sum(0) == 0);
+  assert(va_array(5, 0, 5, 1, 1, 2, 1)==45); // 15 + 30
+
+  // should give memory error
+  test1(-1, 52, 37, 2.0, p);
+
+  return 0;
+}
diff --git a/test/Feature/WithLibc.c b/test/Feature/WithLibc.c
new file mode 100644
index 00000000..5e84eb4a
--- /dev/null
+++ b/test/Feature/WithLibc.c
@@ -0,0 +1,22 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --libc=klee %t2.bc > %t3.log
+// RUN: echo "good" > %t3.good
+// RUN: diff %t3.log %t3.good
+
+int main() {
+  char buf[4];
+  char *s = "foo";
+
+  klee_make_symbolic(buf, sizeof buf);
+  buf[3] = 0;
+
+  if (strcmp(buf, s)==0) {
+    if (buf[0]=='f' && buf[1]=='o' && buf[2]=='o' && buf[3]==0) {
+      printf("good\n");
+    } else {
+      printf("bad\n");
+    }
+  }
+  
+  return 0;
+}
diff --git a/test/Feature/WriteCov.c b/test/Feature/WriteCov.c
new file mode 100644
index 00000000..defc7e59
--- /dev/null
+++ b/test/Feature/WriteCov.c
@@ -0,0 +1,15 @@
+// RUN: %llvmgcc %s -emit-llvm -g -c -o %t2.bc
+// RUN: %klee --exit-on-error --write-cov %t2.bc
+// RUN: grep WriteCov.c:10 klee-last/test000002.cov
+// RUN: grep WriteCov.c:12 klee-last/test000001.cov
+
+#include <assert.h>
+
+int main() {
+  if (klee_range(0,2, "range")) {
+    assert(__LINE__ == 10); printf("__LINE__ = %d\n", __LINE__);
+  } else {
+    assert(__LINE__ == 12); printf("__LINE__ = %d\n", __LINE__);
+  }
+  return 0;
+}
diff --git a/test/Feature/_utils._ll b/test/Feature/_utils._ll
new file mode 100644
index 00000000..32a73bb1
--- /dev/null
+++ b/test/Feature/_utils._ll
@@ -0,0 +1,71 @@
+define i32 @util_make_and_i1(i32 %a, i32 %b) {
+        %a_i1 = icmp ne i32 %a, 0
+        %b_i1 = icmp ne i32 %b, 0
+        %res_i1 = and i1 %a_i1, %b_i1
+        %res = zext i1 %res_i1 to i32
+        ret i32 %res
+}
+
+define i32 @util_make_or_i1(i32 %a, i32 %b) {
+        %a_i1 = icmp ne i32 %a, 0
+        %b_i1 = icmp ne i32 %b, 0
+        %res_i1 = or i1 %a_i1, %b_i1
+        %res = zext i1 %res_i1 to i32
+        ret i32 %res
+}
+
+define i16 @util_make_concat2(i8 %a, i8 %b) {
+        %tmp = alloca i16
+        %tmp8 = bitcast i16* %tmp to i8*
+        %p0 = getelementptr i8* %tmp8, i32 0
+        %p1 = getelementptr i8* %tmp8, i32 1
+        store i8 %b, i8* %p0
+        store i8 %a, i8* %p1
+        %concat = load i16* %tmp
+        ret i16 %concat
+}
+
+define i32 @util_make_concat4(i8 %a, i8 %b, i8 %c, i8 %d) {
+        %tmp = alloca i32
+        %tmp8 = bitcast i32* %tmp to i8*
+        %p0 = getelementptr i8* %tmp8, i32 0
+        %p1 = getelementptr i8* %tmp8, i32 1
+        %p2 = getelementptr i8* %tmp8, i32 2
+        %p3 = getelementptr i8* %tmp8, i32 3
+        store i8 %d, i8* %p0
+        store i8 %c, i8* %p1
+        store i8 %b, i8* %p2
+        store i8 %a, i8* %p3
+        %concat = load i32* %tmp
+        ret i32 %concat
+}
+
+define i64 @util_make_concat8(i8 %a, i8 %b, i8 %c, i8 %d, 
+                              i8 %e, i8 %f, i8 %g, i8 %h) {
+        %tmp = alloca i64
+        %tmp8 = bitcast i64* %tmp to i8*
+        %p0 = getelementptr i8* %tmp8, i32 0
+        %p1 = getelementptr i8* %tmp8, i32 1
+        %p2 = getelementptr i8* %tmp8, i32 2
+        %p3 = getelementptr i8* %tmp8, i32 3
+        %p4 = getelementptr i8* %tmp8, i32 4
+        %p5 = getelementptr i8* %tmp8, i32 5
+        %p6 = getelementptr i8* %tmp8, i32 6
+        %p7 = getelementptr i8* %tmp8, i32 7
+        store i8 %h, i8* %p0
+        store i8 %g, i8* %p1
+        store i8 %f, i8* %p2
+        store i8 %e, i8* %p3
+        store i8 %d, i8* %p4
+        store i8 %c, i8* %p5
+        store i8 %b, i8* %p6
+        store i8 %a, i8* %p7
+        %concat = load i64* %tmp
+        ret i64 %concat
+}
+
+define i32 @util_make_select(i32 %cond, i32 %t, i32 %f) {
+        %cond_i1 = icmp ne i32 %cond, 0
+        %res = select i1 %cond_i1, i32 %t, i32 %f
+        ret i32 %res
+}
\ No newline at end of file
diff --git a/test/Feature/const_array_opt1.c b/test/Feature/const_array_opt1.c
new file mode 100644
index 00000000..96c46fb9
--- /dev/null
+++ b/test/Feature/const_array_opt1.c
@@ -0,0 +1,37 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --const-array-opt --max-time=10 --only-output-states-covering-new %t.bc >%t.log
+// grep -q "Finished successfully!\n"
+
+/* This is testing the const array optimization.  On my 2.3GHz machine
+   this takes under 2 seconds w/ the optimization and almost 6 minutes
+   w/o.  So we kill it in 10 sec and check if it has finished
+   successfully. */
+
+#include <unistd.h>
+#include <assert.h>
+#include <stdio.h>
+  
+int main() {
+#define N 8192
+#define N_IDX 16
+  unsigned char a[N];
+  unsigned i, k[N_IDX];
+
+  for (i=0; i<N; i++)
+    a[i] = i % 256;
+  
+  klee_make_symbolic_name(k, sizeof(k), "k");
+  
+  for (i=0; i<N_IDX; i++) {
+    if (k[i] >= N)
+      klee_silent_exit(0);
+
+    if (a[k[i]] == i)
+      assert(k[i] % 256 == i);
+    else klee_silent_exit(0);
+  }
+
+  printf("Finished successfully!\n");
+
+  return 0;
+}
diff --git a/test/Feature/dg.exp b/test/Feature/dg.exp
new file mode 100644
index 00000000..879685ca
--- /dev/null
+++ b/test/Feature/dg.exp
@@ -0,0 +1,3 @@
+load_lib llvm.exp
+
+RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{ll,llx,c,cpp,tr}]]
diff --git a/test/Feature/utils.h b/test/Feature/utils.h
new file mode 100644
index 00000000..5423a0dc
--- /dev/null
+++ b/test/Feature/utils.h
@@ -0,0 +1,16 @@
+typedef unsigned char uint8_t;
+typedef unsigned short uint16_t;
+typedef unsigned int uint32_t;
+typedef unsigned long long uint64_t;
+
+uint32_t util_make_and_i1(uint32_t a, uint32_t b);
+uint32_t util_make_or_i1(uint32_t a, uint32_t b);
+
+uint16_t util_make_concat2(uint8_t a, uint8_t b);
+uint32_t util_make_concat4(uint8_t a, uint8_t b, 
+                           uint8_t c, uint8_t d);
+uint64_t util_make_concat8(uint8_t a, uint8_t b,
+                           uint8_t c, uint8_t d,
+                           uint8_t e, uint8_t f,
+                           uint8_t g, uint8_t h);
+uint32_t util_make_select(uint32_t cond, uint32_t true, uint32_t false);