[klee-dev] analyzing java code with Klee
cristian.zamfir at epfl.ch
Tue Feb 23 00:55:01 PST 2010
As a first step, you can check out this thread where I asked a similar thing on the llvm-dev list.
My initial thoughts after looking at the llvm bitcode generated by vmkit were that you would need to modify Klee quite a bit to be able to analyze the llvm bitcode produced by vmkit, but it should be possible.
On Feb 23, 2010, at 2:40 AM, Andreas Saebjoernsen wrote:
> 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?
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
More information about the klee-dev