[klee-dev] Reusing results of symbolic analysis
Paul Marinescu
paul.marinescu at imperial.ac.uk
Fri Feb 22 12:37:17 GMT 2013
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
More information about the klee-dev
mailing list