A Scalable Nonuniform Pointer Analysis for Embedded Programs

Abstract. In this paper we present a scalable pointer analysis for embedded applications that is able to distinguish between instances of recursively defined data structures and elements of arrays. The main contribution consists of an efficient yet precise algorithm that can handle multithreaded programs. We first perform an inexpensive flow-sensitive analysis of each function in the program that generates semantic equations describing the effect of the function on the memory graph. These equations bear numerical constraints that describe nonuniform points-to relationships. We then iteratively solve these equations in order to obabstract storage graph that describes the shape of data structures at every point of the program for all possible thread interleavings. We bring experimental evidence that this approach is tractable and precise for real-size embedded applications.

• Type: Conference
• Year: 2004
• Where: SAS
• Authors: Arnaud Venet
• Keywords: Data Structures, Embedded Applications, Equations, Formal Methods, SAS 2004