1 files changed, 22 insertions, 0 deletions
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;
+}