The general shape of activation records is as follows,
from bottom (lowest offsets) to top:
24 reserved bytes. The first 4 bytes hold the back pointer to the
activation record of the caller. We use the 4 bytes at offset 12
to store the return address. (These are reserved by the PowerPC
application binary interface.) The remaining bytes are unused.
Space for outgoing arguments to function calls.
Local stack slots of integer type.
Saved values of integer callee-save registers used by the function.
One word of padding, if necessary to align the following data
on a 8-byte boundary.
Local stack slots of float type.
Saved values of float callee-save registers used by the function.
Space for the stack-allocated data declared in Cminor.
To facilitate some of the proofs, the Cminor stack-allocated data
starts at offset 0; the preceding areas in the activation record
therefore have negative offsets. This part (with negative offsets)
is called the ``frame'', by opposition with the ``Cminor stack data''
which is the part with positive offsets.
The frame_env compilation environment records the positions of
the boundaries between areas in the frame part.