This web page is a patched version of the table of contents of the official CompCert documentation,
as given on the CompCert Web site.
The unmodified parts of this table appear in gray.
Table of contents
General-purpose libraries, data structures and algorithms
Pass | Source & target | Compiler code | Correctness proof |
---|---|---|---|
Pulling side-effects out of expressions; fixing an evaluation order |
CompCert C to Clight | SimplExpr | SimplExprspec SimplExprproof |
Pulling non-adressable scalar local variables out of memory | Clight to Clight | SimplLocals | SimplLocalsproof |
Simplification of control structures; explication of type-dependent computations |
Clight to Csharpminor | Cshmgen | Cshmgenproof |
Stack allocation of local variables whose address is taken; simplification of switch statements |
Csharpminor to Cminor | Cminorgen | Cminorgenproof |
Recognition of operators and addressing modes |
Cminor to CminorSel | Selection SelectOp SelectLong SelectDiv SplitLong |
Selectionproof SelectOpproof SelectLongproof SelectDivproof SplitLongproof |
Construction of the CFG, 3-address code generation |
CminorSel to RTL | RTLgen | RTLgenspec RTLgenproof |
Recognition of tail calls | RTL to RTL | Tailcall | Tailcallproof |
Function inlining | RTL to RTL | Inlining | Inliningspec Inliningproof |
Postorder renumbering of the CFG | RTL to RTL | Renumber | Renumberproof |
Constant propagation | RTL to RTL | Constprop ConstpropOp |
Constpropproof ConstproppOproof |
Common subexpression elimination | RTL to RTL | CSE CombineOp |
CSEproof CombineOpproof |
Redundancy elimination | RTL to RTL | Deadcode | Deadcodeproof |
Removal of unused static globals | RTL to RTL | Unusedglob | Unusedglobproof |
Register allocation (validation a posteriori) | RTL to LTL | Allocation | Allocproof |
Branch tunneling | LTL to LTL | Tunneling | Tunnelingproof |
Linearization of the CFG | LTL to Linear | Linearize | Linearizeproof |
Removal of unreferenced labels | Linear to Linear | CleanupLabels | CleanupLabelsproof |
Synthesis of debugging information | Linear to Linear | Debugvar | Debugvarproof |
Laying out the activation records | Linear to Mach | Stacking Bounds Stacklayout |
Stackingproof Separation |
Reconstruction of basic-blocks at Mach level | Mach to Machblock | Machblockgen | ForwardSimulationBlock Machblockgenproof |
Emission of purely sequential assembly code | Machblock to Asmblock | Asmblockgen | Asmblockgenproof0 Asmblockgenproof1 Asmblockgenproof |
Bundling (and basic-block scheduling) | Asmblock to Asmvliw | PostpassScheduling using Asmblockdeps and the abstractbb library |
PostpassSchedulingproof |
Flattening bundles (only a bureaucratic operation) | Asmvliw to Asm | Asmgen | Asmgenproof |