summaryrefslogtreecommitdiff
path: root/ia32/Machregs.v
diff options
context:
space:
mode:
Diffstat (limited to 'ia32/Machregs.v')
-rw-r--r--ia32/Machregs.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index 85b561e..da80a6e 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -211,6 +211,7 @@ Definition two_address_op (op: operation) : bool :=
| Oorimm _ => true
| Oxor => true
| Oxorimm _ => true
+ | Onot => true
| Oshl => true
| Oshlimm _ => true
| Oshr => true