I ever used both methods as Paul mentioned. zesti is cool, it could automatically use your concrete command line parameters as search seeds. But you need to use zesti code base:).
For the second method, you could use gen-random-bout tool(under the same folder of your klee binary, source code location: tools/gen-random-bout/gen-random-bout.cpp) for example, you could generate a random ktest file with this command line: gen-random-bout 100 --sym-args 0 2 2 --sym-files 1 8 check the generated file.bout under the current folder. For your specific purpose, you could just copy KTest.h and KTest.cpp file out of klee project and make a standalone program to convert your concrete inputs into ktest files to feed klee with the command line option --seed-out. Still, gen-random-bout.cpp will be a great example for how to do this. Chaoqiang Super On Thu, Nov 14, 2013 at 6:03 AM, Paul Marinescu < [email protected]> wrote: > 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 <[email protected]> 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 > > [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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
