[klee-dev] Generate multiple concrete inputs to cover each path‏

[jiaquan]

Hello All, 
I would like to know if it's possible to generate multiple concrete inputs/tests to cover each path of a test program, with or without modifying KLEE's source code.
I'm new to KLEE and have just gone through the tutorials on klee.llvm.org. In my experience, I noticed that KLEE only produces one concrete input/test for each path of a test program. 
I'm wondering if there's a command line option to let KLEE produce more than one concrete input/test per path? If not, is there another way to achieve this?
On top of my head, the options are:
A. Rerun KLEE multiple times to get different sets of inputs/tests. I have tried this, but I could only see the same inputs/tests getting repeated over and over again. Is there a way to let KLEE generate randomized inputs/tests across different runs?
B. Dump all symbolic inputs/tests generated by KLEE to a file and parse it myself. Is there a command line switch to make such a dump?
C. Re-write KLEE's code that converts a symbolic input to a concrete input. If I have to do this, which part of the code should I look into?
Your help would be greatly appreciated!
Regards,Charlie
 		 	   		  
-------------- next part --------------
HTML attachment scrubbed and removed