Although in most cases class initialization works as expected, some static fields may be read before being initialized, despite being initialized in their corresponding class initializer. We propose an analysis that can be applied to identify the static fields that may be read before being initialized and show how this can improve the precision of a null-pointer analysis.

Keywords: Java, semantics, class initialization, static analysis, control flow, verification

We present a non-null annotations inferencer for the Java bytecode language. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on several benchmarks. The results show a substantial improvement in the precision and, despite being a whole-program analysis, production applications can be analyzed within minutes.

Keywords: Java, NonNull, annotation, inference, static analysis

This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. We prove the analysis correct with respect to a semantics of a minimalistic OO language and complete with respect to the non-null type system proposed by Fähndrich and Leino, in the sense that for every typable program the analysis is able to prove the absence of null dereferences without any hand-written annotations. Experiments with a prototype implementation of the analysis show that the inference is feasible for large programs.

Keywords: Java, NonNull, annotation, inference, static analysis