From 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 1 Jun 2018 10:40:04 +0200 Subject: Use the standalone coq2html tool to generate the HTML documentation coq2html is now a standalone project (https://github.com/xavierleroy/coq2html) packaged as coq-coq2html in OPAM-Coq. --- doc/index.html | 230 ++++++++++++++++++++++++++++----------------------------- 1 file changed, 115 insertions(+), 115 deletions(-) (limited to 'doc/index.html') diff --git a/doc/index.html b/doc/index.html index 2ac5f698..60c4e9a0 100644 --- a/doc/index.html +++ b/doc/index.html @@ -69,73 +69,73 @@ following license.

General-purpose libraries, data structures and algorithms

Definitions and theorems used in many parts of the development

Source, intermediate and target languages: syntax and semantics

@@ -153,170 +153,170 @@ code. Pulling side-effects out of expressions;
fixing an evaluation order CompCert C to Clight - SimplExpr - SimplExprspec
- SimplExprproof + SimplExpr + SimplExprspec
+ SimplExprproof Pulling non-adressable scalar local variables out of memory Clight to Clight - SimplLocals - SimplLocalsproof + SimplLocals + SimplLocalsproof Simplification of control structures;
explication of type-dependent computations Clight to Csharpminor - Cshmgen - Cshmgenproof + Cshmgen + Cshmgenproof Stack allocation of local variables
whose address is taken;
simplification of switch statements Csharpminor to Cminor - Cminorgen - Cminorgenproof + Cminorgen + Cminorgenproof Recognition of operators
and addressing modes Cminor to CminorSel - Selection
- SelectOp
- SelectLong
- SelectDiv
- SplitLong - Selectionproof
- SelectOpproof
- SelectLongproof
- SelectDivproof
- SplitLongproof + Selection
+ SelectOp
+ SelectLong
+ SelectDiv
+ SplitLong + Selectionproof
+ SelectOpproof
+ SelectLongproof
+ SelectDivproof
+ SplitLongproof Construction of the CFG,
3-address code generation CminorSel to RTL - RTLgen - RTLgenspec
- RTLgenproof + RTLgen + RTLgenspec
+ RTLgenproof Recognition of tail calls RTL to RTL - Tailcall - Tailcallproof + Tailcall + Tailcallproof Function inlining RTL to RTL - Inlining - Inliningspec
- Inliningproof + Inlining + Inliningspec
+ Inliningproof Postorder renumbering of the CFG RTL to RTL - Renumber - Renumberproof + Renumber + Renumberproof Constant propagation RTL to RTL - Constprop
- ConstpropOp - Constpropproof
- ConstproppOproof + Constprop
+ ConstpropOp + Constpropproof
+ ConstproppOproof Common subexpression elimination RTL to RTL - CSE
- CombineOp - CSEproof
- CombineOpproof + CSE
+ CombineOp + CSEproof
+ CombineOpproof Redundancy elimination RTL to RTL - Deadcode - Deadcodeproof + Deadcode + Deadcodeproof Removal of unused static globals RTL to RTL - Unusedglob - Unusedglobproof + Unusedglob + Unusedglobproof Register allocation (validation a posteriori) RTL to LTL - Allocation - Allocproof + Allocation + Allocproof Branch tunneling LTL to LTL - Tunneling - Tunnelingproof + Tunneling + Tunnelingproof Linearization of the CFG LTL to Linear - Linearize - Linearizeproof + Linearize + Linearizeproof Removal of unreferenced labels Linear to Linear - CleanupLabels - CleanupLabelsproof + CleanupLabels + CleanupLabelsproof Synthesis of debugging information Linear to Linear - Debugvar - Debugvarproof + Debugvar + Debugvarproof Laying out the activation records Linear to Mach - Stacking
- Bounds
- Stacklayout - Stackingproof
- Separation + Stacking
+ Bounds
+ Stacklayout + Stackingproof
+ Separation Emission of assembly code Mach to Asm - Asmgen - Asmgenproof0
- Asmgenproof1
- Asmgenproof + Asmgen + Asmgenproof0
+ Asmgenproof1
+ Asmgenproof

All together

Static analyses

@@ -325,23 +325,23 @@ The following static analyses are performed over the RTL intermediate representation to support optimizations such as constant propagation, CSE, and dead code elimination.

Type systems

-The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
-- cgit