From 9976ed7a27434cfcc334959ef5f20e4967ff8dcb Mon Sep 17 00:00:00 2001 From: xleroy 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/Asm.v | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index e689c20c..13c2e57b 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -146,7 +146,7 @@ Inductive instruction : Type := (* Pseudo-instructions *) | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) - | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *) + | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) | Pbtbl: ireg -> list label -> instruction. (**r N-way branch through a jump table *) @@ -503,12 +503,16 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | None => Error | Some m2 => OK (nextinstr (rs#IR13 <- sp)) m2 end - | Pfreeframe pos => + | Pfreeframe lo hi pos => match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with | None => Error | Some v => match rs#IR13 with - | Vptr stk ofs => OK (nextinstr (rs#IR13 <- v)) (Mem.free m stk) + | Vptr stk ofs => + match Mem.free m stk lo hi with + | None => Error + | Some m' => OK (nextinstr (rs#IR13 <- v)) m' + end | _ => Error end end -- cgit