diff options
Diffstat (limited to 'ia32/PrintAsm.ml')
| -rw-r--r-- | ia32/PrintAsm.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index d67fb9e..9a2648a 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -644,6 +644,8 @@ let print_instruction oc = function fprintf oc " xorl %a, %a\n" ireg r1 ireg rd | Pxor_ri(rd, n) -> fprintf oc " xorl $%a, %a\n" coqint n ireg rd + | Pnot(rd) -> + fprintf oc " notl %a\n" ireg rd | Psal_rcl(rd) -> fprintf oc " sall %%cl, %a\n" ireg rd | Psal_ri(rd, n) -> |