summaryrefslogtreecommitdiff
path: root/arm/Asmgenretaddr.v
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-07-30 09:54:35 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2011-07-30 09:54:35 +0000
commit1fe68ad575178f7d8a775906947d2fed94d40976 (patch)
tree3bb4b2d1b101f66bcb6f84bd36ce8e334082f7ea /arm/Asmgenretaddr.v
parent9b45e1d24a337e3f0047bf5056315169d4203b49 (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.v8
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.