diff options
Diffstat (limited to 'x86/PrintOp.ml')
| -rw-r--r-- | x86/PrintOp.ml | 18 |
1 files changed, 3 insertions, 15 deletions
diff --git a/x86/PrintOp.ml b/x86/PrintOp.ml index faa5bb5f..356b2027 100644 --- a/x86/PrintOp.ml +++ b/x86/PrintOp.ml @@ -14,17 +14,9 @@ open Printf open Camlcoq -open Integers +open PrintAST open Op -let comparison_name = function - | Ceq -> "==" - | Cne -> "!=" - | Clt -> "<" - | Cle -> "<=" - | Cgt -> ">" - | Cge -> ">=" - let print_condition reg pp = function | (Ccomp c, [r1;r2]) -> fprintf pp "%a %ss %a" reg r1 (comparison_name c) reg r2 @@ -43,13 +35,9 @@ let print_condition reg pp = function | (Ccompluimm(c, n), [r1]) -> fprintf pp "%a %slu %Lu" reg r1 (comparison_name c) (camlint64_of_coqint n) | (Ccompf c, [r1;r2]) -> - fprintf pp "%a %sf %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompf c, [r1;r2]) -> - fprintf pp "%a not(%sf) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sf %a" reg r1 (fp_comparison_name c) reg r2 | (Ccompfs c, [r1;r2]) -> - fprintf pp "%a %sfs %a" reg r1 (comparison_name c) reg r2 - | (Cnotcompfs c, [r1;r2]) -> - fprintf pp "%a not(%sfs) %a" reg r1 (comparison_name c) reg r2 + fprintf pp "%a %sfs %a" reg r1 (fp_comparison_name c) reg r2 | (Cmaskzero n, [r1]) -> fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n) | (Cmasknotzero n, [r1]) -> |