HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

An Inference Algorithm for the Static Verification of Pointer Manipulation

Pascal Fradet 1 Ronan Gaugne 1 Daniel Le Métayer 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : The incorrect use of pointers is one of the most common source of bugs. As a consequence, any kind of static code checking capable of detecting potential bugs at compile time is welcome. This paper presents a static analysis for the detection of incorrect accesses to memory (dereferences of invalid pointers). A pointer may be invalid because it has not been initialised or because it refers to a memory location which has been deallocated. The analyser is derived from an axiomatisation of alias and connectivity properties which is shown to be sound with respect to the natural semantics of the language. It deals with dynamically allocated data structures and it is accurate enough to handle circular structures.
Document type :
Complete list of metadata

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 1:46:11 PM
Last modification on : Friday, February 4, 2022 - 3:23:14 AM
Long-term archiving on: : Sunday, April 4, 2010 - 11:58:27 PM


  • HAL Id : inria-00073795, version 1


Pascal Fradet, Ronan Gaugne, Daniel Le Métayer. An Inference Algorithm for the Static Verification of Pointer Manipulation. [Research Report] RR-2895, INRIA. 1996. ⟨inria-00073795⟩



Record views


Files downloads