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 <[email protected]> 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 >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
