Commit 6c72e95b authored by David Monniaux's avatar David Monniaux
Browse files

écrase X31

parent f1cd6a0d
Pipeline #59032 waiting for manual action with stage
......@@ -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 =>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment