diff options
Diffstat (limited to 'aarch64/Asm.v')
| -rw-r--r-- | aarch64/Asm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asm.v b/aarch64/Asm.v index b5f4c838..c5f4032e 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -1067,7 +1067,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out let sp := (Vptr stk Ptrofs.zero) in match Mem.storev Mint64 m1 (Val.offset_ptr sp pos) rs#SP with | None => Stuck - | Some m2 => Next (nextinstr (rs #X29 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2 + | Some m2 => Next (nextinstr (rs #X15 <- (rs#SP) #SP <- sp #X16 <- Vundef)) m2 end | Pfreeframe sz pos => match Mem.loadv Mint64 m (Val.offset_ptr rs#SP pos) with |