From 801cd27eb78a9ba9dce6f62626288531905fcfed Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Mar 2021 18:48:53 +0100 Subject: [Admitted checker] Oracle expansion for float/float32 constant init --- riscV/PrintOp.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'riscV/PrintOp.ml') 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, [] -> -- cgit