[klee-dev] Using KLEE to generate a test suite for Sed

[Petar Tsankov]

Hello,

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 
way:

$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?

Thanks,
Petar