[klee-dev] Use Klee with Java?

[Zhenyu Zhou]

OK I see.. Thank you so much! I'll take a look at the tools you suggested.

Zhenyu

On Sun, Jun 21, 2015 at 6:02 PM, Sean Bartell <sean at yotann.org> wrote:

> Zhenyu Zhou on 2015-06-20:
>
>  I'm looking for a tool for symbolic execution and find that Klee is a
>> fantastic tool. But now I'm wondering whether Klee can analyse JAVA codes
>> (or class files)? I have searched in the mail list and found the same
>> question is posted several years ago. Does anyone know are there any
>> progresses in this direction?
>>
>
> KLEE only understands LLVM bitcode--this is part of the fundamental design
> of KLEE. If you need to use KLEE on Java code, you might be able to use
> RoboVM[0] or VMKit[1] (unmaintained) to convert Java into LLVM bitcode.
> However, this will require a lot of work to get usable bitcode, especially
> when you have to deal with Java libraries and OS interaction.
>
> It will be much easier to use a Java-specific tool instead of KLEE, such
> as JPF-symbc[2].
>
> [0] http://docs.robovm.com/
> [1] http://vmkit.llvm.org/
> [2] http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc
>
-------------- next part --------------
HTML attachment scrubbed and removed