Static Debugging Of C Programs: Detection Of Pointer Errors In Recursive Data Structures
Ronan Gaugne, 35 (France). Inst. de Recherche en Informatique et Systemes Aleatoires (IRISA) Rennes-1 Univ., 35 - Rennes (France). Inst. de Recherche en Informatique et Systemes Aleatoires (IRISA) Centre National de la Recherche Scientifique (CNRS), 35 (France). Inst . de Recherche en Informatique et Systemes Aleatoires (IRISA) Institut National des Sciences Appliquees de Rennes (INSA), 35 - Rennes (France). Inst. de Recherche en= Informatique et Systemes Aleatoires (IRISA) Institut National de Recherche en Informatique et en Automatique (INRIA) · 1997
: The incorrect use of pointers is one of the most common source of bugs in imperative languages. In this context, any kind of static code checking capable of detecting potential bugs at compile time is welcome. This paper presents a static debugging technique for the detection of incorrect accesses to memory (dereferences of invalid pointers). The analysed language is a subset of C. The tool is based on a static analyser extended with assertions inserted in the body of the program. Assertions are of two kinds: ffl static assertions automatically verified by the analyser, ffl dynamic assertions treated as assumptions by the analyser. The technique deals with dynamically allocated data structures and it is accurate enough to handle circular structures. Key-words: static debugging, static analysis, program verification, dangling pointers, assertion based debugging, Hoare logic (R'esum'e : tsvp) * [email protected] CENTRE NATIONAL DE LA RECHERCHE SCIENTIFIQUE Centre National de la R...