From a289d73e791be5a760c8a9b2f3de2064f001a770 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 11:17:57 +0200 Subject: use sq to save pairs of registers --- mppa_k1c/Asmvliw.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'mppa_k1c/Asmvliw.v') diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 248b8660..6ebc8340 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1189,11 +1189,10 @@ Definition parexec_store_q_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_q) ( let (s0, s1) := gpreg_q_expand s in match eval_offset ofs with | OK eofs => - let base := Val.offset_ptr (rsr a) eofs in - match Mem.storev Many64 mr base (rsr s0) with + match Mem.storev Many64 mr (Val.offset_ptr (rsr a) eofs) (rsr s0) with | None => Stuck | Some m1 => - match Mem.storev Many64 m1 base (rsr s1) with + match Mem.storev Many64 m1 (Val.offset_ptr (rsr a) (Ptrofs.add eofs (Ptrofs.repr 8))) (rsr s1) with | None => Stuck | Some m2 => Next rsw m2 end -- cgit