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/Mach.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Mach.v') diff --git a/backend/Mach.v b/backend/Mach.v index 75b5baa8..b8bf1e36 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -253,7 +253,7 @@ with exec_instrs: (** In addition to reserving the word at offset 0 in the activation record for maintaining the linking of activation records, - we need to reserve the word at offset 4 to store the return address + we need to reserve the word at offset 12 to store the return address into the caller. However, the return address (a pointer within the code of the caller) is not precisely known at this point: it will be determined only after the final translation to PowerPC @@ -280,12 +280,12 @@ with exec_function_body: = (m1, stk) -> let sp := Vptr stk (Int.repr (-f.(fn_framesize))) in store_stack m1 sp Tint (Int.repr 0) parent = Some m2 -> - store_stack m2 sp Tint (Int.repr 4) ra = Some m3 -> + store_stack m2 sp Tint (Int.repr 12) ra = Some m3 -> exec_instrs f sp f.(fn_code) rs m3 t (Mreturn :: c) rs' m4 -> load_stack m4 sp Tint (Int.repr 0) = Some parent -> - load_stack m4 sp Tint (Int.repr 4) = Some ra -> + load_stack m4 sp Tint (Int.repr 12) = Some ra -> exec_function_body f parent ra rs m t rs' (Mem.free m4 stk) with exec_function: -- cgit