diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 15:21:12 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-02-09 15:21:12 +0000 |
commit | 44cfa794dabe701959624c5cf2f0760c5827ccc0 (patch) | |
tree | dbaff031fb3c243d5bab534e00dba6c465ead3ee | |
parent | d933a48a352b6de8128c795b6725da318b37c562 (diff) |
MAJ fichier ppal
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@3 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r-- | doc/backend.html (renamed from doc/compcert.html) | 126 |
1 files changed, 63 insertions, 63 deletions
diff --git a/doc/compcert.html b/doc/backend.html index c778632..e33896c 100644 --- a/doc/compcert.html +++ b/doc/backend.html @@ -61,60 +61,60 @@ License</A> version 2.</P> <H3>Libraries, algorithms, data structures</H3> <UL> -<LI> <A HREF="Coqlib.html">Coqlib</A>: addendum to the Coq standard library. +<LI> <A HREF="lib.Coqlib.html">Coqlib</A>: addendum to the Coq standard library. (Coq source file with proofs: <A HREF="Coqlib.v"><code>Coqlib.v</code></a>.) -<LI> <A HREF="Maps.html">Maps</A>: finite maps. +<LI> <A HREF="lib.Maps.html">Maps</A>: finite maps. (Coq source file with proofs: <A HREF="Maps.v"><code>Maps.v</code></a>.) -<LI> <A HREF="Sets.html">Sets</A>: finite sets. -<LI> <A HREF="union_find.html">Union-find</A>: representation of +<LI> <A HREF="lib.Sets.html">Sets</A>: finite sets. +<LI> <A HREF="lib.union_find.html">Union-find</A>: representation of equivalence classes. (Coq source file with proofs: <A HREF="union_find.v"><code>union_find.v</code></a>.) -<LI> <A HREF="Inclusion.html">Inclusion</A>: tactics to prove list inclusions. -<LI> <A HREF="AST.html">AST</A>: identifiers, whole programs and other +<LI> <A HREF="lib.Inclusion.html">Inclusion</A>: tactics to prove list inclusions. +<LI> <A HREF="backend.AST.html">AST</A>: identifiers, whole programs and other common elements of abstract syntaxes. (Coq source file with proofs: <A HREF="AST.v"><code>AST.v</code></a>.) -<LI> <A HREF="Integers.html">Integers</A>: machine integers. +<LI> <A HREF="lib.Integers.html">Integers</A>: machine integers. (Coq source file with proofs: <A HREF="Integers.v"><code>Integers.v</code></a>.) -<LI> <A HREF="Floats.html">Floats</A>: machine floating-point numbers. -<LI> <A HREF="Mem.html">Mem</A>: the memory model. -<LI> <A HREF="Globalenvs.html">Globalenvs</A>: global execution environments. -<LI> <A HREF="Op.html">Op</A>: operators, addressing modes and their +<LI> <A HREF="lib.Floats.html">Floats</A>: machine floating-point numbers. +<LI> <A HREF="backend.Mem.html">Mem</A>: the memory model. +<LI> <A HREF="backend.Globalenvs.html">Globalenvs</A>: global execution environments. +<LI> <A HREF="backend.Op.html">Op</A>: operators, addressing modes and their semantics. -<LI> <A HREF="Ordered.html">Ordered</A>: construction of +<LI> <A HREF="lib.Ordered.html">Ordered</A>: construction of ordered types. -<LI> <A HREF="Lattice.html">Lattice</A>: construction of +<LI> <A HREF="lib.Lattice.html">Lattice</A>: construction of semi-lattices. -<LI> <A HREF="Kildall.html">Kildall</A>: resolution of dataflow +<LI> <A HREF="backend.Kildall.html">Kildall</A>: resolution of dataflow inequations by fixpoint iteration. </UL> <H3>Source, intermediate and target languages: syntax and semantics</H3> <UL> -<LI> <A HREF="Csharpminor.html">Csharpminor</A>: low-level structured language. -<LI> <A HREF="Cminor.html">Cminor</A>: low-level structured +<LI> <A HREF="backend.Csharpminor.html">Csharpminor</A>: low-level structured language. +<LI> <A HREF="backend.Cminor.html">Cminor</A>: low-level structured language, with explicit stack allocation of certain local variables. -<LI> <A HREF="RTL.html">RTL</A>: register transfer language (3-address +<LI> <A HREF="backend.RTL.html">RTL</A>: register transfer language (3-address code, control-flow graph, infinitely many pseudo-registers). <BR> -See also: <A HREF="Registers.html">Registers</A> (representation of +See also: <A HREF="backend.Registers.html">Registers</A> (representation of pseudo-registers). -<LI> <A HREF="LTL.html">LTL</A>: location transfer language (3-address +<LI> <A HREF="backend.LTL.html">LTL</A>: location transfer language (3-address code, control-flow graph, finitely many physical registers, infinitely many stack slots). <BR> -See also: <A HREF="Locations.html">Locations</A> (representation of +See also: <A HREF="backend.Locations.html">Locations</A> (representation of locations). -<LI> <A HREF="Linear.html">Linear</A>: like LTL, but the CFG is +<LI> <A HREF="backend.Linear.html">Linear</A>: like LTL, but the CFG is replaced by a linear list of instructions with explicit branches and labels. -<LI> <A HREF="Mach.html">Mach</A>: like Linear, with a more concrete +<LI> <A HREF="backend.Mach.html">Mach</A>: like Linear, with a more concrete view of the activation record. <BR> See also: an alternate semantics for the same -syntax is given in <A HREF="Machabstr.html">Machabstr</A>. <BR> -<LI> <A HREF="PPC.html">PPC</A>: abstract syntax for PowerPC assembly +syntax is given in <A HREF="backend.Machabstr.html">Machabstr</A>. <BR> +<LI> <A HREF="backend.PPC.html">PPC</A>: abstract syntax for PowerPC assembly code. </UL> @@ -131,87 +131,87 @@ code. <TR valign="top"> <TD>Recognition of operators and addressing modes</TD> <TD>Csharpminor to Cminor</TD> - <TD><A HREF="Cmconstr.html">Cmconstr</A></TD> - <TD><A HREF="Cmconstrproof.html">Cmconstrproof</A></TD> + <TD><A HREF="backend.Cmconstr.html">Cmconstr</A></TD> + <TD><A HREF="backend.Cmconstrproof.html">Cmconstrproof</A></TD> </TR> <TR valign="top"> <TD>Stack allocation of local variables<br>whose address is taken</TD> <TD>Csharpminor to Cminor</TD> - <TD><A HREF="Cminorgen.html">Cminorgen</A></TD> - <TD><A HREF="Cminorgenproof.html">Cminorgenproof</A></TD> + <TD><A HREF="backend.Cminorgen.html">Cminorgen</A></TD> + <TD><A HREF="backend.Cminorgenproof.html">Cminorgenproof</A></TD> </TR> <TR valign="top"> <TD>Construction of the CFG, <br>3-address code generation</TD> <TD>Cminor to RTL</TD> - <TD><A HREF="RTLgen.html">RTLgen</A></TD> - <TD><A HREF="RTLgenproof1.html">RTLgenproof1</A><BR> - <A HREF="RTLgenproof.html">RTLgenproof</A></TD> + <TD><A HREF="backend.RTLgen.html">RTLgen</A></TD> + <TD><A HREF="backend.RTLgenproof1.html">RTLgenproof1</A><BR> + <A HREF="backend.RTLgenproof.html">RTLgenproof</A></TD> </TR> <TR valign="top"> <TD>Constant propagation</TD> <TD>RTL to RTL</TD> - <TD><A HREF="Constprop.html">Constprop</A></TD> - <TD><A HREF="Constpropproof.html">Constpropproof</A></TD> + <TD><A HREF="backend.Constprop.html">Constprop</A></TD> + <TD><A HREF="backend.Constpropproof.html">Constpropproof</A></TD> </TR> <TR valign="top"> <TD>Common subexpression elimination</TD> <TD>RTL to RTL</TD> - <TD><A HREF="CSE.html">CSE</A></TD> - <TD><A HREF="CSEproof.html">CSEproof</A></TD> + <TD><A HREF="backend.CSE.html">CSE</A></TD> + <TD><A HREF="backend.CSEproof.html">CSEproof</A></TD> </TR> <TR valign="top"> <TD>Register allocation by coloring<br>of an interference graph</TD> <TD>RTL to LTL</TD> - <TD><A HREF="Conventions.html">Conventions</A><BR> - <A HREF="InterfGraph.html">InterfGraph</A><BR> - <A HREF="Coloring.html">Coloring</A><BR> - <A HREF="Parallelmove.html">Parallelmove</A><BR> - <A HREF="Allocation.html">Allocation</A></TD> + <TD><A HREF="backend.Conventions.html">Conventions</A><BR> + <A HREF="backend.InterfGraph.html">InterfGraph</A><BR> + <A HREF="backend.Coloring.html">Coloring</A><BR> + <A HREF="backend.Parallelmove.html">Parallelmove</A><BR> + <A HREF="backend.Allocation.html">Allocation</A></TD> <TD><BR> <BR> - <A HREF="Coloringproof.html">Coloringproof</A><BR> - <A HREF="Allocproof_aux.html">Allocproof_aux</A><BR> - <A HREF="Allocproof.html">Allocproof</A></TD> + <A HREF="backend.Coloringproof.html">Coloringproof</A><BR> + <A HREF="backend.Allocproof_aux.html">Allocproof_aux</A><BR> + <A HREF="backend.Allocproof.html">Allocproof</A></TD> </TR> <TR valign="top"> <TD>Branch tunneling</TD> <TD>LTL to LTL</TD> - <TD><A HREF="Tunneling.html">Tunneling</A></TD> - <TD><A HREF="Tunnelingproof.html">Tunnelingproof</A></TD> + <TD><A HREF="backend.Tunneling.html">Tunneling</A></TD> + <TD><A HREF="backend.Tunnelingproof.html">Tunnelingproof</A></TD> </TR> <TR valign="top"> <TD>Linearization of the CFG</TD> <TD>LTL to Linear</TD> - <TD><A HREF="Linearize.html">Linearize</A></TD> - <TD><A HREF="Linearizeproof.html">Linearizeproof</A></TD> + <TD><A HREF="backend.Linearize.html">Linearize</A></TD> + <TD><A HREF="backend.Linearizeproof.html">Linearizeproof</A></TD> </TR> <TR valign="top"> <TD>Laying out the activation records</TD> <TD>Linear to Mach</TD> - <TD><A HREF="Stacking.html">Stacking</A></TD> - <TD><A HREF="Stackingroof.html">Stackingproof</A></TD> + <TD><A HREF="backend.Stacking.html">Stacking</A></TD> + <TD><A HREF="backend.Stackingroof.html">Stackingproof</A></TD> </TR> <TR valign="top"> <TD>Storing the activation records in memory</TD> <TD>Mach to Mach</TD> <TD>(none) - <TD><A HREF="Machabstr2mach.html">Machabstr2mach</A></TD> + <TD><A HREF="backend.Machabstr2mach.html">Machabstr2mach</A></TD> <TR valign="top"> <TD>Emission of PowerPC assembly</TD> <TD>Mach to PPC</TD> - <TD><A HREF="PPCgen.html">PPCgen</A></TD> - <TD><A HREF="PPCgenproof1.html">PPCgenproof1</A><BR> - <A HREF="PPCgenproof.html">PPCgenproof</A></TD> + <TD><A HREF="backend.PPCgen.html">PPCgen</A></TD> + <TD><A HREF="backend.PPCgenproof1.html">PPCgenproof1</A><BR> + <A HREF="backend.PPCgenproof.html">PPCgenproof</A></TD> </TR> </TABLE> @@ -220,25 +220,25 @@ code. Trivial type systems are used to statically capture well-formedness conditions on the intermediate languages. <UL> -<LI> <A HREF="RTLtyping.html">RTLtyping</A>: typing for RTL + type +<LI> <A HREF="backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type reconstruction. -<LI> <A HREF="LTLtyping.html">LTLtyping</A>: typing for LTL. -<LI> <A HREF="Lineartyping.html">Lineartyping</A>: typing for Linear. -<LI> <A HREF="Machtyping.html">Machtyping</A>: typing for Mach. +<LI> <A HREF="backend.LTLtyping.html">LTLtyping</A>: typing for LTL. +<LI> <A HREF="backend.Lineartyping.html">Lineartyping</A>: typing for Linear. +<LI> <A HREF="backend.Machtyping.html">Machtyping</A>: typing for Mach. </UL> Proofs that compiler passes are type-preserving: <UL> -<LI> <A HREF="Alloctyping_aux.html">Alloctyping_aux</A> and - <A HREF="Alloctyping.html">Alloctyping</A> (register allocation). -<LI> <A HREF="Tunnelingtyping.html">Tunnelingtyping</A> (branch tunneling). -<LI> <A HREF="Lineartyping.html">Lineartyping</A> (branch tunneling). -<LI> <A HREF="Stackingtyping.html">Stackingtyping</A> (layout of activation records). +<LI> <A HREF="backend.Alloctyping_aux.html">Alloctyping_aux</A> and + <A HREF="backend.Alloctyping.html">Alloctyping</A> (register allocation). +<LI> <A HREF="backend.Tunnelingtyping.html">Tunnelingtyping</A> (branch tunneling). +<LI> <A HREF="backend.Lineartyping.html">Lineartyping</A> (branch tunneling). +<LI> <A HREF="backend.Stackingtyping.html">Stackingtyping</A> (layout of activation records). </UL> <H3>All together</H3> <UL> -<LI> <A HREF="Main.html">Main</A>: composing the passes together; the +<LI> <A HREF="backend.Main.html">Main</A>: composing the passes together; the final semantic preservation theorems. </UL> |