diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-27 10:23:16 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-10-27 10:23:16 +0000 |
| commit | e882493e2c4b91024b42f0603ca6869e95695e85 (patch) | |
| tree | 1d90dda6b56b541310d8b8703152fdcd49e8a7fa /common | |
| parent | 7f6ac3209e7fb7d822780c7e990fb604b11a6409 (diff) | |
Linearize: utilisation d'une heuristique externe d'enumeration des noeuds du CFG
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@437 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common')
| -rw-r--r-- | common/Main.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/common/Main.v b/common/Main.v index db15929..bfee3ff 100644 --- a/common/Main.v +++ b/common/Main.v @@ -100,7 +100,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res PPC.fundef := @@ CSE.transf_fundef @@@ Allocation.transf_fundef @@ Tunneling.tunnel_fundef - @@ Linearize.transf_fundef + @@@ Linearize.transf_fundef @@ Reload.transf_fundef @@@ Stacking.transf_fundef @@@ PPCgen.transf_fundef. @@ -224,7 +224,7 @@ Proof. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H6) as [p5 [H5 P5]]. clear H6. generalize (transform_program_partial_program _ _ _ _ _ _ P5). clear P5. intro P5. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H5) as [p4 [H4 P4]]. - clear H5. generalize (transform_program_partial_program _ _ _ _ _ _ P4). clear P4. intro P4. + clear H5. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H4) as [p3 [H3 P3]]. clear H4. generalize (transform_program_partial_program _ _ _ _ _ _ P3). clear P3. intro P3. destruct (transform_partial_program_compose _ _ _ _ _ _ _ _ H3) as [p2 [H2 P2]]. @@ -240,7 +240,7 @@ Proof. assert (WT4 : LTLtyping.wt_program p4). subst p4. apply Tunnelingtyping.program_typing_preserved. auto. assert (WT5 : LTLintyping.wt_program p5). - subst p5. apply Linearizetyping.program_typing_preserved. auto. + apply Linearizetyping.program_typing_preserved with p4. auto. auto. assert (WT6 : Lineartyping.wt_program p6). subst p6. apply Reloadtyping.program_typing_preserved. auto. assert (WT7: Machtyping.wt_program p7). @@ -250,7 +250,7 @@ Proof. apply Machabstr2concr.exec_program_equiv; auto. apply Stackingproof.transf_program_correct with p6; auto. subst p6; apply Reloadproof.transf_program_correct; auto. - subst p5; apply Linearizeproof.transf_program_correct; auto. + apply Linearizeproof.transf_program_correct with p4; auto. subst p4; apply Tunnelingproof.transf_program_correct. apply Allocproof.transf_program_correct with p2; auto. subst p2; apply CSEproof.transf_program_correct. |