diff options
Diffstat (limited to 'mppa_k1c/Asmblock.v')
-rw-r--r-- | mppa_k1c/Asmblock.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index fb0f8c37..cf6fef3b 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -816,14 +816,14 @@ Definition eval_offset (ofs: offset) : ptrofs := end. Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem) - (d: ireg) (a: ireg) (ofs: offset) := + (d: preg) (a: ireg) (ofs: offset) := match Mem.loadv chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) with | None => Stuck | Some v => Next (rs#d <- v) m end. Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem) - (s: ireg) (a: ireg) (ofs: offset) := + (s: preg) (a: ireg) (ofs: offset) := match Mem.storev chunk m (Val.offset_ptr (rs a) (eval_offset ofs)) (rs s) with | None => Stuck | Some m' => Next rs m' |