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

..

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1768 r1769  
    316316\end{center}
    317317
     318\subsection{Graph translations}
     319
    318320\subsection{The RTLabs to RTL translation}
    319321\label{subsect.rtlabs.rtl.translation}
     
    489491
    490492The forward simulation proof for all steps that do not involve function
    491 calls is trivial because $\sigma$ does not alter the memory or the
    492 pseudo-registers. We outline here the invocation of functions and return
    493 from a function.
     493calls are lengthy, but unsurprising. They consists in simulating a
     494front-end operation on front-end pseudo-registers and the front-end memory
     495with sequences of back-end operations on the back-end pseudo-registers
     496and back-end memory. The properties of $\sigma$ presented before that relate
     497values and memories needs to be heavily exploited.
     498
     499The simulation of invocation of functions and returns from functions is
     500less obvious. We sketch here what happens on the source code and on its
     501translation.
    494502
    495503\begin{displaymath}
Note: See TracChangeset for help on using the changeset viewer.