aboutsummaryrefslogtreecommitdiffstats
path: root/ia32/NeedOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/NeedOp.v')
-rw-r--r--ia32/NeedOp.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/ia32/NeedOp.v b/ia32/NeedOp.v
index 9a75cba8..575532b1 100644
--- a/ia32/NeedOp.v
+++ b/ia32/NeedOp.v
@@ -110,6 +110,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Oshllimm _ => op1 (default nv)
| Oshrl => op2 (default nv)
| Oshrlimm _ => op1 (default nv)
+ | Oshrxlimm n => op1 (default nv)
| Oshrlu => op2 (default nv)
| Oshrluimm _ => op1 (default nv)
| Ororlimm _ => op1 (default nv)