# Changeset 1769 for Deliverables/D1.2/CompilerProofOutline

Ignore:
Timestamp:
Feb 27, 2012, 2:52:53 PM (8 years ago)
Message:

..

File:
1 edited

### Legend:

Unmodified
 r1768 \end{center} \subsection{Graph translations} \subsection{The RTLabs to RTL translation} \label{subsect.rtlabs.rtl.translation} The forward simulation proof for all steps that do not involve function calls is trivial because $\sigma$ does not alter the memory or the pseudo-registers. We outline here the invocation of functions and return from a function. calls are lengthy, but unsurprising. They consists in simulating a front-end operation on front-end pseudo-registers and the front-end memory with sequences of back-end operations on the back-end pseudo-registers and back-end memory. The properties of $\sigma$ presented before that relate values and memories needs to be heavily exploited. The simulation of invocation of functions and returns from functions is less obvious. We sketch here what happens on the source code and on its translation. \begin{displaymath}