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
