[klee-dev] analyzing java code with Klee

[Cristian Zamfir]

Hi Andreas, 

As a first step, you can check out this thread where I asked a similar thing on the llvm-dev list.
http://lists.cs.uiuc.edu/pipermail/llvmdev/2009-August/024849.html

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. 

Cristi 


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?
> 
> thanks,
> Andreas
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev