diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-03-19 09:53:00 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-03-19 09:53:00 +0000 |
| commit | 22d8a1d40e38d1ca15d16fdc0aafca8d6228ecae (patch) | |
| tree | 5850b2eb1d8c7b317fa3e239f4218230b188dedc | |
| parent | f85ac5c25d9dbefed72dda18c1d56e2391668c58 (diff) | |
| download | compcert-kvx-22d8a1d40e38d1ca15d16fdc0aafca8d6228ecae.tar.gz compcert-kvx-22d8a1d40e38d1ca15d16fdc0aafca8d6228ecae.zip | |
Nettoyages doc
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
| -rw-r--r-- | backend/Linearize.v | 6 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 15 |
2 files changed, 6 insertions, 15 deletions
diff --git a/backend/Linearize.v b/backend/Linearize.v index 42330ed9..de372cc5 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 12d0a1f3..a7b01861 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 -> |