diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 10:40:04 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-01 10:40:04 +0200 |
commit | 24951d885fbadb8f2fa96ea44a6d3b2a397eab00 (patch) | |
tree | c048b0745667c4a00298c302948ddf7afdc5deba /doc | |
parent | ffc03f2dcb24438d2900743848005c9a058e649c (diff) | |
download | compcert-24951d885fbadb8f2fa96ea44a6d3b2a397eab00.tar.gz compcert-24951d885fbadb8f2fa96ea44a6d3b2a397eab00.zip |
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.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/coq2html.css | 97 | ||||
-rw-r--r-- | doc/coq2html.js | 24 | ||||
-rw-r--r-- | doc/coq2html.mll | 454 | ||||
-rw-r--r-- | doc/coqdoc.css | 62 | ||||
-rw-r--r-- | doc/index.html | 230 |
5 files changed, 115 insertions, 752 deletions
diff --git a/doc/coq2html.css b/doc/coq2html.css deleted file mode 100644 index c5627bfb..00000000 --- a/doc/coq2html.css +++ /dev/null @@ -1,97 +0,0 @@ -/* Classes: - h1.title the title of the page - div.coq encloses all generated body - div.doc contents of (** *) comments - div.footer footer - div.togglescript "Proof." line - div.proofscript contents of proof script - span.docright contents of (**r *) comments - span.bracket contents of [ ] within comments - span.comment contents of (* *) comments - span.kwd Coq keyword - span.tactic Coq tactic - span.id any other identifier -*/ - -body { - color: black; - background: white; -} - -h1.title { - font-size: 2em; - text-align: center -} - -h1 { - font-size: 1.5em; -} -h2 { - font-size: 1.17em; -} -h3 { - font-size: 1em; -} - -h1, h2, h3 { - font-family: sans-serif; - margin-left: -5%; -} - -div.coq { - margin-left: 15%; - margin-right: 5%; - font-family: monospace; -} - -div.doc { - margin-left: -5%; - margin-top: 0.2em; - margin-bottom: 0.5em; - font-family: serif; -} - -div.toggleproof { - font-size: 0.8em; - text-decoration: underline; -} - -div.toggleproof:hover { - cursor: pointer; -} - -div.proofscript { - font-size: 0.8em; -} - -div.footer { - margin-top: 1em; - margin-bottom: 1em; - font-size: 0.8em; - font-style: italic; -} - -span.docright { - position: absolute; - left: 60%; - width: 40%; - font-family: serif; -} - -span.bracket { - font-family: monospace; - color: #008000; -} - -span.kwd { - color: #cf1d1d; -} - -span.comment { - color: #008000; -} - -a:visited {color : #416DFF; text-decoration : none; } -a:link {color : #416DFF; text-decoration : none; } -a:hover {text-decoration : none; } -a:active {text-decoration : none; } diff --git a/doc/coq2html.js b/doc/coq2html.js deleted file mode 100644 index a840b004..00000000 --- a/doc/coq2html.js +++ /dev/null @@ -1,24 +0,0 @@ -function toggleDisplay(id) -{ - var elt = document.getElementById(id); - if (elt.style.display == 'none') { - elt.style.display = 'block'; - } else { - elt.style.display = 'none'; - } -} - -function hideAll(cls) -{ - var testClass = new RegExp("(^|s)" + cls + "(s|$)"); - var tag = tag || "*"; - var elements = document.getElementsByTagName("div"); - var current; - var length = elements.length; - for(var i=0; i<length; i++){ - current = elements[i]; - if(testClass.test(current.className)) { - current.style.display = 'none'; - } - } -} diff --git a/doc/coq2html.mll b/doc/coq2html.mll deleted file mode 100644 index cdc844dc..00000000 --- a/doc/coq2html.mll +++ /dev/null @@ -1,454 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -{ -open Printf - -(** Cross-referencing *) - -let current_module = ref "" - -type xref = - | Def of string * string (* path, type *) - | Ref of string * string * string (* unit, path, type *) - -let xref_table : (string * int, xref) Hashtbl.t = Hashtbl.create 273 -let xref_modules : (string, unit) Hashtbl.t = Hashtbl.create 29 - -let path sp id = - match sp, id with - | "<>", "<>" -> "" - | "<>", _ -> id - | _ , "<>" -> sp - | _ , _ -> sp ^ "." ^ id - -let add_module m = - (*eprintf "add_module %s\n" m;*) - Hashtbl.add xref_modules m () - -let add_reference curmod pos dp sp id ty = - (*eprintf "add_reference %s %d %s %s %s %s\n" curmod pos dp sp id ty;*) - if not (Hashtbl.mem xref_table (curmod, pos)) - then Hashtbl.add xref_table (curmod, pos) (Ref(dp, path sp id, ty)) - -let add_definition curmod pos sp id ty = - if not (Hashtbl.mem xref_table (curmod, pos)) - then Hashtbl.add xref_table (curmod, pos) (Def(path sp id, ty)) - -type link = Link of string | Anchor of string | Nolink - -let coqlib_url = "http://coq.inria.fr/library/" - -let re_coqlib = Str.regexp "Coq\\." -let re_sane_path = Str.regexp "[A-Za-z0-9_.]+$" -let re_shortname = Str.regexp "^.*\\." - -let shortname m = Str.replace_first re_shortname "" m - -let crossref m pos = - (*eprintf "crossref %s %d\n" m pos;*) - try match Hashtbl.find xref_table (m, pos) with - | Def(p, _) -> - Anchor p - | Ref(m', p, _) -> - let url = - if Hashtbl.mem xref_modules m' then - shortname m' ^ ".html" - else if Str.string_match re_coqlib m' 0 then - coqlib_url ^ m' ^ ".html" - else - raise Not_found in - if p = "" then - Link url - else if Str.string_match re_sane_path p 0 then - Link(url ^ "#" ^ p) - else - Nolink - with Not_found -> - Nolink - -(** Keywords, etc *) - -module StringSet = Set.Make(String) - -let mkset l = List.fold_right StringSet.add l StringSet.empty - -let coq_keywords = mkset [ - "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; - "dest"; "fun"; "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; - "where"; "struct"; "wf"; "measure"; - "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; - "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; - "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; - "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; - "Hypotheses"; "Resolve"; "Unfold"; "Immediate"; "Extern"; - "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; - "Local"; "Ltac"; "Module"; "Module Type"; "Declare Module"; - "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; - "Qed"; "Record"; "Recursive"; "Remark"; "Require"; - "Save"; "Scheme"; "Induction"; "for"; "Sort"; "Section"; "Show"; - "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; "Set"; - "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; - "Notation"; "Reserved"; "Tactic"; "Delimit"; "Bind"; "Open"; - "Scope"; "Boxed"; "Unboxed"; "Inline"; "Implicit Arguments"; "Add"; - "Strict"; "Typeclasses"; "Instance"; "Global Instance"; "Class"; - "Instantiation"; "subgoal"; "Program"; "Example"; "Obligation"; - "Obligations"; "Solve"; "using"; "Next"; "Instance"; "Equations"; - "Equations_nocomp" -] - -let coq_tactics = mkset [ - "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; - "injection"; "elimtype"; "progress"; "setoid_rewrite"; "destruct"; - "destruction"; "destruct_call"; "dependent"; "elim"; - "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; - "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; - "set"; "assert"; "do"; "repeat"; "cut"; "assumption"; "exact"; - "split"; "subst"; "try"; "discriminate"; "simpl"; "unfold"; "red"; - "compute"; "at"; "in"; "by"; "reflexivity"; "symmetry"; - "transitivity"; "replace"; "setoid_replace"; "inversion"; - "inversion_clear"; "pattern"; "intuition"; "congruence"; "fail"; - "fresh"; "trivial"; "exact"; "tauto"; "firstorder"; "ring"; - "clapply"; "program_simpl"; "program_simplify"; "eapply"; "auto"; - "eauto" -] - -(** HTML generation *) - -let oc = ref stdout - -let character = function - | '<' -> output_string !oc "<" - | '>' -> output_string !oc ">" - | '&' -> output_string !oc "&" - | c -> output_char !oc c - -let section_level = function - | "*" -> 1 - | "**" -> 2 - | _ -> 3 - -let start_section sect = - fprintf !oc "<h%d>" (section_level sect) -let end_section sect = - fprintf !oc "</h%d>\n" (section_level sect) - -let start_doc_right () = - fprintf !oc "<span class=\"docright\">(* " -let end_doc_right () = - fprintf !oc " *)</span>" - -let enum_depth = ref 0 - -let set_enum_depth d = - if !enum_depth < d then begin - fprintf !oc "<ul>\n"; - fprintf !oc "<li>\n"; - incr enum_depth; - end - else if !enum_depth > d then begin - fprintf !oc "</li>\n"; - fprintf !oc "</ul>\n"; - decr enum_depth; - end - else if !enum_depth > 0 then begin - fprintf !oc "</li>\n"; - fprintf !oc "<li>\n" - end - -let start_doc () = - fprintf !oc "<div class=\"doc\">" -let end_doc () = - set_enum_depth 0; - fprintf !oc "</div>\n" - -let ident pos id = - if StringSet.mem id coq_keywords then - fprintf !oc "<span class=\"kwd\">%s</span>" id - else if StringSet.mem id coq_tactics then - fprintf !oc "<span class=\"tactic\">%s</span>" id - else match crossref !current_module pos with - | Nolink -> - fprintf !oc "<span class=\"id\">%s</span>" id - | Link p -> - fprintf !oc "<span class=\"id\"><a href=\"%s\">%s</a></span>" p id - | Anchor p -> - fprintf !oc "<span class=\"id\"><a name=\"%s\">%s</a></span>" p id - -let space s = - for _ = 1 to String.length s do fprintf !oc " " done - -let newline () = - fprintf !oc "<br/>\n" - -let dashes = function - | "-" -> set_enum_depth 1 - | "--" -> set_enum_depth 2 - | "---" -> set_enum_depth 3 - | "----" -> set_enum_depth 4 - | _ -> fprintf !oc "<hr/>\n" - -let start_verbatim () = - fprintf !oc "<pre>\n" - -let end_verbatim () = - fprintf !oc "</pre>\n" - -let start_comment () = - fprintf !oc "<span class=\"comment\">(*" - -let end_comment () = - fprintf !oc "*)</span>" - -let start_bracket () = - fprintf !oc "<span class=\"bracket\">" - -let end_bracket () = - fprintf !oc "</span>" - -let in_proof = ref false -let proof_counter = ref 0 - -let start_proof kwd = - in_proof := true; - incr proof_counter; - fprintf !oc - "<div class=\"toggleproof\" onclick=\"toggleDisplay('proof%d')\">%s</div>\n" - !proof_counter kwd; - fprintf !oc "<div class=\"proofscript\" id=\"proof%d\">\n" !proof_counter - -let end_proof kwd = - fprintf !oc "%s</div>\n" kwd; - in_proof := false - -let start_html_page modname = - fprintf !oc -{|<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> - -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<title>Module %s</title> -<meta name="description" content="Documentation of Coq module %s" /> -<link href="coq2html.css" rel="stylesheet" type="text/css" /> -<script type="text/javascript" src="coq2html.js"> </script> -</head> - -<body onload="hideAll('proofscript')"> -<h1 class="title">Module %s</h1> -<div class="coq"> -|} modname modname modname - -let end_html_page () = - fprintf !oc -{|</div> -<div class="footer"><hr/>Generated by coq2html</div> -</body> -</html> -|} - -} - -let space = [' ' '\t'] -let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* -let path = ident ("." ident)* -let start_proof = ("Proof" space* ".") | ("Proof" space+ "with") | ("Next" space+ "Obligation.") -let end_proof = "Qed." | "Defined." | "Save." | "Admitted." | "Abort." - -let xref = ['A'-'Z' 'a'-'z' '0'-'9' '_' '.']+ | "<>" -let integer = ['0'-'9']+ - -rule coq_bol = parse - | space* (start_proof as sp) - { start_proof sp; - skip_newline lexbuf } - | space* "(** " ("*"+ as sect) - { start_section sect; - doc lexbuf; - end_section sect; - skip_newline lexbuf } - | space* "(** " - { start_doc(); - doc lexbuf; - end_doc(); - skip_newline lexbuf } - | space* "(*" - { comment lexbuf; - skip_newline lexbuf } - | eof - { () } - | space* as s - { space s; - coq lexbuf } - -and skip_newline = parse - | space* "\n" - { coq_bol lexbuf } - | "" - { coq lexbuf } - -and coq = parse - | end_proof as ep - { end_proof ep; - skip_newline lexbuf } - | "(**r " - { start_doc_right(); - doc lexbuf; - end_doc_right(); - coq lexbuf } - | "(*" - { if !in_proof then start_comment(); - comment lexbuf; - coq lexbuf } - | path as id - { ident (Lexing.lexeme_start lexbuf) id; coq lexbuf } - | "\n" - { newline(); coq_bol lexbuf } - | eof - { () } - | _ as c - { character c; coq lexbuf } - -and bracket = parse - | ']' - { () } - | '[' - { character '['; bracket lexbuf; character ']'; bracket lexbuf } - | path as id - { ident (Lexing.lexeme_start lexbuf) id; bracket lexbuf } - | eof - { () } - | _ as c - { character c; bracket lexbuf } - -and comment = parse - | "*)" - { if !in_proof then end_comment() } - | "(*" - { if !in_proof then start_comment(); - comment lexbuf; comment lexbuf } - | eof - { () } - | "\n" - { if !in_proof then newline(); - comment lexbuf } - | space* as s - { if !in_proof then space s; - comment lexbuf } - | eof - { () } - | _ as c - { if !in_proof then character c; - comment lexbuf } - -and doc_bol = parse - | "<<" space* "\n" - { start_verbatim(); - verbatim lexbuf; - end_verbatim(); - doc_bol lexbuf } - | "-"+ as d - { dashes d; doc lexbuf } - | "\n" - { set_enum_depth 0; doc_bol lexbuf } - | "" - { doc lexbuf } - -and doc = parse - | "*)" - { () } - | "\n" - { character '\n'; doc_bol lexbuf } - | "[" - { start_bracket(); bracket lexbuf; end_bracket(); doc lexbuf } - | "$" [^ '\n' '$']* "$" - { doc lexbuf } - | "#" ([^ '\n' '#']* as html) "#" - { output_string !oc html; doc lexbuf } - | eof - { () } - | _ as c - { character c; doc lexbuf } - -and verbatim = parse - | "\n>>" space* "\n" - { () } - | eof - { () } - | _ as c - { character c; verbatim lexbuf } - -and globfile = parse - | eof - { () } - | "F" (path as m) space* "\n" - { current_module := m; add_module m; - globfile lexbuf } - | "R" (integer as pos) ":" (integer) - space+ (xref as dp) - space+ (xref as sp) - space+ (xref as id) - space+ (ident as ty) - space* "\n" - { add_reference !current_module (int_of_string pos) dp sp id ty; - globfile lexbuf } - | (ident as ty) - space+ (integer as pos) ":" (integer) - space+ (xref as sp) - space+ (xref as id) - space* "\n" - { add_definition !current_module (int_of_string pos) sp id ty; - globfile lexbuf } - | [^ '\n']* "\n" - { globfile lexbuf } - -{ - -let output_name = ref "-" - -let process_file f = - if Filename.check_suffix f ".v" then begin - let pref_f = Filename.chop_suffix f ".v" in - let base_f = Filename.basename pref_f in - current_module := - "compcert." ^ Str.global_replace (Str.regexp "/") "." pref_f; - let ic = open_in f in - if !output_name = "-" then - oc := stdout - else - oc := open_out (Str.global_replace (Str.regexp "%") base_f !output_name); - start_html_page base_f; - coq_bol (Lexing.from_channel ic); - end_html_page(); - if !output_name <> "-" then (close_out !oc; oc := stdout); - close_in ic - end else - if Filename.check_suffix f ".glob" then begin - current_module := ""; - let ic = open_in f in - globfile (Lexing.from_channel ic); - close_in ic - end else begin - eprintf "Don't know what to do with file %s\n" f; - exit 2 - end - -let _ = - Arg.parse [ - "-o", Arg.String (fun s -> output_name := s), - " <output> Set output file ('%' replaced by module name)" - ] process_file - "Usage: coq2html [options] <file.glob> file.v\nOptions are:" -} diff --git a/doc/coqdoc.css b/doc/coqdoc.css deleted file mode 100644 index f2ae96da..00000000 --- a/doc/coqdoc.css +++ /dev/null @@ -1,62 +0,0 @@ -body { - color: black; - background: white; - margin-left: 15%; - margin-right: 5%; -} - -#main a.idref:visited {color : #416DFF; text-decoration : none; } -#main a.idref:link {color : #416DFF; text-decoration : none; } -#main a.idref:hover {text-decoration : none; } -#main a.idref:active {text-decoration : none; } - -#main a.modref:visited {color : #416DFF; text-decoration : none; } -#main a.modref:link {color : #416DFF; text-decoration : none; } -#main a.modref:hover {text-decoration : none; } -#main a.modref:active {text-decoration : none; } - -#main .keyword { color : #cf1d1d } - -#main .doc { - margin-left: -5%; -} - -#main span.docright { - position: absolute; - left: 60%; - width: 40% -} - -h1.libtitle { - font-size: 2em; - margin-left: -15%; - margin-right: -5%; - text-align: center -} - -h1 { - font-size: 1.5em; -} -h2 { - font-size: 1.17em; -} - -h1, h2 { - font-family: sans-serif; -} - -.doc code { - color: #008000; -} - -/* Pied de page */ - -hr { margin-left: -15%; margin-right:-5%; } - -#footer { font-size: 0.83em; - font-family: sans-serif; } - -#footer a:visited { color: blue; } -#footer a:link { text-decoration: none; - color: #888888; } - 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 <A HREF="LICENSE">license</A>. <H3>General-purpose libraries, data structures and algorithms</H3> <UL> -<LI> <A HREF="html/Coqlib.html">Coqlib</A>: addendum to the Coq standard library. -<LI> <A HREF="html/Maps.html">Maps</A>: finite maps. -<LI> <A HREF="html/Integers.html">Integers</A>: machine integers. -<LI> <A HREF="html/Floats.html">Floats</A>: machine floating-point numbers. -<LI> <A HREF="html/Iteration.html">Iteration</A>: various forms of "while" loops. -<LI> <A HREF="html/Ordered.html">Ordered</A>: construction of +<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/Lattice.html">Lattice</A>: construction of +<LI> <A HREF="html/compcert.lib.Lattice.html">Lattice</A>: construction of semi-lattices. -<LI> <A HREF="html/Kildall.html">Kildall</A>: resolution of dataflow +<LI> <A HREF="html/compcert.backend.Kildall.html">Kildall</A>: resolution of dataflow inequations by fixpoint iteration. -<LI> <A HREF="html/UnionFind.html">UnionFind</A>: a persistent union-find data structure. -<LI> <A HREF="html/Postorder.html">Postorder</A>: postorder numbering of a directed graph. +<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> <H3>Definitions and theorems used in many parts of the development</H3> <UL> -<LI> <A HREF="html/Errors.html">Errors</A>: the Error monad. -<LI> <A HREF="html/AST.html">AST</A>: identifiers, whole programs and other +<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/Linking.html">Linking</A>: generic framework to define syntactic linking over the CompCert languages. -<LI> <A HREF="html/Values.html">Values</A>: run-time values. -<LI> <A HREF="html/Events.html">Events</A>: observable events and traces. -<LI> <A HREF="html/Memory.html">Memory</A>: memory model. <BR> -See also: <A HREF="html/Memdata.html">Memdata</A> (in-memory representation of data). -<LI> <A HREF="html/Globalenvs.html">Globalenvs</A>: global execution environments. -<LI> <A HREF="html/Smallstep.html">Smallstep</A>: tools for small-step semantics. -<LI> <A HREF="html/Behaviors.html">Behaviors</A>: from small-step semantics to observable behaviors of programs. -<LI> <A HREF="html/Determinism.html">Determinism</A>: determinism properties of small-step semantics. -<LI> <A HREF="html/Op.html"><I>Op</I></A>: operators, addressing modes and their +<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.powerpc.Op.html"><I>Op</I></A>: operators, addressing modes and their semantics. -<LI> <A HREF="html/Unityping.html">Unityping</A>: a solver for atomic unification constraints. +<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/Csyntax.html">syntax</A> and -<A HREF="html/Csem.html">semantics</A> and -<A HREF="html/Cstrategy.html">determinized semantics</A> and -<A HREF="html/Ctyping.html">type system</A>.<BR> -See also: <A HREF="html/Ctypes.html">type expressions</A> and -<A HREF="html/Cop.html">operators (syntax and semantics)</A>.<BR> -See also: <A HREF="html/Cexec.html">reference interpreter</A>. -<LI> <A HREF="html/Clight.html">Clight</A>: a simpler version of CompCert C where expressions contain no side-effects. -<LI> <A HREF="html/Csharpminor.html">Csharpminor</A>: low-level +<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/Cminor.html">Cminor</A>: low-level structured +<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/CminorSel.html">CminorSel</A>: like Cminor, +<LI> <A HREF="html/compcert.backend.CminorSel.html">CminorSel</A>: like Cminor, with machine-specific operators and addressing modes. -<LI> <A HREF="html/RTL.html">RTL</A>: register transfer language (3-address +<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/Registers.html">Registers</A> (representation of +See also: <A HREF="html/compcert.backend.Registers.html">Registers</A> (representation of pseudo-registers). -<LI> <A HREF="html/LTL.html">LTL</A>: location transfer language (3-address +<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/Locations.html">Locations</A> (representation of -locations) and <A HREF="html/Machregs.html"><I>Machregs</I></A> (description of processor registers). -<LI> <A HREF="html/Linear.html">Linear</A>: like LTL, but the CFG is +See also: <A HREF="html/compcert.backend.Locations.html">Locations</A> (representation of +locations) and <A HREF="html/compcert.powerpc.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/Mach.html">Mach</A>: like Linear, with a more concrete +<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/Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly +<LI> <A HREF="html/compcert.powerpc.Asm.html"><I>Asm</I></A>: abstract syntax for PowerPC assembly code. </UL> @@ -153,170 +153,170 @@ code. <TD>Pulling side-effects out of expressions;<br> fixing an evaluation order</TD> <TD>CompCert C to Clight</TD> - <TD><A HREF="html/SimplExpr.html">SimplExpr</A></TD> - <TD><A HREF="html/SimplExprspec.html">SimplExprspec</A><br> - <A HREF="html/SimplExprproof.html">SimplExprproof</A></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/SimplLocals.html">SimplLocals</A></TD> - <TD><A HREF="html/SimplLocalsproof.html">SimplLocalsproof</A></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/Cshmgen.html">Cshmgen</A></TD> - <TD><A HREF="html/Cshmgenproof.html">Cshmgenproof</A></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/Cminorgen.html">Cminorgen</A></TD> - <TD><A HREF="html/Cminorgenproof.html">Cminorgenproof</A></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</TD> <TD>Cminor to CminorSel</TD> - <TD><A HREF="html/Selection.html">Selection</A><br> - <A HREF="html/SelectOp.html"><I>SelectOp</I></A><br> - <A HREF="html/SelectLong.html"><I>SelectLong</I></A><br> - <A HREF="html/SelectDiv.html">SelectDiv</A><br> - <A HREF="html/SplitLong.html">SplitLong</A></TD> - <TD><A HREF="html/Selectionproof.html">Selectionproof</A><br> - <A HREF="html/SelectOpproof.html"><I>SelectOpproof</I></A><br> - <A HREF="html/SelectLongproof.html"><I>SelectLongproof</I></A><br> - <A HREF="html/SelectDivproof.html">SelectDivproof</A><br> - <A HREF="html/SplitLongproof.html">SplitLongproof</A></TD> + <TD><A HREF="html/compcert.backend.Selection.html">Selection</A><br> + <A HREF="html/Selectcompcert.powerpc.Op.html"><I>SelectOp</I></A><br> + <A HREF="html/compcert.powerpc.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.powerpc.SelectOpproof.html"><I>SelectOpproof</I></A><br> + <A HREF="html/compcert.powerpc.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/RTLgen.html">RTLgen</A></TD> - <TD><A HREF="html/RTLgenspec.html">RTLgenspec</A><BR> - <A HREF="html/RTLgenproof.html">RTLgenproof</A></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/Tailcall.html">Tailcall</A></TD> - <TD><A HREF="html/Tailcallproof.html">Tailcallproof</A></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/Inlining.html">Inlining</A></TD> - <TD><A HREF="html/Inliningspec.html">Inliningspec</A><BR> - <A HREF="html/Inliningproof.html">Inliningproof</A></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/Renumber.html">Renumber</A></TD> - <TD><A HREF="html/Renumberproof.html">Renumberproof</A></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/Constprop.html">Constprop</A><br> - <A HREF="html/ConstpropOp.html"><I>ConstpropOp</I></A></TD> - <TD><A HREF="html/Constpropproof.html">Constpropproof</A><br> - <A HREF="html/ConstpropOpproof.html"><I>ConstproppOproof</I></A></TD> + <TD><A HREF="html/compcert.backend.Constprop.html">Constprop</A><br> + <A HREF="html/compcert.powerpc.Constpropcompcert.powerpc.Op.html"><I>ConstpropOp</I></A></TD> + <TD><A HREF="html/compcert.backend.Constpropproof.html">Constpropproof</A><br> + <A HREF="html/compcert.powerpc.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/CSE.html">CSE</A><BR> - <A HREF="html/CombineOp.html"><I>CombineOp</I></A></TD> - <TD><A HREF="html/CSEproof.html">CSEproof</A><BR> - <A HREF="html/CombineOpproof.html"><I>CombineOpproof</I></A></TD> + <TD><A HREF="html/compcert.backend.CSE.html">CSE</A><BR> + <A HREF="html/compcert.powerpc.Combinecompcert.powerpc.Op.html"><I>CombineOp</I></A></TD> + <TD><A HREF="html/compcert.backend.CSEproof.html">CSEproof</A><BR> + <A HREF="html/compcert.powerpc.CombineOpproof.html"><I>CombineOpproof</I></A></TD> </TR> <TR valign="top"> <TD>Redundancy elimination</TD> <TD>RTL to RTL</TD> - <TD><A HREF="html/Deadcode.html">Deadcode</A></TD> - <TD><A HREF="html/Deadcodeproof.html">Deadcodeproof</A></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/Unusedglob.html">Unusedglob</A></TD> - <TD><A HREF="html/Unusedglobproof.html">Unusedglobproof</A></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/Allocation.html">Allocation</A></TD> - <TD><A HREF="html/Allocproof.html">Allocproof</A></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/Tunneling.html">Tunneling</A></TD> - <TD><A HREF="html/Tunnelingproof.html">Tunnelingproof</A></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/Linearize.html">Linearize</A></TD> - <TD><A HREF="html/Linearizeproof.html">Linearizeproof</A></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/CleanupLabels.html">CleanupLabels</A></TD> - <TD><A HREF="html/CleanupLabelsproof.html">CleanupLabelsproof</A></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/Debugvar.html">Debugvar</A></TD> - <TD><A HREF="html/Debugvarproof.html">Debugvarproof</A></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/Stacking.html">Stacking</A><BR> - <A HREF="html/Bounds.html">Bounds</A><BR> - <A HREF="html/Stacklayout.html"><I>Stacklayout</I></A></TD> - <TD><A HREF="html/Stackingproof.html">Stackingproof</A><br> - <A HREF="html/Separation.html">Separation</A></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.powerpc.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/Asmgen.html"><I>Asmgen</I></A></TD> - <TD><A HREF="html/Asmgenproof0.html"><I>Asmgenproof0</I></A><BR> - <A HREF="html/Asmgenproof1.html"><I>Asmgenproof1</I></A><BR> - <A HREF="html/Asmgenproof.html"><I>Asmgenproof</I></A></TD> + <TD><A HREF="html/compcert.powerpc.Asmgen.html"><I>Asmgen</I></A></TD> + <TD><A HREF="html/compcert.backend.Asmgenproof0.html"><I>Asmgenproof0</I></A><BR> + <A HREF="html/compcert.powerpc.Asmgenproof1.html"><I>Asmgenproof1</I></A><BR> + <A HREF="html/compcert.powerpc.Asmgenproof.html"><I>Asmgenproof</I></A></TD> </TR> </TABLE> <H3>All together</H3> <UL> -<LI> <A HREF="html/Compiler.html">Compiler</A>: composing the passes together; +<LI> <A HREF="html/compcert.driver.Compiler.html">Compiler</A>: composing the passes together; whole-compiler semantic preservation theorems. -<LI> <A HREF="html/Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems. +<LI> <A HREF="html/compcert.driver.Complements.html">Complements</A>: interesting consequences of the semantic preservation theorems. </UL> <H3>Static analyses</H3> @@ -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. <UL> -<LI> <A HREF="html/Liveness.html">Liveness</A>: liveness analysis</A>. -<LI> <A HREF="html/ValueAnalysis.html">ValueAnalysis</A>: value and alias analysis</A> <BR> -See also: <A HREF="html/ValueDomain.html">ValueDomain</A>: the abstract domain for value analysis.<BR> -See also: <A HREF="html/ValueAOp.html"><I>ValueAOp</I></A>: processor-dependent parts of value analysis. -<LI> <A HREF="html/Deadcode.html">Deadcode</A>: neededness analysis</A> <BR> -See also: <A HREF="html/NeedDomain.html">NeedDomain</A>: the abstract domain for neededness analysis.<BR> -See also: <A HREF="html/NeedOp.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis. +<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/ValueAcompcert.powerpc.Op.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.powerpc.Needcompcert.powerpc.Op.html"><I>NeedOp</I></A>: processor-dependent parts of neededness analysis. </UL> <H3>Type systems</H3> -The <A HREF="html/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. +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/Ctyping.html">RTLtyping</A>: typing for CompCert C + type-checking functions. -<LI> <A HREF="html/RTLtyping.html">RTLtyping</A>: typing for RTL + type +<LI> <A HREF="html/compcert.cfrontend.Ctyping.html">RTLtyping</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/Lineartyping.html">Lineartyping</A>: typing for Linear. +<LI> <A HREF="html/compcert.backend.Lineartyping.html">Lineartyping</A>: typing for Linear. </UL> <HR> |