diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 18:48:53 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-03-02 18:48:53 +0100 |
| commit | 801cd27eb78a9ba9dce6f62626288531905fcfed (patch) | |
| tree | 83a5811930ebb3fa659fa2e531fc270f1e145b38 /riscV/PrintOp.ml | |
| parent | 3e953ef41f736ed5b7db699b1adf21d46cb5b8db (diff) | |
| download | compcert-kvx-801cd27eb78a9ba9dce6f62626288531905fcfed.tar.gz compcert-kvx-801cd27eb78a9ba9dce6f62626288531905fcfed.zip | |
[Admitted checker] Oracle expansion for float/float32 constant init
Diffstat (limited to 'riscV/PrintOp.ml')
| -rw-r--r-- | riscV/PrintOp.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml index 84380251..4734795a 100644 --- a/riscV/PrintOp.ml +++ b/riscV/PrintOp.ml @@ -97,10 +97,10 @@ let print_condition reg pp = function let print_operation reg pp = function | Omove, [r1] -> reg pp r1 - | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) - | Olongconst n, [] -> fprintf pp "%LdL" (camlint64_of_coqint n) - | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) - | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n) + | Ointconst n, [] -> fprintf pp "Ointconst(%ld)" (camlint_of_coqint n) + | Olongconst n, [] -> fprintf pp "Olongconst(%LdL)" (camlint64_of_coqint n) + | Ofloatconst n, [] -> fprintf pp "Ofloatconst(%F)" (camlfloat_of_coqfloat n) + | Osingleconst n, [] -> fprintf pp "Osingleconst(%Ff)" (camlfloat_of_coqfloat32 n) | Oaddrsymbol(id, ofs), [] -> fprintf pp "\"%s\" + %Ld" (extern_atom id) (camlint64_of_ptrofs ofs) | Oaddrstack ofs, [] -> |