[klee-dev] Using KLEE to generate a test suite for Sed
peshko at gatech.edu
Thu Oct 29 10:46:09 PDT 2009
I wanted to use KLEE to generate a Test suite for one of my research subjects
- Sed. I installed KLEE and the uclibc library and ran KLEE in the following
$klee --libc=uclibc --posix-runtime --init-env sed.bc --sym-args
0 3 5 --sym-files 0 2 10
My intend is to run KLEE with up to 3 symbolic program arguments and 2
symbolic files with max length of 10. I let KLEE run for about 10 hours and it
generated 2-3 thousands of test cases. I was surprised that the coverage of
the test suite was very low, and I am not sure why this is the case. The
source code of Sed is ~ 15K lines.
Am I using klee incorrectly?
More information about the klee-dev