diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 09:54:35 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-30 09:54:35 +0000 |
| commit | 1fe68ad575178f7d8a775906947d2fed94d40976 (patch) | |
| tree | 3bb4b2d1b101f66bcb6f84bd36ce8e334082f7ea /arm/Asmgenretaddr.v | |
| parent | 9b45e1d24a337e3f0047bf5056315169d4203b49 (diff) | |
ARM codegen ported to new ABI + VFD floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm/Asmgenretaddr.v')
| -rw-r--r-- | arm/Asmgenretaddr.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v index 5238d21..48b6328 100644 --- a/arm/Asmgenretaddr.v +++ b/arm/Asmgenretaddr.v @@ -68,7 +68,7 @@ Qed. Inductive return_address_offset: Mach.function -> Mach.code -> int -> Prop := | return_address_offset_intro: forall c f ofs, - code_tail ofs (transl_function f) (transl_code f c) -> + code_tail ofs (fn_code (transl_function f)) (transl_code f c) -> return_address_offset f c (Int.repr ofs). (** We now show that such an offset always exists if the Mach code [c] @@ -209,11 +209,11 @@ Proof. Qed. Lemma return_address_exists: - forall f sg ros c, is_tail (Mcall sg ros :: c) f.(fn_code) -> + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> exists ra, return_address_offset f c ra. Proof. - intros. assert (is_tail (transl_code f c) (transl_function f)). - unfold transl_function. IsTail. apply transl_code_tail; eauto with coqlib. + intros. assert (is_tail (transl_code f c) (fn_code (transl_function f))). + unfold transl_function. simpl. IsTail. apply transl_code_tail; eauto with coqlib. destruct (is_tail_code_tail _ _ H0) as [ofs A]. exists (Int.repr ofs). constructor. auto. Qed. |