diff options
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 2ad99304..796bad3d 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -142,7 +142,7 @@ Inductive instruction : Type := | Paddic: ireg -> ireg -> constant -> instruction (**r add immediate and set carry *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add carry *) - | Pallocframe: Z -> int -> instruction (**r allocate new stack frame (pseudo) *) + | Pallocframe: Z -> int -> int -> instruction (**r allocate new stack frame (pseudo) *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -324,7 +324,7 @@ lbl: .double floatcst lfd rdst, 0(r1) addi r1, r1, 8 >> -- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction +- [Pallocframe sz ofs retofs]: in the formal semantics, this pseudo-instruction allocates a memory block with bounds [0] and [sz], stores the value of register [r1] (the stack pointer, by convention) at offset [ofs] in this block, and sets [r1] to a pointer to the bottom of this @@ -623,7 +623,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Paddze rd r1 => Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m - | Pallocframe sz ofs => + | Pallocframe sz ofs _ => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Int.zero in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with |