summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-03-19 09:53:00 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-03-19 09:53:00 +0000
commit22d8a1d40e38d1ca15d16fdc0aafca8d6228ecae (patch)
tree5850b2eb1d8c7b317fa3e239f4218230b188dedc /backend
parentf85ac5c25d9dbefed72dda18c1d56e2391668c58 (diff)
Nettoyages doc
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend')
-rw-r--r--backend/Linearize.v6
-rw-r--r--backend/Linearizeproof.v15
2 files changed, 6 insertions, 15 deletions
diff --git a/backend/Linearize.v b/backend/Linearize.v
index 42330ed..de372cc 100644
--- a/backend/Linearize.v
+++ b/backend/Linearize.v
@@ -63,7 +63,7 @@ Open Scope error_monad_scope.
In this file, we present linearization in a way that clearly
separates the heuristic part (choosing an order for the basic blocks)
- from the actual code transformation parts. We proceed in three passes:
+ from the actual code transformation parts. We proceed in two passes:
- Choosing an order for the nodes. This returns an enumeration of CFG
nodes stating that they must be laid out in the order shown in the
list.
@@ -110,11 +110,11 @@ Definition reachable (f: LTL.function) : PMap.t bool :=
Parameter enumerate_aux: LTL.function -> PMap.t bool -> list node.
-(** Now comes the validation of an enumeration a posteriori. *)
+(** Now comes the a posteriori validation of a node enumeration. *)
Module Nodeset := FSetAVL.Make(OrderedPositive).
-(** Build a Nodeset.t from a list of nodes, checking that the list
+(** Build a [Nodeset.t] from a list of nodes, checking that the list
contains no duplicates. *)
Fixpoint nodeset_of_list (l: list node) (s: Nodeset.t)
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 12d0a1f..a7b0186 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -128,8 +128,8 @@ Qed.
- All nodes for reachable basic blocks must be in the list.
- The list is without repetition (so that no code duplication occurs).
-We prove that our [enumerate] function satisfies both conditions. *)
-
+We prove that the result of the [enumerate] function satisfies both
+conditions. *)
Lemma nodeset_of_list_correct:
forall l s s',
@@ -211,7 +211,7 @@ Qed.
(** * Properties related to labels *)
(** If labels are globally unique and the LTLin code [c] contains
- a subsequence [Llabel lbl :: c1], [find_label lbl c] returns [c1].
+ a subsequence [Llabel lbl :: c1], then [find_label lbl c] returns [c1].
*)
Fixpoint unique_labels (c: code) : Prop :=
@@ -299,15 +299,6 @@ Proof.
auto.
Qed.
-(*
-Lemma transf_function_inv:
- forall f tf, transf_function f = OK tf ->
- exists enum, enumerate f = OK enum /\ fn_code tf = add_branch (LTL.fn_entrypoint f) (linearize_body f enum).
-Proof.
- intros. monadInv H. exists x; auto.
-Qed.
-*)
-
Lemma find_label_lin:
forall f tf pc b,
transf_function f = OK tf ->