Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [29 references]  Display  Hide  Download

https://hal.inria.fr/inria-00547888
Contributor : Pascal Sotin Connect in order to contact the contributor
Submitted on : Monday, January 3, 2011 - 11:02:18 AM
Last modification on : Sunday, June 26, 2022 - 4:56:36 AM
Long-term archiving on: : Monday, April 4, 2011 - 2:30:18 AM

Files

SotinJeannet2011-ExactPointerA...
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00547888, version 1

Collections

UGA | CNRS | INRIA | INRIA2 | ANR

Citation

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

Share

Metrics

Record views

141

Files downloads

342