Jump to : Note | Abstract | Contact | BibTex reference | EndNote reference |


Pascal Sotin, Bertrand Jeannet. Precise Interprocedural Analysis in the Presence of Pointers to the Stack. In European Symposium on Programming, ESOP'11, LNCS, Volume 6602, Pages 459-479, Sarrebrück, 2011.

Note on this paper

accepted to the conference


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


Bertrand Jeannet http://pop-art.inrialpes.fr/people/bjeannet/

BibTex Reference

   Author = {Sotin, Pascal and Jeannet, Bertrand},
   Title = {Precise Interprocedural Analysis in the Presence of Pointers to the Stack},
   BookTitle = {European Symposium on Programming, ESOP'11},
   Volume = {6602},
   Pages = {459--479},
   Series = {LNCS},
   Address = {Sarrebrück},
   Year = {2011}

EndNote Reference [help]

Get EndNote Reference (.ref)