Skip to Main content Skip to Navigation
Conference papers

Semantic Foundations and Inference of Non-null Annotations

Laurent Hubert 1 Thomas Jensen 1 David Pichardie 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in ob ject- oriented programs. The analysis is formulated for a minimalistic OO language and is expressed as a constraint-based abstract interpretation of the program which for each field of a class infers whether the field is definitely non-null or possibly null after ob ject initialization. The analysis is proved correct with respect to an operational semantics of the mini- malistic OO language. This correctness proof has been machine checked using the Coq proof assistant. We also prove the analysis complete with respect to the non-null type system proposed by F ̈ahndrich 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : David Pichardie Connect in order to contact the contributor
Submitted on : Monday, October 20, 2008 - 4:40:28 PM
Last modification on : Friday, February 4, 2022 - 3:25:14 AM
Long-term archiving on: : Monday, June 7, 2010 - 7:00:23 PM


Files produced by the author(s)


  • HAL Id : inria-00332356, version 1


Laurent Hubert, Thomas Jensen, David Pichardie. Semantic Foundations and Inference of Non-null Annotations. 10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), 2008, Oslo, Norway. ⟨inria-00332356⟩



Record views


Files downloads