Hi, I'm struggling to figure out how to replay generated test cases with symbolic files.
I see in the documentation that there are two ways to replay test cases. 1. (As shown in: https://klee.github.io/tutorials/testing-function/) is to run the executable with the KTEST_FILE flag set to a .ktest file. 2. (As shown in: https://klee.github.io/tutorials/testing-coreutils/) is to use klee-replay My intuition is that the KTEST_FILE method won't work since there is no call to klee_make_symbolic to intercept. I'm not sure why the second method fails. I've included my attempt at both methods. I've included a tester file for reproduction, the command I used to launch KLEE and KLEE-replay, and the behavior I saw. -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Here is the tester I wrote up: #include <stdio.h> #include <stdlib.h> #include <klee/klee.h> int main(int argc, char **argv) { char buf[1]; FILE *file = fopen(argv[1], "r"); if ( file != NULL ) { fread(buf, 1, 1, file); } fclose(file); printf("%d", buf[0]); return 0; } -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- I generate files with the following command: $ klee --libc=uclibc --posix-runtime --min-query-time-to-log=-1 --max-solver-time=10 --max-time=21600 --max-memory=4096 --simplify-sym-indices --write-cvcs --write-cov --dump-states-on-halt=false --disable-inlining --use-forked-solver --use-cex-cache --allow-external-sym-calls -write-test-info --max-instruction-time=30. --watchdog test5-cov-outputs-klee.bc A -sym-files 1 32 -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- And I get the following behavior: $ KTEST_FILE=./klee-last/test000001.ktest ./tester Segmentation fault $ klee-replay ./tester klee-last/test000001.ktest klee-replay: TEST CASE: klee-last/test000001.ktest klee-replay: ARGS: "./tester" "A" warning: check_file A: dev mismatch: 2049 vs 0 warning: check_file A: mode mismatch: 0100000 vs 0 warning: check_file A: nlink mismatch: 1 vs 0 warning: check_file A: blksize mismatch: 4096 vs 0 klee-replay: EXIT STATUS: CRASHED signal 11 (0 seconds) Thanks, Daniel Schwartz
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev