diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-09-19 14:03:58 +0100 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2018-09-20 21:49:58 +0100 |
commit | 86ad40951ff303b7dc8cc2492900ca5d82ff4d6f (patch) | |
tree | 0b32e5f516676d232d4efc5c71347f6cb5e2d76e /test/Runtime/POSIX/DirSeek.c | |
parent | c05a0dc1d61187b3ac95c56b0d660731946218fd (diff) | |
download | klee-86ad40951ff303b7dc8cc2492900ca5d82ff4d6f.tar.gz |
Updated DirSeek test to use --sym-stdin instead of --sym-files 0 x to make stdin symbolic.
Diffstat (limited to 'test/Runtime/POSIX/DirSeek.c')
-rw-r--r-- | test/Runtime/POSIX/DirSeek.c | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/test/Runtime/POSIX/DirSeek.c b/test/Runtime/POSIX/DirSeek.c index 4c68a30c..821ff8f5 100644 --- a/test/Runtime/POSIX/DirSeek.c +++ b/test/Runtime/POSIX/DirSeek.c @@ -7,7 +7,7 @@ // RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2 // RUN: rm -rf %t.klee-out %t.klee-out-tmp // RUN: %gentmp %t.klee-out-tmp -// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 0 2 +// RUN: %klee --output-dir=%t.klee-out --run-in=%t.klee-out-tmp --libc=uclibc --posix-runtime --exit-on-error %t2.bc --sym-files 1 2 --sym-stdin 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 @@ -15,10 +15,8 @@ // Therefore gentmp generates a directory with a specific amount of entries #include <assert.h> -#include <stdio.h> -#include <stdlib.h> +#include <sys/types.h> #include <dirent.h> -#include <sys/stat.h> #include <errno.h> #include <string.h> @@ -54,7 +52,7 @@ int main(int argc, char **argv) { rewinddir(d); de = readdir(d); assert(de); - assert(strcmp(de->d_name, first) == 0); + assert(strcmp(de->d_name, first) == 0); closedir(d); return 0; |