Using OpenJDK for static analysis
fweimer at redhat.com
Tue Feb 11 12:59:27 UTC 2014
On 02/11/2014 01:11 AM, Pascal Kesseli wrote:
> We are developing a bounded model checker for C/C++ called CBMC here at the
> University of Oxford. We're currently evaluating different options to
> implement a Java frontend for the program, allowing us to statically verify
> Java code as well.
> There's obviously a whole series of problems to be tackled before this is
> possible, one of which is the following: In order to provide a reasonable
> scope, the verifier needs to know the semantics of native JRE library code.
> One way of allowing us to do so is for our program to model JNI and use
> OpenJDK's C/C++ implementations to determine the semantics of such a method
> call in Java.
jdk7u-dev isn't the right mailing list for this question. The discuss
list might be better (and I'm redirecting it there), but officially, I
think such questions should be posted to the forums (which I don't
> This approach begs the following questions:
> 1.) Are all native runtime library operations in OpenJDK implemented in
> proper JNI or are there exceptions and caveats to this approach?
There are exceptions, like methods that won't work properly when not
> 2.) Are the implementations of these functions reasonably detached from
> each other and the rest of the VM, such that they can be analysed in
There was a proposal to write to documentation:
But I don't think this was ever turned into a real JEP, and I haven't
seen the documentation.
Florian Weimer / Red Hat Product Security Team
More information about the discuss