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/Allocproof.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/Allocproof.v')
| -rw-r--r-- | backend/Allocproof.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 07c0f58b..0b252d56 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -1231,9 +1231,7 @@ Proof. destruct (regalloc f t). intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; simpl; auto. congruence. congruence. congruence. - destruct (type_external_function e). intro EQ; inversion EQ; subst tf. reflexivity. - congruence. Qed. Lemma entrypoint_function_translated: @@ -1780,7 +1778,7 @@ Lemma transl_function_correct: exec_function_prop (Internal f) args m t vres (free m2 stk). Proof. intros; red; intros until tf. - unfold transf_fundef, transf_function. + unfold transf_fundef, transf_partial_fundef, transf_function. caseEq (type_function f). intros env TRF. caseEq (analyze f). @@ -1856,7 +1854,7 @@ Lemma transl_external_function_correct: Proof. intros; red; intros. simpl in H0. - destruct (type_external_function ef); simplify_eq H0; intro. + simplify_eq H0; intro. exists (Locmap.set (R (loc_result (funsig tf))) res ls); split. subst tf. eapply exec_funct_external; eauto. apply Locmap.gss. |