Precise Null-Pointer Analysis

In Java, C or C++, attempts to dereference the nil value result in anexception or a segmentation fault. Hence it is importantto identify those program points where this undesired behaviourmight occur or provethe other program points (and possibly the entire program) safe.To that purpose,null-pointer analysis of computer programs checks or infers non-nil annotationsfor variables and object fields. With few notable exceptions, null-pointeranalyses currently use run-time checks or are incorrect or only verifymanually provided annotations. In this paper, we use abstract interpretationto build and prove correct a first, flow and context-sensitivestatic null-pointer analysis for Javabytecode (and hence Java) which infers non-nil annotations. It isbased on Boolean formulas, implemented with binary decisiondiagrams. For better precision, it identifies instance or static fieldsthat remain emph{always} non- il after being initialised.Our experiments show this analysis faster and more precise than the correctnull-pointer analysis by Hubert, Jensen and Pichardie.Moreover, our analysis deals with exceptions, which isnot the case of most others; its formulation istheoretically clean and its implementation strong and scalable.We subsequently improve that analysis by using local reasoning about fieldsthat are not always non-nil,but are actually non- il when they are accessed.This is a frequent situation, since programmers typically checks fornon-nullness of a field before the access. This second,improved analysis is highly precise.We conclude with an example of use of our analyses to infernull-pointer annotations which are more precise than those that otherinference tools can achieve.