Attempts to dereference null result in an exception or a segmentation fault. Hence it is important to know those program points where this might occur and prove the others (or the entire program) safe. Nullness analysis of computer programs checks or infers non-null annotations for variables and object fields. Most nullness analyses currently use run-time checks or are simply syntactical (as in Eclipse and Idea) or incorrect or only verify manual annotations. We use abstract interpretation to build and prove correct a static nullness analysis for Java bytecode which infers non-null annotations. It is based on Boolean formulas, implemented with binary decision diagrams. Our experiments show it faster and more precise than the correct nullness analysis by Hubert, Jensen and Pichardie. We deal with static fields and exceptions, which is not the case of most other analyses. The result is theoretically clean and the implementation strong and scalable.
