On Dec 31, 2010, at 12:37 PM, Shuying Liang wrote: > wrote a simple parser using flex/bison, making the parser accept > string input(size of 64 or 1024), > then make the string symbolic in klee, and let klee generate test > cases for the parser. > It turns out that the test cases starts from all 0x00, to some random > values. and also the parser keeps reporting syntax errors (of course). > and the whole program seems to be never stop. > > The conclusion is that klee can not really test structured input to > test parser.
You might want to look at these papers, which address this very issue: http://people.csail.mit.edu/akiezun/pldi-kiezun.pdf http://www.cs.ucla.edu/~rupak/Papers/Directed_test_generation_with_symbolic_grammars Also, section 5.3 of this paper http://people.csail.mit.edu/akiezun/issta54-kiezun.pdf discusses actually using KLEE on a program expecting structured input, with the help of the string solver Hampi to restrict inputs to a given grammar. I've been looking into this myself recently, so if you want to run experiments like those in this paper, send me an email off-list and I'll see if I can help. Elnatan
