aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Asmblock.v
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2019-01-28 17:53:46 +0100
committerCyril SIX <cyril.six@kalray.eu>2019-01-29 16:06:00 +0100
commitba51ef8f74a36501574ca44c664fec2736b4a724 (patch)
treef87f720134651a060d63662c98de62b6fbea12e3 /mppa_k1c/Asmblock.v
parent253446c20b5aa03014fd04bcb21e6fd607a3ac5a (diff)
downloadcompcert-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.v4
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'