diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 11:17:57 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 11:17:57 +0200 |
| commit | a289d73e791be5a760c8a9b2f3de2064f001a770 (patch) | |
| tree | e106a015b1eb2a33a107135267da9d73243d0215 /mppa_k1c/Asmvliw.v | |
| parent | e1c864b670812eda55e0ee129855c69d32c8b84a (diff) | |
| download | compcert-kvx-a289d73e791be5a760c8a9b2f3de2064f001a770.tar.gz compcert-kvx-a289d73e791be5a760c8a9b2f3de2064f001a770.zip | |
use sq to save pairs of registers
Diffstat (limited to 'mppa_k1c/Asmvliw.v')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 5 |
1 files changed, 2 insertions, 3 deletions
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 |