Hi, A question with regard to replay seeds with standard input. Say, I have a program 'replace', which accept two strings pat, sub, and a standard input file, and output to standard output file.
klee klee --libc=uclibc --posix-runtime replace abc def < a.txt will actually run the program concretely, and generate a ktest file. then, I want to replay this test case from klee-out-* folder, for doing that, I tried some ways, they didn't work. klee klee --libc=uclibc --posix-runtime --only-replay-seeds --seed-out-dir=klee-out-0/ replace.o --sym-arg 3 --sym-arg 3 < a.txt the one below does not work either: klee klee --libc=uclibc --posix-runtime --only-replay-seeds --seed-out-dir=klee-out-0/ replace.o --sym-arg 3 --sym-arg 3 --sym-files 1 100 Basically, I want to put the content of standard input content into the generated ktest file. If it's not possible, is there a way I redirect a file content to standard intput when I replay seeds with symbolic input? Regards, Chaoqiang
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
