Reference Shape Graph

We represent the memory configurations with the tuple
where: **L** is the set of memory locations; **P** is the
set of pointer variables (pvars) used in the program; **S** is the
set of selectors declared in the data structures; **PS** is the set
of references from pvars to memory locations, of the type ,
with
and ; and **LS** is the set of links
between memory locations, of the form
where references by selector . We will use L(m),
P(m), S(m), PS(m), and LS(m) to refer to each one of these sets for a
particular memory configuration, .

Therefore, we can assume that the RSRSG of a program sentence is
an approximation of all possible memory configurations, after the
execution of this sentence. However, let us first describe the
*RSGs* now that we know how a memory configuration is defined.

To obtain the RSG which approximates a memory configuration, , an abstraction function is used, . This function maps memory locations into nodes and references to memory locations into references to nodes at the same time. In other words, , translates the memory domain into the graph domain. This, function comprises three functions: takes care of mapping memory locations into nodes; maps references from pvars to memory locations into references from pvars to nodes, and maps links between locations into links between nodes.

It is easy to see that: iif and iif which means that translating references to locations into references to nodes is trivial after mapping locations into nodes. This translates almost all the complexity involved in function to function which actually maps locations into nodes.