From a36cc972f9a8b56f48d90a5c99b9a5cb02a00a3c Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 29 Apr 2014 09:18:29 +0200 Subject: Fix testcase FD_Fail2.c Major issue was that puts was used for the succeed printf calls. With newer gcc/clang versions, printf is always used. The former took different code paths leading to much more possibilities to trigger failed writes and therefore generating more test cases. This patch avoids the generation of puts. And checks for the 4 possible generated test cases for 2 possible errors. --- test/Runtime/POSIX/FD_Fail2.c | 18 +++++++++++------- 1 file 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 #include @@ -18,7 +21,8 @@ #include 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; -- cgit 1.4.1 From 448872a3e885dec5c4ef402e179af17f185a32c0 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sun, 14 Sep 2014 20:12:34 +0200 Subject: Use not test instead of non-existing FAIL. --- test/Runtime/POSIX/FD_Fail2.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Runtime/POSIX/FD_Fail2.c b/test/Runtime/POSIX/FD_Fail2.c index cdf1303e..c2e5596b 100644 --- a/test/Runtime/POSIX/FD_Fail2.c +++ b/test/Runtime/POSIX/FD_Fail2.c @@ -10,7 +10,7 @@ // RUN: test -f %t.klee-out/test000002.ktest // RUN: test -f %t.klee-out/test000003.ktest // RUN: test -f %t.klee-out/test000004.ktest -// FAIL: test -f %t.klee-out/test000005.ktest +// RUN: not test -f %t.klee-out/test000005.ktest #include #include -- cgit 1.4.1