diff options
| -rw-r--r-- | test/Runtime/POSIX/FD_Fail2.c | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c index 74957597..cdf1303e 100644 --- a/test/Runtime/POSIX/FD_Fail2.c +++ b/test/Runtime/POSIX/FD_Fail2.c @@ -1,13 +1,16 @@ // RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --search=dfs %t1.bc --sym-files 1 10 --max-fail 1 +// RUN: %klee --output-dir=%t.klee-out --libc=uclibc --posix-runtime --search=dfs %t1.bc --sym-files 1 10 --max-fail 2 +// +// Check that generated assembly doesn't use puts to output strings +// RUN: FileCheck -input-file=%t.klee-out/assembly.ll %s +// CHECK-NOT: puts +// // RUN: test -f %t.klee-out/test000001.ktest // RUN: test -f %t.klee-out/test000002.ktest // RUN: test -f %t.klee-out/test000003.ktest // RUN: test -f %t.klee-out/test000004.ktest -// RUN: test -f %t.klee-out/test000005.ktest -// RUN: test -f %t.klee-out/test000006.ktest -// RUN: test -f %t.klee-out/test000007.ktest +// FAIL: test -f %t.klee-out/test000005.ktest #include <stdio.h> #include <assert.h> @@ -18,7 +21,8 @@ #include <stdio.h> int main(int argc, char** argv) { - char buf[1024]; + char buf[1024]; + // Open the symbolic file "A" int fd = open("A", O_RDONLY); assert(fd != -1); @@ -26,12 +30,12 @@ int main(int argc, char** argv) { r = read(fd, buf, 1, 5); if (r != -1) - printf("read() succeeded\n"); + printf("read() succeeded %u\n", fd); else printf("read() failed with error '%s'\n", strerror(errno)); r = close(fd); if (r != -1) - printf("close() succeeded\n"); + printf("close() succeeded %u\n", fd); else printf("close() failed with error '%s'\n", strerror(errno)); return 0; |