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 object-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 object initialization. The analysis is proved correct with respect to an operational semantics of the minimalistic 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ä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.
Type de document :
Rapport
[Research Report] 2008
Liste complète des métadonnées

https://hal.inria.fr/inria-00266171
Contributeur : Laurent Hubert <>
Soumis le : vendredi 21 mars 2008 - 17:51:01
Dernière modification le : vendredi 6 février 2015 - 12:24:55
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 11:31:24

Fichier

report.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00266171, version 1

Collections

Citation

Laurent Hubert, Thomas Jensen, David Pichardie. Semantic foundations and inference of non-null annotations. [Research Report] 2008. <inria-00266171v1>

Partager

Métriques

Consultations de
la notice

1

Téléchargements du document

7