Hi Daniel, I think the first method doesn't understand symbolic inputs specified by '--posix-runtime', so you're right.
Isn't it an expected result for the second method? If 'A' doesn't exist or is unreadable then the program crashes on fclose(NULL); test000001 probably specifies an unreadable case. If there is an test000002, it should be the not-null case. Regards, Yude On Fri, Aug 4, 2017 at 7:35 AM, Daniel Schwartz <[email protected]> wrote: > 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 > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
