19 files changed, 584 insertions, 0 deletions

diff --git a/test/Runtime/POSIX/DirConsistency.c b/test/Runtime/POSIX/DirConsistency.c
new file mode 100644
index 00000000..613655e9
--- /dev/null
+++ b/test/Runtime/POSIX/DirConsistency.c
@@ -0,0 +1,64 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --run-in=/tmp --use-random-search --init-env --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t1.log
+// RUN: %llvmgcc -D_FILE_OFFSET_BITS=64 %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --run-in=/tmp --use-random-search --init-env --libc=uclibc --posix-runtime --exit-on-error %t.bc --sym-files 1 1 > %t2.log
+// RUN: sort %t1.log %t2.log | uniq -c > %t3.log
+// RUN: grep -q "4 COUNT" %t3.log
+
+// For this test really to work as intended it needs to be run in a
+// directory large enough to cause uclibc to do multiple getdents
+// calls (otherwise uclibc will handle the seeks itself). We should
+// create a bunch of files or something.
+//
+// It is even more important for this test because it requires the
+// directory not to change while running, which might be a lot to
+// demand of /tmp.
+
+#define _LARGEFILE64_SOURCE
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <dirent.h>
+#include <sys/stat.h>
+#include <errno.h>
+
+int main(int argc, char **argv) {
+  struct stat s;
+  int res = stat("A", &s);
+  int hasA = !(res!=0 && errno==ENOENT);
+
+  //printf("sizeof(dirent) = %d\n", sizeof(struct dirent));
+  //printf("sizeof(dirent64) = %d\n", sizeof(struct dirent64));
+
+  //printf("\"A\" exists: %d\n", hasA);
+
+  DIR *d = opendir(".");
+  assert(d);
+
+  int snum = 1;
+  if (klee_range(0,2,"range")) {
+    snum = 2;
+    printf("state%d\n", snum);
+  }
+
+  int foundA = 0, count = 0;
+  struct dirent *de;
+  while ((de = readdir(d))) {
+    //    printf("state%d: dirent: %s\n", snum, de->d_name);
+    if (strcmp(de->d_name, "A") == 0)
+      foundA = 1;
+    count++;
+  }
+  
+  closedir(d);
+
+  //printf("found A: %d\n", foundA);
+
+  // Ensure atomic write
+  char buf[64];
+  sprintf(buf, "COUNT: %d\n", count);
+  fputs(buf, stdout);
+  assert(hasA == foundA);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c
new file mode 100644
index 00000000..1735fdb8
--- /dev/null
+++ b/test/Runtime/POSIX/DirSeek.c
@@ -0,0 +1,57 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --run-in=/tmp --init-env --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 2 2
+// RUN: %klee --run-in=/tmp --init-env --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2
+// RUN: %klee --run-in=/tmp --init-env --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 0 2
+
+// For this test really to work as intended it needs to be run in a
+// directory large enough to cause uclibc to do multiple getdents
+// calls (otherwise uclibc will handle the seeks itself). We should
+// create a bunch of files or something.
+
+#include <assert.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <dirent.h>
+#include <sys/stat.h>
+#include <errno.h>
+#include <string.h>
+
+int main(int argc, char **argv) {
+  struct stat s;
+
+  char first[256], second[256];
+  DIR *d = opendir(".");
+  struct dirent *de = readdir(d);
+  assert(de);
+  strcpy(first, de->d_name);
+  off_t pos = telldir(d);
+  printf("pos: %d\n", telldir(d));
+  de = readdir(d);
+  assert(de);
+  strcpy(second, de->d_name);
+
+  // Go back to second and check
+  seekdir(d, pos);
+  de = readdir(d);
+  assert(de);
+  assert(strcmp(de->d_name, second) == 0);
+
+  // Go to end, then back to 2nd
+  while (de)
+    de = readdir(d);
+  assert(!errno);
+  seekdir(d, pos);
+  assert(telldir(d) == pos);
+  de = readdir(d);
+  assert(de);
+  assert(strcmp(de->d_name, second) == 0);
+
+  // Go to beginning and check
+  rewinddir(d);
+  de = readdir(d);
+  assert(de);
+  assert(strcmp(de->d_name, first) == 0);  
+  closedir(d);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/FDNumbers.c b/test/Runtime/POSIX/FDNumbers.c
new file mode 100644
index 00000000..e576f9bb
--- /dev/null
+++ b/test/Runtime/POSIX/FDNumbers.c
@@ -0,0 +1,24 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --init-env --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+
+#include <assert.h>
+#include <fcntl.h>
+#include <errno.h>
+
+int main(int argc, char **argv) {
+  int fd = open("A", O_TRUNC);
+  assert(fd == 3);
+  assert(!close(0));
+  assert(!close(1));
+  assert(close(0) == -1);
+  assert(close(1) == -1);
+  assert(open("A", O_TRUNC) == 0);  
+  assert(dup(0) == 1);
+  assert(open("A", O_TRUNC) == 4);
+  assert(!close(1));
+  assert(open("A", O_TRUNC) == 1);
+  assert(dup(0) != 1);
+  assert(dup2(0,1) == 1);
+  
+  return 0;
+}
diff --git a/test/Runtime/POSIX/FD_Fail.c b/test/Runtime/POSIX/FD_Fail.c
new file mode 100644
index 00000000..cf1d4d5a
--- /dev/null
+++ b/test/Runtime/POSIX/FD_Fail.c
@@ -0,0 +1,25 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --libc=uclibc --posix-runtime --init-env %t1.bc --sym-files 0 0 --max-fail 1 > %t.log
+// RUN: grep -q "fread(): ok" %t.log
+// RUN: grep -q "fread(): fail" %t.log
+// RUN: grep -q "fclose(): ok" %t.log
+// RUN: grep -q "fclose(): fail" %t.log
+
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  char buf[1024];  
+  FILE* f = fopen("/etc/fstab", "r");
+  assert(f);
+    
+  int r = fread(buf, 1, 100, f);
+  printf("fread(): %s\n", 
+         r ? "ok" : "fail");
+
+  r = fclose(f);
+  printf("fclose(): %s\n", 
+         r ? "ok" : "fail");
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c
new file mode 100644
index 00000000..c9195f66
--- /dev/null
+++ b/test/Runtime/POSIX/FD_Fail2.c
@@ -0,0 +1,34 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --libc=uclibc --posix-runtime --init-env %t1.bc --sym-files 0 0 --max-fail 1
+// RUN: test -f klee-last/test000001.bout
+// RUN: test -f klee-last/test000002.bout
+// RUN: test -f klee-last/test000003.bout
+// RUN: test -f klee-last/test000004.bout
+// RUN: test -f klee-last/test000005.bout
+// RUN: test -f klee-last/test000006.bout
+// RUN: test -f klee-last/test000007.bout
+
+#include <stdio.h>
+#include <assert.h>
+#include <errno.h>
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <fcntl.h>
+
+int main(int argc, char** argv) {
+  char buf[1024];  
+  int fd = open("/etc/fstab", O_RDONLY);
+  assert(fd != -1);
+    
+  int r = read(fd, buf, 1, 100);
+  if (r != -1)
+    printf("read() succeeded\n");
+  else printf("read() failed with errno %s\n", strerror(errno));
+
+  r = close(fd);
+  if (r != -1)
+    printf("close() succeeded\n");
+  else printf("close() failed with errno %s\n", strerror(errno));
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Fcntl.c b/test/Runtime/POSIX/Fcntl.c
new file mode 100644
index 00000000..139fb1f3
--- /dev/null
+++ b/test/Runtime/POSIX/Fcntl.c
@@ -0,0 +1,17 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --init-env --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+
+#include <assert.h>
+#include <fcntl.h>
+
+int main(int argc, char **argv) {
+  int fd = open("A", O_RDWR|O_TRUNC);
+  if (fd == -1)
+    klee_silent_exit(0);
+  assert(fd == 3);
+  assert((fcntl(fd, F_GETFD) & FD_CLOEXEC) == 0);
+  assert(fcntl(fd, F_SETFD, FD_CLOEXEC, 1) == 0);
+  assert((fcntl(fd, F_GETFD) & FD_CLOEXEC) != 0);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/FilePerm.c b/test/Runtime/POSIX/FilePerm.c
new file mode 100644
index 00000000..818d482f
--- /dev/null
+++ b/test/Runtime/POSIX/FilePerm.c
@@ -0,0 +1,20 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --posix-runtime --init-env %t.bc --sym-files 1 10 --sym-stdout 2>%t.log 
+// RUN: test -f klee-last/test000001.bout
+// RUN: test -f klee-last/test000002.bout
+// RUN: test -f klee-last/test000003.bout
+
+#include <stdio.h>       
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <fcntl.h>
+
+int main(int argc, char** argv) {
+  int fd = open("A", O_RDWR);
+  if (fd != -1)
+    fprintf(stderr, "File 'A' opened successfully\n");
+  else fprintf(stderr, "Cannot open file 'A'\n");
+
+  if (fd != -1)
+    close(fd);
+}
diff --git a/test/Runtime/POSIX/FreeArgv.c b/test/Runtime/POSIX/FreeArgv.c
new file mode 100644
index 00000000..37909b80
--- /dev/null
+++ b/test/Runtime/POSIX/FreeArgv.c
@@ -0,0 +1,20 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --init-env --posix-runtime %t.bc --sym-args 1 1 1
+// RUN: test -f klee-last/test000001.free.err
+// RUN: test -f klee-last/test000002.free.err
+// RUN: test -f klee-last/test000003.free.err
+
+int main(int argc, char **argv) {
+  switch(klee_range(0, 3, "range")) {
+  case 0:
+    free(argv);
+    break;
+  case 1:
+    free(argv[0]);
+    break;
+  case 2:
+    free(argv[1]);
+    break;
+  }
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Getenv.c b/test/Runtime/POSIX/Getenv.c
new file mode 100644
index 00000000..7ec66788
--- /dev/null
+++ b/test/Runtime/POSIX/Getenv.c
@@ -0,0 +1,21 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --init-env --libc=klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+
+#include <assert.h>
+
+int main(int argc, char **argv) {
+  char *g = getenv("PWD");
+  if (g) {
+    printf("have PWD\n");
+  } else {
+    printf("have no PWD\n");
+  }
+
+  g = getenv("HELLO");
+  if (!g || strcmp(g, "nice")==0) {
+    printf("getenv(\"HELLO\") = %p\n", g);
+    if (g) assert(strcmp(getenv("HELLO"),"nice") == 0);
+  }
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Ioctl.c b/test/Runtime/POSIX/Ioctl.c
new file mode 100644
index 00000000..0e7b2cad
--- /dev/null
+++ b/test/Runtime/POSIX/Ioctl.c
@@ -0,0 +1,31 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --init-env --posix-runtime --exit-on-error %t.bc --sym-files 0 4
+
+#include <assert.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <termios.h>
+#include <asm/ioctls.h>
+#include <errno.h>
+#include <stdio.h>
+
+int main(int argc, char **argv) {
+  struct stat s;
+  struct termios ts;
+
+  assert(fstat(0, &s) == 0);
+
+  assert(ioctl(10, FIONREAD, &ts) == -1 && errno == EBADF);
+
+  if (S_ISCHR(s.st_mode)) {
+    printf("is chr\n");
+    assert(ioctl(0, TIOCGWINSZ, &ts) == 0);
+  } else {
+    printf("not chr\n");
+    // I think TC* ioctls basically always fail on nonchr?
+    assert(ioctl(0, TIOCGWINSZ, &ts) == -1);
+    assert(errno == ENOTTY);
+  }
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c
new file mode 100644
index 00000000..6a78dc96
--- /dev/null
+++ b/test/Runtime/POSIX/Isatty.c
@@ -0,0 +1,33 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 0 10 --sym-stdout 2>%t.log
+
+// RUN: test -f klee-last/test000001.bout
+// RUN: test -f klee-last/test000002.bout
+// RUN: test -f klee-last/test000003.bout
+// RUN: test -f klee-last/test000004.bout
+
+// RUN: grep -q "stdin is a tty" %t.log
+// RUN: grep -q "stdin is NOT a tty" %t.log
+// RUN: grep -q "stdout is a tty" %t.log
+// RUN: grep -q "stdout is NOT a tty" %t.log
+
+#include <unistd.h>
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  int fd0 = 0; // stdin
+  int fd1 = 1; // stdout
+
+  int r = isatty(fd0);
+  if (r) 
+    fprintf(stderr, "stdin is a tty\n");
+  else fprintf(stderr, "stdin is NOT a tty\n");
+  
+  r = isatty(fd1);
+  if (r) 
+    fprintf(stderr, "stdout is a tty\n");
+  else fprintf(stderr, "stdout is NOT a tty\n");
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/PrgName.c b/test/Runtime/POSIX/PrgName.c
new file mode 100644
index 00000000..19a56889
--- /dev/null
+++ b/test/Runtime/POSIX/PrgName.c
@@ -0,0 +1,31 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --init-env --posix-runtime --exit-on-error %t2.bc --sym-arg 10 >%t.log
+// RUN: test -f klee-last/test000001.bout
+// RUN: test -f klee-last/test000002.bout
+// RUN: grep -q "No" %t.log
+// RUN: grep -qv "Yes" %t.log
+
+
+/* Simple test for argv[0] */
+
+#include <stdio.h>
+
+int f(int argc, char **argv) {
+
+  if (argv[0][5] == '7')
+    printf("Yes\n");
+  else printf("No\n");
+
+  printf("%c\n", argv[0][5]);
+
+  if (argv[1][1] == 4)
+    printf("4\n");
+  printf("not 4\n");
+
+  return 0;
+}
+
+
+int main(int argc, char **argv) {
+  f(argc, argv);
+}
diff --git a/test/Runtime/POSIX/Read1.c b/test/Runtime/POSIX/Read1.c
new file mode 100644
index 00000000..3b24bfb9
--- /dev/null
+++ b/test/Runtime/POSIX/Read1.c
@@ -0,0 +1,34 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --exit-on-error --posix-runtime --init-env %t.bc --sym-files 1 8 >%t.log
+
+#include <unistd.h>
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <fcntl.h>
+#include <errno.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  char buf[32];
+
+  // If count is zero, read() returns zero and has  no  other  results. (man page)
+  int x = read(0, 0, 0);
+  assert(x == 0);
+  
+  int fd = open("A", O_RDONLY);
+  assert(fd != -1);
+
+  // EFAULT buf is outside your accessible address space. (man page)
+  x = read(fd, 0, 1);
+  assert(x == -1 && errno == EFAULT);
+ 
+  // EBADF  fd is not a valid file descriptor (man page)
+  x = read(-1, buf, 1);
+  assert(x == -1 && errno == EBADF);
+
+  fd = open("A", O_RDONLY);
+  assert(fd != -1);
+  x = read(fd, buf, 1);
+  assert(x == 1);  
+}
+
diff --git a/test/Runtime/POSIX/SELinux.c b/test/Runtime/POSIX/SELinux.c
new file mode 100644
index 00000000..65dd1a7f
--- /dev/null
+++ b/test/Runtime/POSIX/SELinux.c
@@ -0,0 +1,30 @@
+/* Very basic test, as right now SELinux support is extremely basic */
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: %klee --posix-runtime --exit-on-error %t1.bc --sym-arg 2 > %t.log
+// XFAIL: no-selinux
+
+#include <selinux/selinux.h>
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  security_context_t con;
+
+  assert(argc == 2);
+
+  int selinux = is_selinux_enabled();
+  printf("selinux enabled = %d\n", selinux);
+  
+  if (setfscreatecon(argv[1]) < 0)
+    printf("Error: set\n");
+  else printf("Success: set\n");
+  
+  if (getfscreatecon(&con) < 0)
+    printf("Error: get\n");
+  else printf("Success: get\n");
+
+  printf("create_con = %s\n", con);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/SeedAndFail.c b/test/Runtime/POSIX/SeedAndFail.c
new file mode 100644
index 00000000..64cf79bd
--- /dev/null
+++ b/test/Runtime/POSIX/SeedAndFail.c
@@ -0,0 +1,38 @@
+// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc
+// RUN: rm -rf tmp-123
+// RUN: %klee --libc=klee --output-dir=tmp-123 --posix-runtime --init-env %t.bc --sym-files 1 10  2>%t.log
+// RUN: klee --seed-out-dir=tmp-123 --zero-seed-extension --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 1 10 --max-fail 1
+// RUN: ls klee-last | grep -c assert | grep 4
+
+
+
+#include <stdio.h>
+#include <assert.h>
+#include <unistd.h>
+#include <sys/types.h>
+#include <sys/stat.h>
+#include <fcntl.h>
+
+
+int main(int argc, char** argv) {
+  char buf[32];
+  
+  int fd = open("A", O_RDWR | O_CREAT, S_IRWXU);
+  assert(fd != -1);
+  int nbytes = write(fd, "Hello", sizeof("Hello"));
+  assert(nbytes == sizeof("Hello"));
+
+  off_t off = lseek(fd, 0, SEEK_SET);
+  assert(off != (off_t) -1);
+
+  nbytes = read(fd, buf, sizeof("Hello"));
+  assert(nbytes == sizeof("Hello"));
+  
+  int r = close(fd);
+  assert(r == 0);
+
+  r = memcmp(buf, "Hello", sizeof("Hello"));
+  assert(r == 0);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Stdin.c b/test/Runtime/POSIX/Stdin.c
new file mode 100644
index 00000000..065533a1
--- /dev/null
+++ b/test/Runtime/POSIX/Stdin.c
@@ -0,0 +1,56 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --init-env --libc=klee --posix-runtime --exit-on-error %t.bc --sym-files 0 4 > %t.log
+// RUN: grep "mode:file" %t.log
+// RUN: grep "mode:dir" %t.log
+// RUN: grep "mode:chr" %t.log
+// RUN: grep "mode:blk" %t.log
+// RUN: grep "mode:fifo" %t.log
+// RUN: grep "mode:lnk" %t.log
+// RUN: grep "read:sym:yes" %t.log
+// RUN: grep "read:sym:no" %t.log
+
+#include <stdio.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <assert.h>
+
+int main(int argc, char **argv) {
+  struct stat stats;
+  assert(fstat(0, &stats) == 0);
+
+  if (S_ISREG(stats.st_mode)) {
+    printf("mode:file\n");
+  } else if (S_ISDIR(stats.st_mode)) {
+    printf("mode:dir\n");
+  } else if (S_ISCHR(stats.st_mode)) {
+    printf("mode:chr\n");
+  } else if (S_ISBLK(stats.st_mode)) {
+    printf("mode:blk\n");
+  } else if (S_ISFIFO(stats.st_mode)) {
+    printf("mode:fifo\n");
+  } else if (S_ISLNK(stats.st_mode)) {
+    printf("mode:lnk\n");
+  } else if (S_ISSOCK(stats.st_mode)) {
+    printf("mode:sock\n");
+  } else {
+    printf("unknown mode\n");
+  }
+
+  assert(stats.st_size==4);
+
+  if (S_ISREG(stats.st_mode)) {
+    char buf[10];
+    int n = read(0, buf, 5);
+    assert(n == 4);
+    
+    if (strcmp(buf, "HI!")) {
+      printf("read:sym:yes\n");
+    } else {
+      printf("read:sym:no\n");
+    }
+  }
+
+  fflush(stdout);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Write1.c b/test/Runtime/POSIX/Write1.c
new file mode 100644
index 00000000..73902363
--- /dev/null
+++ b/test/Runtime/POSIX/Write1.c
@@ -0,0 +1,23 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --exit-on-error --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
+
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  char buf[32];
+  
+  FILE* f = fopen("A", "w");
+  if (!f)
+    klee_silent_exit(0);
+  fwrite("Hello", sizeof("Hello"), 1, f);
+  fclose(f);
+  
+  f = fopen("A", "r");
+  fread(buf, sizeof("Hello"), 1, f);
+  fclose(f);
+
+  assert(memcmp(buf, "Hello", sizeof("Hello")) == 0);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Write2.c b/test/Runtime/POSIX/Write2.c
new file mode 100644
index 00000000..4865b479
--- /dev/null
+++ b/test/Runtime/POSIX/Write2.c
@@ -0,0 +1,21 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
+// RUN: %klee --exit-on-error --libc=uclibc --posix-runtime --init-env %t.bc --sym-files 1 10 --sym-stdout 2>%t.log
+
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  const char* msg = "This will eventually overflow stdout. ";
+  char buf[32];
+  int i;
+  
+  FILE* f = stdout;//fopen("A", "w");
+  if (!f)
+    klee_silent_exit(0);
+
+  for (i = 0; i < 300; i++)
+    fwrite(msg, sizeof(msg), 1, f);
+  fclose(f);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/dg.exp b/test/Runtime/POSIX/dg.exp
new file mode 100644
index 00000000..88406208
--- /dev/null
+++ b/test/Runtime/POSIX/dg.exp
@@ -0,0 +1,5 @@
+load_lib llvm.exp
+
+if { [klee_supports_posix_runtime] } {
+    RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{ll,llx,c,cpp,tr}]]
+}