Hello, Anton.
KLEE can generate tests only for main function level without any modifications of original code.
This is not actually correct, KLEE will generate inputs for any variable marked as symbolic (by klee_make_symbolic function) no difference whenever this variable in main() function or in any other function, most important that variable is activated for any combination of inputs, otherwise klee will not able to build any paths for this variable.
Same for arguments of the program (argv) and any symbolic files (by the way i were not able to activate symbolic files generation by klee, but maybe you will success…)
First: parsing test code would collect input/output variables and global data.
Yes, will generate any possible paths and generate inputs for the paths.
Second: variating by KLEE of input and global data used by function will provide basic testcase.
Not actually, you should not variate anything, simply necessary to set variables, that will be treated as inputs, symbolic.
Third: generated testcases could be exported to test framewort (e.g. Google Test Framework).
For that is possible to write separate program, that will transfer klee generated data to suitable for Framework format.
I suggest to write a C++ program for example, that will get klee output, located in klee-last folder, as input and generate suitable data (investigate
ktest-tool --write-ints klee-last/test000001.ktest
command).
I suggest for the beginning to look through tutorials from KLEE page:
http://klee.llvm.org/Tutorial-1.html
http://klee.llvm.org/Tutorial-2.html
They provide many useful data.
Hope this helps,
Urmas Repinski.