diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-25 11:43:20 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-25 11:43:20 +0100 |
| commit | a9763cd4327e12316d62e80648122f122581cca4 (patch) | |
| tree | 0670cd0e7cb2bae722e357f2a41939af7671ad1b /riscV | |
| parent | 6c72e95b59f07e7356c05d95b3015df01a4389cf (diff) | |
| download | compcert-kvx-a9763cd4327e12316d62e80648122f122581cca4.tar.gz compcert-kvx-a9763cd4327e12316d62e80648122f122581cca4.zip | |
Adding missing operators in PrintOp for debugging
Diffstat (limited to 'riscV')
| -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 9ec474b3..7e78283e 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -156,6 +156,11 @@ let print_operation reg pp = function | Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1 | Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1 | Ocmp c, args -> print_condition reg pp (c, args) + | 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 |