aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/Machregs.v
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/Machregs.v')
-rw-r--r--mppa_k1c/Machregs.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index ee3a63c7..5a7d42b4 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -216,7 +216,7 @@ Definition two_address_op (op: operation) : bool :=
| Omadd | Omaddimm _
| Omaddl | Omaddlimm _
| Omsub | Omsubl
- | Osel _ _
+ | Osel _ _ | Oselimm _ _ | Osellimm _ _
| Oinsf _ _ | Oinsfl _ _ => true
| _ => false
end.