diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-10-22 16:54:24 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-10-22 16:54:24 +0000 |
commit | 210352d90e5972aabfb253f7c8a38349f53917b3 (patch) | |
tree | 93ccbf36e6840118abe84ee940252a7a1fbc7720 /backend/Machabstr2mach.v | |
parent | ee41c6eae5af0703605780e0b3d8f5c3937f3276 (diff) | |
download | compcert-210352d90e5972aabfb253f7c8a38349f53917b3.tar.gz compcert-210352d90e5972aabfb253f7c8a38349f53917b3.zip |
Lever la restriction sur les fonctions externes, restriction qui exigeait que tous les arguments resident en registres
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Machabstr2mach.v')
-rw-r--r-- | backend/Machabstr2mach.v | 27 |
1 files changed, 26 insertions, 1 deletions
diff --git a/backend/Machabstr2mach.v b/backend/Machabstr2mach.v index a07f64af..8a2b01dd 100644 --- a/backend/Machabstr2mach.v +++ b/backend/Machabstr2mach.v @@ -906,6 +906,29 @@ Proof. constructor. exact A. constructor. Qed. +(** Preservation of arguments to external functions. *) + +Lemma transl_extcall_arguments: + forall rs fr sg args stk base cs m ms, + Machabstr.extcall_arguments rs fr sg args -> + callstack_invariant ((fr, stk, base) :: cs) m ms -> + wt_frame fr -> + extcall_arguments rs ms (Vptr stk base) sg args. +Proof. + unfold Machabstr.extcall_arguments, extcall_arguments; intros. + assert (forall locs vals, + Machabstr.extcall_args rs fr locs vals -> + extcall_args rs ms (Vptr stk base) locs vals). + induction locs; intros; inversion H2; subst; clear H2. + constructor. + constructor; auto. + inversion H7; subst; clear H7. + constructor. + constructor. eapply callstack_get_slot; eauto. + eapply wt_get_slot; eauto. + auto. +Qed. + (** * The proof of simulation *) Section SIMULATION. @@ -1132,7 +1155,9 @@ Proof. auto. (* external function *) - exists ms; split. econstructor; eauto. auto. + exists ms; split. econstructor; eauto. + eapply transl_extcall_arguments; eauto. + auto. Qed. End SIMULATION. |