about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorTimotej Kapus <tk1713@ic.ac.uk>2020-02-25 11:27:27 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-09-17 18:17:25 +0100
commit730dde87ee6809f2954e59070755dbce9b60e19a (patch)
tree85babf02b338e5b5a1151ff36ac27d1ee876b631
parent2eb75ac973f7dace65c4d7179540a658b0113d4c (diff)
downloadklee-730dde87ee6809f2954e59070755dbce9b60e19a.tar.gz
Add test for klee-zesti
-rw-r--r--test/Replay/klee-replay/KleeZesti.c103
-rw-r--r--test/lit.cfg1
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', ''),