From 9976ed7a27434cfcc334959ef5f20e4967ff8dcb Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 28 Mar 2010 10:01:53 +0000
Subject: Updating ARM port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/Asmgen.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'arm/Asmgen.v')

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 069a08a2..2a3b3f36 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -473,10 +473,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pblsymb symb :: k
   | Mtailcall sig (inl r) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe f.(fn_link_ofs) :: Pbreg (ireg_of r) :: k)
+        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+         :: Pbreg (ireg_of r) :: k)
   | Mtailcall sig (inr symb) =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe f.(fn_link_ofs) :: Pbsymb symb :: k)
+        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+         :: Pbsymb symb :: k)
   | Mlabel lbl =>
       Plabel lbl :: k
   | Mgoto lbl =>
@@ -488,7 +490,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) :=
       Pbtbl IR14 tbl :: k
   | Mreturn =>
       loadind_int IR13 f.(fn_retaddr_ofs) IR14
-        (Pfreeframe f.(fn_link_ofs) :: Pbreg IR14 :: k)
+        (Pfreeframe (-f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs)
+         :: Pbreg IR14 :: k)
   end.
 
 Definition transl_code (f: Mach.function) (il: list Mach.instruction) :=
-- 
cgit