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/PPCgenproof.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/PPCgenproof.v')
| -rw-r--r-- | backend/PPCgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v index 32649998..9cbbc659 100644 --- a/backend/PPCgenproof.v +++ b/backend/PPCgenproof.v @@ -1061,11 +1061,11 @@ Lemma exec_function_body_prop_: (align_16_top (- fn_framesize f) (fn_stacksize f)) = (m1, stk) -> let sp := Vptr stk (Int.repr (- fn_framesize f)) 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 ge f sp (fn_code f) ms m3 t (Mreturn :: c) ms' m4 -> exec_instr_prop f sp (fn_code f) ms m3 t (Mreturn :: c) ms' 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_prop f parent ra ms m t ms' (free m4 stk). Proof. intros; red; intros. |