[klee-dev] Reusing results of symbolic analysis

[Super Zhang]

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
-------------- next part --------------
HTML attachment scrubbed and removed