about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--runtime/POSIX/fd.c22
l---------runtime/POSIX/testing-dir/a1
l---------runtime/POSIX/testing-dir/b1
-rwxr-xr-xruntime/POSIX/testing-dir/c2
-rw-r--r--runtime/POSIX/testing-dir/d0
-rw-r--r--runtime/POSIX/testing-env27
-rw-r--r--test/Runtime/POSIX/Isatty.c4
7 files changed, 14 insertions, 43 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/runtime/POSIX/testing-env b/runtime/POSIX/testing-env
deleted file mode 100644
index 5a6e8eb8..00000000
--- a/runtime/POSIX/testing-env
+++ /dev/null
@@ -1,27 +0,0 @@
-# This file is sourced prior to running the testing environment, make
-# sure to quote things.
-
-export TERM="xterm"
-export SHELL="/bin/bash"
-export LS_COLORS="no=00:fi=00:di=01;34:ln=01;36:pi=40;33:so=01;35:do=01;35:bd=40;33;01:cd=40;33;01:or=40;31;01:su=37;41:sg=30;43:tw=30;42:ow=34;42:st=37;44:ex=01;32:*.tar=01;31:*.tgz=01;31:*.arj=01;31:*.taz=01;31:*.lzh=01;31:*.zip=01;31:*.z=01;31:*.Z=01;31:*.gz=01;31:*.bz2=01;31:*.deb=01;31:*.rpm=01;31:*.jar=01;31:*.jpg=01;35:*.jpeg=01;35:*.gif=01;35:*.bmp=01;35:*.pbm=01;35:*.pgm=01;35:*.ppm=01;35:*.tga=01;35:*.xbm=01;35:*.xpm=01;35:*.tif=01;35:*.tiff=01;35:*.png=01;35:*.mov=01;35:*.mpg=01;35:*.mpeg=01;35:*.avi=01;35:*.fli=01;35:*.gl=01;35:*.dl=01;35:*.xcf=01;35:*.xwd=01;35:*.flac=01;35:*.mp3=01;35:*.mpc=01;35:*.ogg=01;35:*.wav=01;35:"
-export PATH="/usr/local/bin:/usr/bin:/bin"
-export COLORTERM="gnome-terminal"
-export LC_ALL=C
-export TABSIZE=8
-export COLUMNS=80
-
-#       1 BLOCK_SIZE
-#       2 COLUMNS
-#       1 DF_BLOCK_SIZE
-#       1 DU_BLOCK_SIZE
-#       1 HOME
-#       1 LS_BLOCK_SIZE
-#       1 LS_COLORS
-#      11 POSIXLY_CORRECT
-#       1 QUOTING_STYLE
-#       3 SHELL
-#       4 SIMPLE_BACKUP_SUFFIX
-#       1 TABSIZE
-#       2 TERM
-#       2 TIME_STYLE
-#       4 TMPDIR
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>
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-05 14:04:35 +0000