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 : jeudi 11 janvier 2018 - 01:48:47

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

90