diff options
| -rw-r--r-- | riscV/Asm.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 => |