[klee-dev] Seeding KLEE with a concrete input

[Paul Marinescu]

There's no easy way to do it as far as I know. We did this, among others, in ZESTI (http://srg.doc.ic.ac.uk/projects/zesti/) but it required changes to code.

If you only want to use KLEE, the 'easiest' way to do it would be to somehow create a ktest file corresponding to your concrete input and then use it as a seed for KLEE - there's a command line argument for that. You probably need to make sure that the symbolic objects are created by KLEE in the same order as they appear in the ktest file (i.e. via --sym-args or klee_make_symbolic). I've never tried this though and can't guarantee it.

Paul

> On 14 Nov 2013, at 02:52, Vijay Ganesh <hellovijay at gmail.com> wrote:
> 
> Hi,
> 
> I want to seed KLEE with a concrete input, i.e., I only care about the symbolic expression corresponding to the path taken by the program on a concrete input. How can I force KLEE to just produce that one path constraint?
> 
> Cheers,
> Vijay.
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev