Precise Interprocedural Analysis in the Presence of Pointers to the Stack

Pascal Sotin 1, * Bertrand Jeannet 1, *
* Auteur correspondant
1 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : In a language with procedures calls and pointers as parameters, an instruction can modify memory locations anywhere in the call-stack. The presence of such side effects breaks most generic interprocedural analysis methods, which assume that only the top of the stack may be modified. We present a method that addresses this issue, based on the definition of an equivalent local semantics in which writing through pointers has a local effect on the stack. Our second contribution in this context is an adequate representation of summary functions that models the effect of a procedure, not only on the values of its scalar and pointer variables, but also on the values contained in pointed memory locations. Our implementation in the interprocedural analyser PInterproc results in a verification tool that infers relational properties on the value of Boolean, numerical and pointer variables.
Type de document :
Communication dans un congrès
European Symposium on Programming, ESOP'11, Apr 2011, Sarrebrueck, Germany. 6602, pp.459-479, 2011, 〈10.1007/978-3-642-19718-5_24〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00786327
Contributeur : Bertrand Jeannet <>
Soumis le : vendredi 8 février 2013 - 13:29:01
Dernière modification le : mercredi 11 avril 2018 - 01:55:00

Lien texte intégral

Identifiants

Collections

Citation

Pascal Sotin, Bertrand Jeannet. Precise Interprocedural Analysis in the Presence of Pointers to the Stack. European Symposium on Programming, ESOP'11, Apr 2011, Sarrebrueck, Germany. 6602, pp.459-479, 2011, 〈10.1007/978-3-642-19718-5_24〉. 〈hal-00786327〉

Partager

Métriques

Consultations de la notice

108