diff options
author | Timotej Kapus <tk1713@ic.ac.uk> | 2020-02-25 11:27:27 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-09-17 18:17:25 +0100 |
commit | 730dde87ee6809f2954e59070755dbce9b60e19a (patch) | |
tree | 85babf02b338e5b5a1151ff36ac27d1ee876b631 /test | |
parent | 2eb75ac973f7dace65c4d7179540a658b0113d4c (diff) | |
download | klee-730dde87ee6809f2954e59070755dbce9b60e19a.tar.gz |
Add test for klee-zesti
Diffstat (limited to 'test')
-rw-r--r-- | test/Replay/klee-replay/KleeZesti.c | 103 | ||||
-rw-r--r-- | test/lit.cfg | 1 |
2 files changed, 104 insertions, 0 deletions
diff --git a/test/Replay/klee-replay/KleeZesti.c b/test/Replay/klee-replay/KleeZesti.c new file mode 100644 index 00000000..a6e0cb26 --- /dev/null +++ b/test/Replay/klee-replay/KleeZesti.c @@ -0,0 +1,103 @@ +// -- Core testing commands +// REQUIRES: uclibc +// REQUIRES: posix-runtime +// RUN: rm -rf %t.out +// RUN: rm -f %t.bc +// RUN: mkdir -p %t.out +// RUN: echo -n aaaa > %t.out/aaaa.txt +// RUN: echo -n bbbb > %t.out/bbbb.txt +// RUN: echo -n ccc > %t.out/cccc.txt +// RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc +// RUN: %klee-zesti -only-replay-seeds -libc=uclibc -posix-runtime %t.bc -o -p -q %t.out/bbbb.txt %t.out/cccc.txt < %t.out/aaaa.txt &> %t.out/out.txt +// RUN: FileCheck --input-file=%t.out/out.txt %s + +#include <fcntl.h> +#include <stdio.h> +#include <string.h> +#include <sys/stat.h> +#include <sys/types.h> +#include <unistd.h> + +int check_fd(int fd, const int file_size, const char *file_contents) { + struct stat fs; + char contents[10] = {0}; + + if (fstat(fd, &fs) < 0) + return -1; + + if (fs.st_size != file_size) + return -1; + + read(fd, contents, 10); + + if (strcmp(contents, file_contents) != 0) + return -1; + + return 0; +} + +int check_file(const char *file_name, const int file_size, const char *file_contents) { + int fd; + + if ((fd = open(file_name, O_RDONLY)) < 0) + return -1; + + if (check_fd(fd, file_size, file_contents) < 0) + return -1; + + close(fd); + return 0; +} + +int main(int argc, char **argv) { + if (argc == 6) { + // CHECK-DAG: Got 5 args + printf("Got 5 args\n"); + } + + if (strcmp(argv[1], "-o") == 0) { + // CHECK-DAG: Got -o flag + printf("Got -o flag\n"); + } + + if (strcmp(argv[2], "-p") == 0) { + // CHECK-DAG: Got -p flag + printf("Got -p flag\n"); + } + + if (strcmp(argv[3], "-q") == 0) { + // CHECK-DAG: Got -q flag + printf("Got -q flag\n"); + } + + if (strcmp(argv[4], "A") == 0) { + // CHECK-DAG: Got A file + printf("Got A file\n"); + } + + if (check_file(argv[4], 4, "bbbb") == 0) { + // CHECK-DAG: Got A file size + printf("Got A file size\n"); + } + + if (strcmp(argv[5], "B") == 0) { + // CHECK-DAG: Got B file + printf("Got B file\n"); + } + + // File sizes get increased to the highest among files, so even B has file size 4. + // This is due to the limitaiton of posix-runtime API + if (check_file(argv[5], 4, "ccc") == 0) { + // CHECK-DAG: Got B file size + printf("Got B file size\n"); + } + + if (check_fd(0, 4, "aaaa") == 0) { + // CHECK-DAG: Got stdin file size + printf("Got stdin file size\n"); + } + // CHECK-DAG: KLEE: done: completed paths = 1 + // CHECK-DAG: KLEE: done: generated tests = 1 + + return 0; +} diff --git a/test/lit.cfg b/test/lit.cfg index 86b65d7f..47d1e734 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -131,6 +131,7 @@ if len(kleaver_extra_params) != 0: # to come first, e.g., klee-replay should come before klee subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), ('%klee-replay', 'klee-replay', ''), + ('%klee-zesti', 'klee-zesti', ''), ('%klee','klee', klee_extra_params), ('%ktest-tool', 'ktest-tool', ''), ('%gen-random-bout', 'gen-random-bout', ''), |