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

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.