aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--mppa_k1c/Machregs.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index 4e8eedda..ee3a63c7 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -216,6 +216,7 @@ Definition two_address_op (op: operation) : bool :=
| Omadd | Omaddimm _
| Omaddl | Omaddlimm _
| Omsub | Omsubl
+ | Osel _ _
| Oinsf _ _ | Oinsfl _ _ => true
| _ => false
end.