aboutsummaryrefslogtreecommitdiffhomepage
path: root/test/Runtime
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/Runtime
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/Runtime')
-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);
}