Hi Cristi, Given you experience it sounds like the design of Klee and/or vmkit makes it so that this task is quite prohibitive. I am curious though what in the vmkit bytecode makes it different from llvm-gcc bytecode with respect to Klee?
thanks, Andreas But Nicolas suggests generating a .so with vmkit and analyzing that On Tue, Feb 23, 2010 at 12:55 AM, Cristian Zamfir <cristian.zamfir at epfl.ch>wrote: > 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 > > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100225/a7de5c68/attachment.html
