[Cherry picking] 01ade46b340267d8782c413f6bd5a3cff13ef0a6

starting a new index-verimag.html on BTL doc
author: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> 2021-12-06 21:34:46 +0100
committer: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> 2021-12-06 21:34:46 +0100
commit: 820e1ecbca864982ebc7b8efc453d057e374a4f7 (patch)
tree: 260d27374b776f025c62a44f0ba08dcf4ea7a32f /doc
parent: 47cdb65b2290df66690d34d6a09745fb364ef392 (diff)
download: compcert-kvx-820e1ecbca864982ebc7b8efc453d057e374a4f7.tar.gz
compcert-kvx-820e1ecbca864982ebc7b8efc453d057e374a4f7.zip
1 files changed, 395 insertions, 0 deletions
diff --git a/doc/index-verimag.html b/doc/index-verimag.html
new file mode 100644
index 00000000..242fa1cd
--- /dev/null
+++ b/doc/index-verimag.html
@@ -0,0 +1,395 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+<HTML>
+<HEAD>
+<TITLE>The CompCert verified compiler</TITLE>
+<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
+
+<style type="text/css">
+body {
+  color: black; background: white;
+  margin-left: 5%; margin-right: 5%;
+}
+h2 { margin-left: -5%;}
+h3 { margin-left: -3%; }
+h1,h2,h3 { font-family: sans-serif; }
+hr { margin-left: -5%; margin-right:-5%; }
+a:visited {color : #416DFF; text-decoration : none; font-weight : bold}
+a:link {color : #416DFF; text-decoration : none; font-weight : bold}
+a:hover {color : Red; text-decoration : underline; }
+a:active {color : Red; text-decoration : underline; }
+</style>
+
+</HEAD>
+<BODY>
+  <font color=gray>
+<H1 align="center">The CompCert verified compiler</H1>
+<H2 align="center">Commented Coq development</H2>
+<H3 align="center">Version 3.9, 2021-05-10</H3>
+</font>
+<H3 align="center">VERIMAG fork version 2021-29-10</H3>
+
+<H2>The CompCert Verimag's fork</H2>
+<p>This web page is a patched version of the table of contents of the official CompCert sources documentation, as given on <A HREF="http://compcert.org/doc/index.html">the CompCert Web site</A>.
+  The unmodified parts of this table appear in <font color=gray>gray</font>.
+  <br>
+  <br>
+  A high-level view of this CompCert backend is provided by the following documents:
+  <ul>
+    <li>The Six's thesis:
+      <div><a href=https://hal.archives-ouvertes.fr/tel-03326923>Optimized and formally-verified compilation for a VLIW processor.</a></div></li>
+    <li>Our OOPSLA'20 paper (of Six, Boulm&eacute; and Monniaux):
+      <div><a href=https://hal.archives-ouvertes.fr/hal-02185883>Certified and Efficient Instruction Scheduling. Application to Interlocked VLIW Processors.</a></div></li>
+    <li>A preprint (of Six, Gourdin, Boulm&eacute; and Monniaux):
+        <div><a href=https://hal.archives-ouvertes.fr/hal-03200774>Verified Superblock Scheduling with Related Optimizations.</a></div></li>
+    <li>A short paper published at AFADL'21 (of Gourdin):
+          <div><a href=https://www.lirmm.fr/afadl2021/papers/afadl2021_paper_9.pdf>Formally verified postpass scheduling with peephole optimization for AArch64.</a></div></li>
+    <!--TODO add the CPP'22 publication-->
+    <li>The <tt>README.md</tt> of our <a href=https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/compcert-kvx>GitLab public repository</a>.</li>
+  </ul>
+</p>
+
+<H2>Introduction</H2>
+
+<font color="gray">
+<P>CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly
+code from CompCert C, a large subset of the C programming language.
+The particularity of this compiler is that it is written mostly within
+the specification language of the Coq proof assistant, and its
+correctness --- the fact that the generated assembly code is
+semantically equivalent to its source program --- was entirely proved
+within the Coq proof assistant.</P>
+
+<P>High-level descriptions of the CompCert compiler and its proof of 
+correctness can be found in the following papers (in increasing order of technical details):</P>
+<UL>
+<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-CACM.pdf">Formal verification of a realistic compiler</A>.  Communications of the ACM 52(7), July 2009.
+<LI>Xavier Leroy, <A HREF="https://xavierleroy.org/publi/compcert-backend.pdf">A formally verified compiler back-end</A>. 
+Journal of Automated Reasoning 43(4):363-446, 2009.
+</UL>
+
+<P>This Web site gives a commented listing of the underlying Coq
+specifications and proofs.  Proof scripts are folded by default, but
+can be viewed by clicking on "Proof".  Some modules (written in <I>italics</I> below) differ between the five target architectures.  The
+PowerPC versions of these modules are shown below; the AArch64, ARM,
+x86 and RISC-V versions can be found in the source distribution.
+</P>
+
+<P> This development is a work in progress; some parts have
+substantially changed since the overview papers above were
+written.</P>
+
+<P>The complete sources for CompCert can be downloaded from
+<A HREF="https://github.com/AbsInt/CompCert/">the Git repository</A>
+or <A HREF="https://compcert.org/">the CompCert Web site</A>.
+</P>
+
+<P>This document and the CompCert sources are copyright Institut
+National de Recherche en Informatique et en Automatique (INRIA) and
+AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the
+following <A HREF="LICENSE.txt">license</A>.
+</P>
+</font>
+
+<H2>Table of contents</H2>
+
+<font color="gray">
+<H3>General-purpose libraries, data structures and algorithms</H3>
+
+<UL>
+<LI> <A HREF="html/compcert.lib.Coqlib.html">Coqlib</A>: addendum to the Coq standard library.
+<LI> <A HREF="html/compcert.lib.Maps.html">Maps</A>: finite maps.
+<LI> <A HREF="html/compcert.lib.Integers.html">Integers</A>: machine integers.
+<LI> <A HREF="html/compcert.lib.Floats.html">Floats</A>: machine floating-point numbers.
+<LI> <A HREF="html/compcert.lib.Iteration.html">Iteration</A>: various forms of "while" loops.
+<LI> <A HREF="html/compcert.lib.Ordered.html">Ordered</A>: construction of
+ordered types.
+<LI> <A HREF="html/compcert.lib.Lattice.html">Lattice</A>: construction of
+semi-lattices.
+<LI> <A HREF="html/compcert.backend.Kildall.html">Kildall</A>: resolution of dataflow
+inequations by fixpoint iteration.
+<LI> <A HREF="html/compcert.lib.UnionFind.html">UnionFind</A>: a persistent union-find data structure.
+<LI> <A HREF="html/compcert.lib.Postorder.html">Postorder</A>: postorder numbering of a directed graph.
+</UL></font>
+
+<H4><A HREF=https://github.com/boulme/ImpureDemo>The Impure library</A> (of Boulm&eacute;)</H4>
+<UL>
+<LI><A HREF="html/compcert.lib.Impure.ImpConfig.html">ImpConfig</A>: declares the <tt>Impure</tt> monad and defines its extraction.</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpCore.html">ImpCore</A>: defines notations for the <tt>Impure</tt> monad and a <tt>wlp_simplify</tt> tactic (to reason about <tt>Impure</tt> functions in a Hoare-logic style).</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpLoops.html">ImpLoops</A>, <A HREF="html/compcert.lib.Impure.ImpIO.html">ImpIO</A>, <A HREF="html/compcert.lib.Impure.ImpHCons.html">ImpHCons</A>: declare <tt>Impure</tt> oracles and define operators from these oracles. <A HREF="html/compcert.lib.Impure.ImpExtern.html">ImpExtern</A> exports all these impure operators.</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpMonads.html">ImpMonads</A>: axioms of "impure computations" and some Coq models of these axioms.</LI>
+<LI><A HREF="html/compcert.lib.Impure.ImpPrelude.html">ImpPrelude</A>: declares the data types exchanged with <tt>Impure</tt> oracles.</LI>
+</UL>
+
+<H4>The <tt>abstractbb</tt> library, introduced for Aarch64 and KVX cores</H4>
+This library introduces a block intermediate representation used for postpass scheduling verification. It might be extended to others backends.
+<UL>
+<LI> <A HREF="html/compcert.scheduling.abstractbb.AbstractBasicBlocksDef.html">AbstractBasicBlocksDef</A>: an IR for verifying some semantic properties on basic-blocks.
+<LI> <A HREF="html/compcert.scheduling.abstractbb.Parallelizability.html">Parallelizability</A>: verifying that sequential and parallel semantics are equivalent for a given abstract basic-block.
+<LI> <A HREF="html/compcert.scheduling.abstractbb.ImpSimuTest.html">ImpSimuTest</A>: verifying that a given abstract basic-block is simulated by another one for sequential semantics. This module refines <A HREF="html/compcert.scheduling.abstractbb.SeqSimuTheory.html">SeqSimuTheory</A> with hash-consing and uses <A HREF=https://github.com/boulme/ImpureDemo>the Impure library</A> to reason on physical equality and handling of imperative code in Coq.
+</UL>
+<H3>Definitions and theorems used in many parts of the development</H3>
+
+<UL>
+<LI> <A HREF="html/compcert.common.Errors.html">Errors</A>: the Error monad.
+<LI> <A HREF="html/compcert.common.AST.html">AST</A>: identifiers, whole programs and other
+common elements of abstract syntaxes.
+<LI> <A HREF="html/compcert.common.Linking.html">Linking</A>: generic framework to define syntactic linking over the CompCert languages.
+<LI> <A HREF="html/compcert.common.Values.html">Values</A>: run-time values.
+<LI> <A HREF="html/compcert.common.Events.html">Events</A>: observable events and traces.
+<LI> <A HREF="html/compcert.common.Memory.html">Memory</A>: memory model. <BR>
+See also: <A HREF="html/compcert.common.Memdata.html">Memdata</A> (in-memory representation of data).
+<LI> <A HREF="html/compcert.common.Globalenvs.html">Globalenvs</A>: global execution environments.
+<LI> <A HREF="html/compcert.common.Smallstep.html">Smallstep</A>: tools for small-step semantics.
+<LI> <A HREF="html/compcert.common.Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs.
+<LI> <A HREF="html/compcert.common.Determinism.html">Determinism</A>: determinism properties of small-step semantics.
+<LI> <A HREF="html/compcert.kvx.Op.html"><I>Op</I></A>: operators, addressing modes and their
+semantics.
+<LI> <A HREF="html/compcert.common.Builtins.html">Builtins</A>: semantics of built-in functions. <BR>
+See also: <A HREF="html/compcert.common.Builtins0.html">Builtins0</A> (target-independent part), <A HREF="html/compcert.kvx.Builtins1.html"><I>Builtins1</I></A> (target-dependent part).
+<LI> <A HREF="html/compcert.common.Unityping.html">Unityping</A>: a solver for atomic unification constraints.
+</UL>
+
+<H3>Source, intermediate and target languages: syntax and semantics</H3>
+
+<UL>
+<LI> The CompCert C source language:
+<A HREF="html/compcert.cfrontend.Csyntax.html">syntax</A> and
+<A HREF="html/compcert.cfrontend.Csem.html">semantics</A> and
+<A HREF="html/compcert.cfrontend.Cstrategy.html">determinized semantics</A> and
+<A HREF="html/compcert.cfrontend.Ctyping.html">type system</A>.<BR>
+See also: <A HREF="html/compcert.cfrontend.Ctypes.html">type expressions</A> and
+<A HREF="html/compcert.cfrontend.Cop.html">operators (syntax and semantics)</A>.<BR>
+See also: <A HREF="html/compcert.cfrontend.Cexec.html">reference interpreter</A>.
+<LI> <A HREF="html/compcert.cfrontend.Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects.
+<LI> <A HREF="html/compcert.cfrontend.Csharpminor.html">Csharpminor</A>: low-level
+ structured language.
+<LI> <A HREF="html/compcert.backend.Cminor.html">Cminor</A>: low-level structured
+language, with explicit stack allocation of certain local variables.
+<LI> <A HREF="html/compcert.backend.CminorSel.html">CminorSel</A>: like Cminor,
+with machine-specific operators and addressing modes.
+<LI> <A HREF="html/compcert.backend.RTL.html">RTL</A>: register transfer language (3-address
+code, control-flow graph, infinitely many pseudo-registers). <BR>
+See also: <A HREF="html/compcert.backend.Registers.html">Registers</A> (representation of
+pseudo-registers).
+<LI> <A HREF="html/compcert.backend.LTL.html">LTL</A>: location transfer language (3-address
+code, control-flow graph of basic blocks, finitely many physical registers, infinitely
+many stack slots). <BR>
+See also: <A HREF="html/compcert.backend.Locations.html">Locations</A> (representation of
+locations) and <A HREF="html/compcert.kvx.Machregs.html"><I>Machregs</I></A> (description of processor registers).
+<LI> <A HREF="html/compcert.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="html/compcert.backend.Mach.html">Mach</A>: like Linear, with a more concrete
+view of the activation record.  
+<LI> <A HREF="html/compcert.kvx.Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly
+code.
+</UL>
+
+<H3>Compiler passes</H3>
+
+<TABLE cellpadding="5%">
+<TR valign="top">
+  <TH align=left>Pass</TH>
+  <TH align=left>Source &amp; target</TH>
+  <TH align=left>Compiler&nbsp;code</TH>
+  <TH align=left>Correctness&nbsp;proof</TH>
+</TR>
+
+<TR valign="top">
+  <TD>Pulling side-effects out of expressions;<br>
+      fixing an evaluation order</TD>
+  <TD>CompCert C to Clight</TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplExpr.html">SimplExpr</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplExprspec.html">SimplExprspec</A><br>
+      <A HREF="html/compcert.cfrontend.SimplExprproof.html">SimplExprproof</A></TD>
+</TR>
+<TR valign="top">
+  <TD>Pulling non-adressable scalar local variables out of memory</TD>
+  <TD>Clight to Clight</TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplLocals.html">SimplLocals</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.SimplLocalsproof.html">SimplLocalsproof</A></TD>
+</TR>
+<TR valign="top">
+  <TD>Simplification of control structures; <br>
+      explication of type-dependent computations</TD>
+  <TD>Clight to Csharpminor</TD>
+  <TD><A HREF="html/compcert.cfrontend.Cshmgen.html">Cshmgen</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cshmgenproof.html">Cshmgenproof</A></TD>
+</TR>
+<TR valign="top">
+  <TD>Stack allocation of local variables<br>
+      whose address is taken;<br>
+      simplification of switch statements</TD>
+  <TD>Csharpminor to Cminor</TD>
+  <TD><A HREF="html/compcert.cfrontend.Cminorgen.html">Cminorgen</A></TD>
+  <TD><A HREF="html/compcert.cfrontend.Cminorgenproof.html">Cminorgenproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Recognition of operators<br>and addressing modes;<br>
+      if-conversion</TD>
+  <TD>Cminor to CminorSel</TD>
+  <TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br>
+      <A HREF="html/compcert.kvx.SelectOp.html"><I>SelectOp</I></A><br>
+      <A HREF="html/compcert.kvx.SelectLong.html"><I>SelectLong</I></A><br>
+      <A HREF="html/compcert.backend.SelectDiv.html">SelectDiv</A><br>
+      <A HREF="html/compcert.backend.SplitLong.html">SplitLong</A></TD>
+  <TD><A HREF="html/compcert.backend.Selectionproof.html">Selectionproof</A><br>
+      <A HREF="html/compcert.kvx.SelectOpproof.html"><I>SelectOpproof</I></A><br>
+      <A HREF="html/compcert.kvx.SelectLongproof.html"><I>SelectLongproof</I></A><br>
+      <A HREF="html/compcert.backend.SelectDivproof.html">SelectDivproof</A><br>
+      <A HREF="html/compcert.backend.SplitLongproof.html">SplitLongproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Construction of the CFG, <br>3-address code generation</TD>
+  <TD>CminorSel to RTL</TD>
+  <TD><A HREF="html/compcert.backend.RTLgen.html">RTLgen</A></TD>
+  <TD><A HREF="html/compcert.backend.RTLgenspec.html">RTLgenspec</A><BR>
+      <A HREF="html/compcert.backend.RTLgenproof.html">RTLgenproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Recognition of tail calls</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Tailcall.html">Tailcall</A></TD>
+  <TD><A HREF="html/compcert.backend.Tailcallproof.html">Tailcallproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Function inlining</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Inlining.html">Inlining</A></TD>
+  <TD><A HREF="html/compcert.backend.Inliningspec.html">Inliningspec</A><BR>
+      <A HREF="html/compcert.backend.Inliningproof.html">Inliningproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Postorder renumbering of the CFG</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Renumber.html">Renumber</A></TD>
+  <TD><A HREF="html/compcert.backend.Renumberproof.html">Renumberproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Constant propagation</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br>
+      <A HREF="html/compcert.kvx.ConstpropOp.html"><I>ConstpropOp</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br>
+      <A HREF="html/compcert.kvx.ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Common subexpression elimination</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR>
+      <A HREF="html/compcert.kvx.CombineOp.html"><I>CombineOp</I></A></TD>
+  <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR>
+      <A HREF="html/compcert.kvx.CombineOpproof.html"><I>CombineOpproof</I></A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Redundancy elimination</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Deadcode.html">Deadcode</A></TD>
+  <TD><A HREF="html/compcert.backend.Deadcodeproof.html">Deadcodeproof</A></TD>
+</TR>
+<TR valign="top">
+  <TD>Removal of unused static globals</TD>
+  <TD>RTL to RTL</TD>
+  <TD><A HREF="html/compcert.backend.Unusedglob.html">Unusedglob</A></TD>
+  <TD><A HREF="html/compcert.backend.Unusedglobproof.html">Unusedglobproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Register allocation (validation a posteriori)</TD>
+  <TD>RTL to LTL</TD>
+  <TD><A HREF="html/compcert.backend.Allocation.html">Allocation</A></TD>
+  <TD><A HREF="html/compcert.backend.Allocproof.html">Allocproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Branch tunneling</TD>
+  <TD>LTL to LTL</TD>
+  <TD><A HREF="html/compcert.backend.Tunneling.html">Tunneling</A></TD>
+  <TD><A HREF="html/compcert.backend.Tunnelingproof.html">Tunnelingproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Linearization of the CFG</TD>
+  <TD>LTL to Linear</TD>
+  <TD><A HREF="html/compcert.backend.Linearize.html">Linearize</A></TD>
+  <TD><A HREF="html/compcert.backend.Linearizeproof.html">Linearizeproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Removal of unreferenced labels</TD>
+  <TD>Linear to Linear</TD>
+  <TD><A HREF="html/compcert.backend.CleanupLabels.html">CleanupLabels</A></TD>
+  <TD><A HREF="html/compcert.backend.CleanupLabelsproof.html">CleanupLabelsproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Synthesis of debugging information</TD>
+  <TD>Linear to Linear</TD>
+  <TD><A HREF="html/compcert.backend.Debugvar.html">Debugvar</A></TD>
+  <TD><A HREF="html/compcert.backend.Debugvarproof.html">Debugvarproof</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Laying out the activation records</TD>
+  <TD>Linear to Mach</TD>
+  <TD><A HREF="html/compcert.backend.Stacking.html">Stacking</A><BR>
+      <A HREF="html/compcert.backend.Bounds.html">Bounds</A><BR>
+      <A HREF="html/compcert.kvx.Stacklayout.html"><I>Stacklayout</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Stackingproof.html">Stackingproof</A><br>
+      <A HREF="html/compcert.common.Separation.html">Separation</A></TD>
+</TR>
+
+<TR valign="top">
+  <TD>Emission of assembly code</TD>
+  <TD>Mach to Asm</TD>
+  <TD><A HREF="html/compcert.kvx.Asmgen.html"><I>Asmgen</I></A></TD>
+  <TD><A HREF="html/compcert.backend.Asmgenproof0.html"><I>Asmgenproof0</I></A><BR>
+      <A HREF="html/compcert.kvx.Asmgenproof1.html"><I>Asmgenproof1</I></A><BR>
+      <A HREF="html/compcert.kvx.Asmgenproof.html"><I>Asmgenproof</I></A></TD>
+</TR>
+</TABLE>
+
+<H3>All together (there are many more passes than on vanilla CompCert: their order is specified in Compiler)</H3>
+
+<UL>
+<LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together;
+whole-compiler semantic preservation theorems.
+<font color=gray>
+<LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems.
+</UL>
+
+<H3>Static analyses</H3>
+
+The following static analyses are performed over the RTL intermediate
+representation to support optimizations such as constant propagation,
+CSE, and dead code elimination.
+<UL>
+<LI> <A HREF="html/compcert.backend.Liveness.html">Liveness</A>: liveness analysis</A>.
+<LI> <A HREF="html/compcert.backend.ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR>
+See also: <A HREF="html/compcert.backend.ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR>
+See also: <A HREF="html/compcert.kvx.ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis.
+<LI> <A HREF="html/compcert.backend.Deadcode.html">Deadcode</A>: neededness analysis</A> <BR>
+See also: <A HREF="html/compcert.backend.NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR>
+See also: <A HREF="html/compcert.kvx.NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis.
+</UL>
+
+<H3>Type systems</H3>
+
+The <A HREF="html/compcert.cfrontend.Ctyping.html">type system of CompCert C</A> is fully formalized.  For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions.
+<UL>
+<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">Ctyping</A>: typing for CompCert C + type-checking functions.
+<LI> <A HREF="html/compcert.backend.RTLtyping.html">RTLtyping</A>: typing for RTL + type
+reconstruction.
+<LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear.
+</UL>
+</font>
+
+</BODY>
+</HTML>
author	Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>	2021-12-06 21:34:46 +0100
committer	Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>	2021-12-06 21:34:46 +0100
commit	820e1ecbca864982ebc7b8efc453d057e374a4f7 (patch)
tree	260d27374b776f025c62a44f0ba08dcf4ea7a32f /doc
parent	47cdb65b2290df66690d34d6a09745fb364ef392 (diff)
download	compcert-kvx-820e1ecbca864982ebc7b8efc453d057e374a4f7.tar.gz compcert-kvx-820e1ecbca864982ebc7b8efc453d057e374a4f7.zip