I am considering using Klee for analyzing Java code and I have a question regarding the feasibility of this. The reason why I am considering this is that it seems like Klee can take any llvm bytecode as input. VMKit is capable of producing llvm bytecode for java, which is what llvm-gcc produce as well, but on the Klee webpage llvm-gcc is listed as the only option for generating bytecode. That it is the only option does not have to mean too much, but at the same time I want to double check to make sure that I am not heading down the wrong path.
Is there anything in Klee that makes it so that it can only analyze llvm bytecode from llvm-gcc or can it also be used to analyze the llvm bytecode produced by llvm-vmkit? thanks, Andreas -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100222/f2516320/attachment.html
