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.
Type de document :
Communication dans un congrès
10th International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'08), 2008, Oslo, Norway. 2008
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00332356
Contributeur : David Pichardie <>
Soumis le : lundi 20 octobre 2008 - 16:40:28
Dernière modification le : mercredi 16 mai 2018 - 11:23:03
Document(s) archivé(s) le : lundi 7 juin 2010 - 19:00:23

Fichier

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

Identifiants

  • HAL Id : inria-00332356, version 1

Collections

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. 2008. 〈inria-00332356〉

Partager

Métriques

Consultations de la notice

157

Téléchargements de fichiers

98