Merge pull request #69 from MartinNowack/fix_runtime_posix

Fix runtime posix

6 files changed, 14 insertions, 16 deletions

diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index 09dd7be5..1c75cd76 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -35,7 +35,7 @@ void klee_warning(const char*);
 void klee_warning_once(const char*);
 int klee_get_errno(void);
 
-/* Returns pointer to the symbolic file structure is the pathname is symbolic */
+/* Returns pointer to the symbolic file structure fs the pathname is symbolic */
 static exe_disk_file_t *__get_sym_file(const char *pathname) {
   char c = pathname[0];
   unsigned i;
@@ -489,15 +489,15 @@ off64_t __fd_lseek(int fd, off64_t offset, int whence) {
        the offset, but really directories should only be SEEK_SET, so
        this solves the problem. */
     if (whence == SEEK_SET) {
-      new_off = syscall(__NR_lseek, f->fd, (int) offset, SEEK_SET);
+      new_off = syscall(__NR_lseek, f->fd, offset, SEEK_SET);
     } else {
-      new_off = syscall(__NR_lseek, f->fd, (int) f->off, SEEK_SET);
+      new_off = syscall(__NR_lseek, f->fd, f->off, SEEK_SET);
 
       /* If we can't seek to start off, just return same error.
          Probably ESPIPE. */
       if (new_off != -1) {
         assert(new_off == f->off);
-        new_off = syscall(__NR_lseek, f->fd, (int) offset, whence);
+        new_off = syscall(__NR_lseek, f->fd, offset, whence);
       }
     }
 
@@ -818,7 +818,7 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) {
     errno = EBADF;
     return -1;
   }
-  
+
   if (f->dfile) {
     klee_warning("symbolic file, ignoring (EINVAL)");
     errno = EINVAL;
@@ -826,7 +826,7 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) {
   } else {
     if ((unsigned long) f->off < 4096u) {
       /* Return our dirents */
-      unsigned i, pad, bytes=0;
+      off64_t i, pad, bytes=0;
 
       /* What happens for bad offsets? */
       i = f->off / sizeof(*dirp);
@@ -856,10 +856,12 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) {
       dirp->d_off = 4096;
       bytes += dirp->d_reclen;
       f->off = pad;
+
       return bytes;
     } else {
-      unsigned os_pos = f->off - 4096;
-      int res, s;
+      off64_t os_pos = f->off - 4096;
+      int res;
+      off64_t s = 0;
 
       /* For reasons which I really don't understand, if I don't
          memset this then sometimes the kernel returns d_ino==0 for
@@ -869,14 +871,13 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) {
          Even more bizarre, interchanging the memset and the seek also
          case strange behavior. Really should be debugged properly. */
       memset(dirp, 0, count);
-      s = syscall(__NR_lseek, f->fd, (int) os_pos, SEEK_SET);
+      s = syscall(__NR_lseek, f->fd, os_pos, SEEK_SET);
       assert(s != (off64_t) -1);
       res = syscall(__NR_getdents64, f->fd, dirp, count);
       if (res == -1) {
         errno = klee_get_errno();
       } else {
         int pos = 0;
-
         f->off = syscall(__NR_lseek, f->fd, 0, SEEK_CUR) + 4096;
 
         /* Patch offsets */
@@ -885,6 +886,7 @@ int __fd_getdents(unsigned int fd, struct dirent64 *dirp, unsigned int count) {
           struct dirent64 *dp = (struct dirent64*) ((char*) dirp + pos);
           dp->d_off += 4096;
           pos += dp->d_reclen;
+
         }
       }
       return res;
diff --git a/runtime/POSIX/testing-dir/a b/runtime/POSIX/testing-dir/a
deleted file mode 120000
index dc1dc0cd..00000000
--- a/runtime/POSIX/testing-dir/a
+++ /dev/null
@@ -1 +0,0 @@
-/dev/null
\ No newline at end of file
diff --git a/runtime/POSIX/testing-dir/b b/runtime/POSIX/testing-dir/b
deleted file mode 120000
index b9251ec6..00000000
--- a/runtime/POSIX/testing-dir/b
+++ /dev/null
@@ -1 +0,0 @@
-/dev/random
\ No newline at end of file
diff --git a/runtime/POSIX/testing-dir/c b/runtime/POSIX/testing-dir/c
deleted file mode 100755
index 2b45f6a5..00000000
--- a/runtime/POSIX/testing-dir/c
+++ /dev/null
@@ -1,2 +0,0 @@
-#!/bin/sh
-echo "Hello world!"
diff --git a/runtime/POSIX/testing-dir/d b/runtime/POSIX/testing-dir/d
deleted file mode 100644
index e69de29b..00000000
--- a/runtime/POSIX/testing-dir/d
+++ /dev/null
diff --git a/test/Runtime/POSIX/Isatty.c b/test/Runtime/POSIX/Isatty.c
index 4f8d1425..293ee653 100644
--- a/test/Runtime/POSIX/Isatty.c
+++ b/test/Runtime/POSIX/Isatty.c
@@ -1,16 +1,16 @@
 // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc
 // RUN: %klee --libc=uclibc --posix-runtime %t.bc --sym-files 0 10 --sym-stdout 2>%t.log
-
 // RUN: test -f klee-last/test000001.ktest
 // RUN: test -f klee-last/test000002.ktest
 // RUN: test -f klee-last/test000003.ktest
 // RUN: test -f klee-last/test000004.ktest
-
 // 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
 
+// Depending on how uClibc is compiled (i.e. without -DKLEE_SYM_PRINTF)
+// fprintf prints out on stdout even stderr is provided.
 #include <unistd.h>
 #include <stdio.h>
 #include <assert.h>