diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-09 09:43:54 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-05-09 09:43:54 +0200 |
| commit | ced4ff38f1309f05c9b750bde241bf87b83745fa (patch) | |
| tree | 8f2047616bf033b7b8cc28852a0a44bdd184a266 /powerpc/PrintOp.ml | |
| parent | a6b6bf31121d975c915c01f501618d97df7879fb (diff) | |
| download | compcert-ced4ff38f1309f05c9b750bde241bf87b83745fa.tar.gz compcert-ced4ff38f1309f05c9b750bde241bf87b83745fa.zip | |
Updated PrintOp for the single-precision FP operations.
Diffstat (limited to 'powerpc/PrintOp.ml')
| -rw-r--r-- | powerpc/PrintOp.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 664280f9..b0213014 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -49,6 +49,7 @@ let print_operation reg pp = function | Omove, [r1] -> reg pp r1 | Ointconst n, [] -> fprintf pp "%ld" (camlint_of_coqint n) | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) + | Osingleconst n, [] -> fprintf pp "%Ff" (camlfloat_of_coqfloat32 n) | Oaddrsymbol(id, ofs), [] -> fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs) | Oaddrstack ofs, [] -> @@ -95,7 +96,14 @@ let print_operation reg pp = function | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2 | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2 | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2 + | Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1 + | Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1 + | Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2 + | Osubfs, [r1;r2] -> fprintf pp "%a -fs %a" reg r1 reg r2 + | Omulfs, [r1;r2] -> fprintf pp "%a *fs %a" reg r1 reg r2 + | Odivfs, [r1;r2] -> fprintf pp "%a /fs %a" reg r1 reg r2 | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1 + | Ofloatofsingle, [r1] -> fprintf pp "floatofsingle(%a)" reg r1 | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1 | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2 | Omakelong, [r1;r2] -> fprintf pp "makelong(%a,%a)" reg r1 reg r2 |