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.