aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/NeedOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'kvx/NeedOp.v')
-rw-r--r--kvx/NeedOp.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/kvx/NeedOp.v b/kvx/NeedOp.v
index cc86fc88..5a3b7190 100644
--- a/kvx/NeedOp.v
+++ b/kvx/NeedOp.v
@@ -131,6 +131,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Olongoffloat | Olonguoffloat | Ofloatoflong | Ofloatoflongu => op1 (default nv)
| Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
| Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
+ | Ointofsingle_ne | Ointuofsingle_ne => op1 (default nv)
+ | Olongoffloat_ne | Olonguoffloat_ne => op1 (default nv)
| Ocmp c => needs_of_condition c
| Oextfz _ _ | Oextfs _ _ | Oextfzl _ _ | Oextfsl _ _ => op1 (default nv)
| Oinsf _ _ | Oinsfl _ _ => op2 (default nv)