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 obtain
an abstract 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.
