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 <
Post by Paul MarinescuThere'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
Post by Vijay GaneshHi,
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?
Post by Vijay GaneshCheers,
Vijay.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev