diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-08 15:43:29 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-08 15:43:29 +0000 |
| commit | 43b4d97a655e52e3962c0d14bda39dacb24af901 (patch) | |
| tree | d4ea6a6694cf3e69323bf7a8756ea4b583c2b068 /backend/PPCgen.v | |
| parent | 593ce3f7c5647e284cd2fdc3dd3ed41be9563982 (diff) | |
| download | compcert-43b4d97a655e52e3962c0d14bda39dacb24af901.tar.gz compcert-43b4d97a655e52e3962c0d14bda39dacb24af901.zip | |
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
Diffstat (limited to 'backend/PPCgen.v')
| -rw-r--r-- | backend/PPCgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 := |