diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-28 17:53:46 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-29 16:06:00 +0100 |
commit | ba51ef8f74a36501574ca44c664fec2736b4a724 (patch) | |
tree | f87f720134651a060d63662c98de62b6fbea12e3 /mppa_k1c/Asmblock.v | |
parent | 253446c20b5aa03014fd04bcb21e6fd607a3ac5a (diff) | |
download | compcert-kvx-ba51ef8f74a36501574ca44c664fec2736b4a724.tar.gz compcert-kvx-ba51ef8f74a36501574ca44c664fec2736b4a724.zip |
Avancement sur exec_basic_instr_pcvar + exec_load et exec_store prennent des ireg au lieu de preg
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 14ceb082..282723f1 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -958,14 +958,14 @@ Definition eval_offset (ofs: offset) : ptrofs := end. Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem) - (d: preg) (a: ireg) (ofs: offset) := + (d: ireg) (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: preg) (a: ireg) (ofs: offset) := + (s: ireg) (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' |