Using OpenJDK for static analysis

Florian Weimer fweimer at
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
> isolation?

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 mailing list