diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-06-09 23:06:41 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2023-06-11 19:23:24 +0100 |
commit | c10e9e926700773e01f44fbb1917deac7be2aaea (patch) | |
tree | 7abfceec757330360ec5d4be383e4c7a5a8933b7 /test/Runtime | |
parent | dab1c0fa376771be1c3cdd5b8d564484755907dd (diff) | |
download | klee-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.c | 15 |
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); } |