The problem is that if you run a program concretely, you will get no seeds with KLEE (for command line arguments or input files). This is a sensible thing to do, since you can use the same concrete values as input and you will get the same results. Perhaps your usage scenario is a bit more complex than what your email explains?
In any case, you can a) modify KLEE to make all inputs symbolic then constrain them to have a single value b) use a fork of KLEE called ZESTI which already does what you want among other things. It's available at http://srg.doc.ic.ac.uk/projects/zesti/ . To use it, you just need to add an extra argument to the command line (--zest) Paul On 19 Feb 2013, at 05:45, Super Zhang <[email protected]> wrote: > 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
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
