Updating ARM port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1291 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 3 deletions

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