Precise Interprocedural Analysis in the Presence of Pointers to the Stack

Pascal Sotin (1, 2) , Bertrand Jeannet (1, 2)

1 LIG - Laboratoire d'Informatique de Grenoble
2 POP ART - Programming languages, Operating Systems, Parallelism, and Aspects for Real-Time

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.

Mots clés: Interprocedural Analysis; Pointers on the Stack; Alias Analysis; Logico-Numerical Properties; Abstract Interpretation

Domaines: Langage de programmation [cs.PL]

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