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 metadatas

Cited literature [15 references]  Display  Hide  Download

https://hal.inria.fr/inria-00332356
Contributor : David Pichardie <>
Submitted on : Monday, October 20, 2008 - 4:40:28 PM
Last modification on : Friday, November 16, 2018 - 1:24:23 AM
Long-term archiving on : Monday, June 7, 2010 - 7:00:23 PM

File

fmoods08.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00332356, version 1

Citation

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⟩

Share

Metrics

Record views

185

Files downloads

181