From 43b4d97a655e52e3962c0d14bda39dacb24af901 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 8 Sep 2006 15:43:29 +0000 Subject: Stocker l'adresse de retour a l'offset 12 au lieu de l'offset 4 pour meilleure compatibilite avec les conventions de MacOSX git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@85 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/PPCgen.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/PPCgen.v') diff --git a/backend/PPCgen.v b/backend/PPCgen.v index 6cf06991..ba8ea285 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -485,7 +485,7 @@ Definition transl_instr (i: Mach.instruction) (k: code) := transl_cond cond args (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) | Mreturn => - Plwz GPR2 (Cint (Int.repr 4)) GPR1 :: + Plwz GPR2 (Cint (Int.repr 12)) GPR1 :: Pmtlr GPR2 :: Pfreeframe :: Pblr :: k end. @@ -501,7 +501,7 @@ Definition transl_function (f: Mach.function) := Pallocframe (- f.(fn_framesize)) (align_16_top (-f.(fn_framesize)) f.(fn_stacksize)) :: Pmflr GPR2 :: - Pstw GPR2 (Cint (Int.repr 4)) GPR1 :: + Pstw GPR2 (Cint (Int.repr 12)) GPR1 :: transl_code f.(fn_code). Fixpoint code_size (c: code) : Z := -- cgit