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
