diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-25 16:24:06 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-25 16:24:06 +0000 |
| commit | b5325808cb1d36d4ff500d2fb754fe7a424e8329 (patch) | |
| tree | 02a27bf00828ce9c176dfd7f84f87a3f766691a1 /backend/Stackingproof.v | |
| parent | 65a29b666dffa2a06528bef062392c809db7efd6 (diff) | |
Simplification de la semantique de LTL et LTLin. Les details lies aux conventions d'appel sont maintenant geres de maniere plus locale dans la passe Reload.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@701 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1759d7f..a9187ee 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -726,9 +726,9 @@ Lemma agree_return_regs: (forall r, In r int_callee_save_regs \/ In r float_callee_save_regs -> rs' r = ls0 (R r)) -> - (forall r, LTL.return_regs ls0 ls (R r) = rs' r). + (forall r, return_regs ls0 ls (R r) = rs' r). Proof. - intros; unfold LTL.return_regs. + intros; unfold return_regs. case (In_dec Loc.eq (R r) temporaries); intro. rewrite H0. eapply agree_reg; eauto. apply int_callee_save_not_destroyed; auto. @@ -778,10 +778,10 @@ Qed. Lemma agree_callee_save_return_regs: forall ls1 ls2, - agree_callee_save (LTL.return_regs ls1 ls2) ls1. + agree_callee_save (return_regs ls1 ls2) ls1. Proof. intros; red; intros. - unfold LTL.return_regs. destruct l; auto. + unfold return_regs. destruct l; auto. generalize (int_callee_save_not_destroyed m); intro. generalize (float_callee_save_not_destroyed m); intro. destruct (In_dec Loc.eq (R m) temporaries). tauto. @@ -988,7 +988,7 @@ Lemma save_callee_save_correct: star step tge (State stack tf sp (save_callee_save fe k) rs empty_frame m) E0 (State stack tf sp k rs fr' m) - /\ agree (LTL.call_regs ls) ls rs fr' cs. + /\ agree (call_regs ls) ls rs fr' cs. Proof. intros. unfold save_callee_save. exploit save_callee_save_int_correct; eauto. @@ -997,7 +997,7 @@ Proof. intros [fr2 [A2 [B2 C2]]]. exists fr2. split. eapply star_trans. eexact A1. eexact A2. traceEq. - constructor; unfold LTL.call_regs; auto. + constructor; unfold call_regs; auto. (* agree_local *) intros. rewrite C2; auto with stacking. rewrite C1; auto with stacking. |