aboutsummaryrefslogtreecommitdiffstats
path: root/arm/Asmexpand.ml
diff options
context:
space:
mode:
authorMichael Schmidt <github@mschmidt.me>2017-08-02 16:01:41 +0200
committerMichael Schmidt <github@mschmidt.me>2017-08-02 16:01:41 +0200
commite5d8d8d2d67daed762f6e0cc8f486b2c1b37bb20 (patch)
tree32284b33df8a2c58cd69e639c680ebbf9433755e /arm/Asmexpand.ml
parent9f6e2aac73ca1f863d236f86f446b0894c8ebcef (diff)
downloadcompcert-kvx-e5d8d8d2d67daed762f6e0cc8f486b2c1b37bb20.tar.gz
compcert-kvx-e5d8d8d2d67daed762f6e0cc8f486b2c1b37bb20.zip
Push correct register
Diffstat (limited to 'arm/Asmexpand.ml')
-rw-r--r--arm/Asmexpand.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index 1a473e03..fbe2e0bb 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -421,7 +421,7 @@ let expand_instruction instr =
let ofs' = camlint_of_coqint ofs in
if ofs' >= 4096l && sz' >= ofs' then begin
expand_subimm IR13 IR13 (coqint_of_camlint (Int32.sub sz' (Int32.add ofs' 4l)));
- emit (Ppush [IR13]);
+ emit (Ppush [IR12]);
expand_subimm IR13 IR13 ofs;
emit (Pcfi_adjust sz);
end else begin