diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 10:29:23 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 10:29:23 +0100 |
| commit | be4dcbd9fcd3c859a0fae7a37cd226493a8abefb (patch) | |
| tree | 3d69513c3f082e7db01bd9ade327c0ebc8a2f441 /riscV/PrintOp.ml | |
| parent | fd1a0395e540ee9fcd91d8f09161b34a22d9c51e (diff) | |
| parent | a9763cd4327e12316d62e80648122f122581cca4 (diff) | |
| download | compcert-kvx-be4dcbd9fcd3c859a0fae7a37cd226493a8abefb.tar.gz compcert-kvx-be4dcbd9fcd3c859a0fae7a37cd226493a8abefb.zip | |
Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work
Diffstat (limited to 'riscV/PrintOp.ml')
| -rw-r--r-- | riscV/PrintOp.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index e11dd530..84380251 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -222,6 +222,11 @@ let print_operation reg pp = function | OEfeqs, [r1;r2] -> fprintf pp "OEfeqs(%a,%s,%a)" reg r1 (comparison_name Ceq) reg r2 | OEflts, [r1;r2] -> fprintf pp "OEflts(%a,%s,%a)" reg r1 (comparison_name Clt) reg r2 | OEfles, [r1;r2] -> fprintf pp "OEfles(%a,%s,%a)" reg r1 (comparison_name Cle) reg r2 + | Obits_of_single, [r1] -> fprintf pp "bits_of_single(%a)" reg r1 + | Obits_of_float, [r1] -> fprintf pp "bits_of_float(%a)" reg r1 + | Osingle_of_bits, [r1] -> fprintf pp "single_of_bits(%a)" reg r1 + | Ofloat_of_bits, [r1] -> fprintf pp "float_of_bits(%a)" reg r1 + | Oselectl, [rb;rt;rf] -> fprintf pp "selectl(b:%a, t:%a, f:%a)" reg rb reg rt reg rf | _ -> fprintf pp "<bad operator>" let print_addressing reg pp = function |