[klee-dev] Reusing results of symbolic analysis

[Paul Marinescu]

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 <chaoqiang.zhang at gmail.com> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed