Precise Interprocedural Analysis in the Presence of Pointers to the Stack

Abstract : In a language with procedures 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 :
Pré-publication, Document de travail
2011
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00547888
Contributeur : Pascal Sotin <>
Soumis le : lundi 3 janvier 2011 - 11:02:18
Dernière modification le : jeudi 11 janvier 2018 - 06:22:03
Document(s) archivé(s) le : lundi 4 avril 2011 - 02:30:18

Fichiers

SotinJeannet2011-ExactPointerA...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00547888, version 1

Collections

Citation

Pascal Sotin, Bertrand Jeannet. Precise Interprocedural Analysis in the Presence of Pointers to the Stack. 2011. 〈inria-00547888〉

Partager

Métriques

Consultations de la notice

175

Téléchargements de fichiers

172