From 1fe68ad575178f7d8a775906947d2fed94d40976 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 30 Jul 2011 09:54:35 +0000 Subject: 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 --- arm/Asmgenretaddr.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'arm/Asmgenretaddr.v') diff --git a/arm/Asmgenretaddr.v b/arm/Asmgenretaddr.v index 5238d215..48b6328c 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. -- cgit