Merge pull request #155 from MartinNowack/fix_fd_fail2

Fix testcase FD_Fail2.c

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..c2e5596b 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
+// RUN: not 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;