about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-06-09 23:06:41 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2023-06-11 19:23:24 +0100
commitc10e9e926700773e01f44fbb1917deac7be2aaea (patch)
tree7abfceec757330360ec5d4be383e4c7a5a8933b7 /test
parentdab1c0fa376771be1c3cdd5b8d564484755907dd (diff)
downloadklee-c10e9e926700773e01f44fbb1917deac7be2aaea.tar.gz
Rewrote has_permission in the POSIX runtime. We now only return with permission error a single time in symbolic execution mode.
The rewrite also fixes a bug reported in #1230.
Rewrote the FilePerm.c test accordingly.
Diffstat (limited to 'test')
-rw-r--r--test/Runtime/POSIX/FilePerm.c15
1 files changed, 10 insertions, 5 deletions
diff --git a/test/Runtime/POSIX/FilePerm.c b/test/Runtime/POSIX/FilePerm.c
index 418e3717..5fc9924f 100644
--- a/test/Runtime/POSIX/FilePerm.c
+++ b/test/Runtime/POSIX/FilePerm.c
@@ -1,21 +1,26 @@
+/* This test checks that when opening a symbolic file in R/W mode, we return exactly twice: 
+   once successfully, and the other time with a permission error */
+
 // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-files 1 10 --sym-stdout 2>%t.log 
+// RUN: %klee --output-dir=%t.klee-out --posix-runtime %t.bc --sym-files 1 10 | FileCheck %s
 // 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: not test -f %t.klee-out/test000003.ktest
 
 #include <stdio.h>       
 #include <sys/types.h>
 #include <sys/stat.h>
 #include <fcntl.h>
+#include <unistd.h>
 
 int main(int argc, char** argv) {
   int fd = open("A", O_RDWR);
   if (fd != -1)
-    fprintf(stderr, "File 'A' opened successfully\n");
-  else fprintf(stderr, "Cannot open file 'A'\n");
-
+    printf("File 'A' opened successfully\n");
+  // CHECK-DAG: File 'A' opened successfully
+  else printf("Cannot open file 'A'\n");
+  // CHECK-DAG: Cannot open file 'A'
   if (fd != -1)
     close(fd);
 }