From 6c72e95b59f07e7356c05d95b3015df01a4389cf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 3 Feb 2021 14:29:33 +0100 Subject: écrase X31 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- riscV/Asm.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/riscV/Asm.v b/riscV/Asm.v index 9a4b2a57..5d3518f2 100644 --- a/riscV/Asm.v +++ b/riscV/Asm.v @@ -957,7 +957,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pselectl rd rb rt rf => Next (nextinstr (rs#rd <- (ExtValues.select01_long - (rs###rb) (rs###rt) (rs###rf)))) m + (rs###rb) (rs###rt) (rs###rf))) + #X31 <- Vundef) m | Plabel lbl => Next (nextinstr rs) m | Ploadsymbol rd s ofs => -- cgit