From 80d67650524c92a378227d0f842a9e9a17fee599 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 25 Mar 2022 22:17:30 +0000 Subject: Updated tests to use ktest-gen instead of gen-bout --- test/CMakeLists.txt | 2 +- test/Replay/klee-replay/GenBout.c | 76 -------------------------------------- test/Replay/klee-replay/KTestGen.c | 76 ++++++++++++++++++++++++++++++++++++++ test/lit.cfg | 2 +- 4 files changed, 78 insertions(+), 78 deletions(-) delete mode 100644 test/Replay/klee-replay/GenBout.c create mode 100644 test/Replay/klee-replay/KTestGen.c (limited to 'test') diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 16d20e1c..42b28a7c 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -151,7 +151,7 @@ file(GENERATE add_custom_target(systemtests COMMAND "${LIT_TOOL}" ${LIT_ARGS} "${CMAKE_CURRENT_BINARY_DIR}" - DEPENDS klee kleaver klee-replay kleeRuntest gen-bout gen-random-bout + DEPENDS klee kleaver klee-replay kleeRuntest ktest-gen gen-random-bout COMMENT "Running system tests" USES_TERMINAL ) diff --git a/test/Replay/klee-replay/GenBout.c b/test/Replay/klee-replay/GenBout.c deleted file mode 100644 index 1f60ed0c..00000000 --- a/test/Replay/klee-replay/GenBout.c +++ /dev/null @@ -1,76 +0,0 @@ -// -- Core testing commands -// RUN: rm -rf %t.out -// RUN: rm -f %t.bout -// RUN: mkdir -p %t.out -// RUN: echo -n aaaa > %t.out/aaaa.txt -// RUN: echo -n bbbb > %t.out/bbbb.txt -// RUN: echo -n cccc > %t.out/cccc.txt -// RUN: %gen-bout -o -p -q file1 --bout-file %t.bout --sym-stdin %t.out/aaaa.txt --sym-file %t.out/bbbb.txt --sym-stdout %t.out/cccc.txt -// RUN: %cc %s -O0 -o %t -// RUN: %klee-replay %t %t.bout 2> %t.out/out.txt -// RUN: FileCheck --input-file=%t.out/out.txt %s - -// CHECK: KLEE-REPLAY: NOTE: EXIT STATUS: NORMAL - -#include -#include -#include -#include -#include -#include - -int check_fd(int fd, const int file_size) { - struct stat fs; - - if (fstat(fd, &fs) < 0) - return -1; - - if (fs.st_size != file_size) - return -1; - - return 0; -} - -int check_file(const char *file_name, const int file_size) { - int fd; - - if ((fd = open(file_name, O_RDONLY)) < 0) - return -1; - - if (check_fd(fd, file_size) < 0) - return -1; - - close(fd); - return 0; -} - -int main(int argc, char **argv) { - if (argc != 5) - return 1; - - if (strcmp(argv[1], "-o")) - return 1; - - if (strcmp(argv[2], "-p")) - return 1; - - if (strcmp(argv[3], "-q")) - return 1; - - if (strcmp(argv[4], "file1")) - return 1; - - if (check_file("A", 4)) - return 1; - - if (check_fd(0, 4)) - return 1; - - if (check_fd(1, 1024)) - return 1; - - printf("tests passed\n"); - - return 0; -} - diff --git a/test/Replay/klee-replay/KTestGen.c b/test/Replay/klee-replay/KTestGen.c new file mode 100644 index 00000000..de031501 --- /dev/null +++ b/test/Replay/klee-replay/KTestGen.c @@ -0,0 +1,76 @@ +// -- Core testing commands +// RUN: rm -rf %t.out +// RUN: rm -f %t.bout +// RUN: mkdir -p %t.out +// RUN: echo -n aaaa > %t.out/aaaa.txt +// RUN: echo -n bbbb > %t.out/bbbb.txt +// RUN: echo -n cccc > %t.out/cccc.txt +// RUN: %ktest-gen -o -p -q file1 --bout-file %t.bout --sym-stdin %t.out/aaaa.txt --sym-file %t.out/bbbb.txt --sym-stdout %t.out/cccc.txt +// RUN: %cc %s -O0 -o %t +// RUN: %klee-replay %t %t.bout 2> %t.out/out.txt +// RUN: FileCheck --input-file=%t.out/out.txt %s + +// CHECK: KLEE-REPLAY: NOTE: EXIT STATUS: NORMAL + +#include +#include +#include +#include +#include +#include + +int check_fd(int fd, const int file_size) { + struct stat fs; + + if (fstat(fd, &fs) < 0) + return -1; + + if (fs.st_size != file_size) + return -1; + + return 0; +} + +int check_file(const char *file_name, const int file_size) { + int fd; + + if ((fd = open(file_name, O_RDONLY)) < 0) + return -1; + + if (check_fd(fd, file_size) < 0) + return -1; + + close(fd); + return 0; +} + +int main(int argc, char **argv) { + if (argc != 5) + return 1; + + if (strcmp(argv[1], "-o")) + return 1; + + if (strcmp(argv[2], "-p")) + return 1; + + if (strcmp(argv[3], "-q")) + return 1; + + if (strcmp(argv[4], "file1")) + return 1; + + if (check_file("A", 4)) + return 1; + + if (check_fd(0, 4)) + return 1; + + if (check_fd(1, 1024)) + return 1; + + printf("tests passed\n"); + + return 0; +} + diff --git a/test/lit.cfg b/test/lit.cfg index 0d7aa1ed..c44575c0 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -136,7 +136,7 @@ subs = [ ('%kleaver', 'kleaver', kleaver_extra_params), ('%klee','klee', klee_extra_params), ('%ktest-tool', 'ktest-tool', ''), ('%gen-random-bout', 'gen-random-bout', ''), - ('%gen-bout', 'gen-bout', '') + ('%ktest-gen', 'ktest-gen', '') ] for s,basename,extra_args in subs: config.substitutions.append( -- cgit 1.4.1