diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
| commit | 5312915c1b29929f82e1f8de80609a277584913f (patch) | |
| tree | 0f7ee475743f0eb05d352148a9e1f0b861ee9d34 /powerpc | |
| parent | f3250c32ff42ae18fd03a5311c1f0caec3415aba (diff) | |
| download | compcert-kvx-5312915c1b29929f82e1f8de80609a277584913f.tar.gz compcert-kvx-5312915c1b29929f82e1f8de80609a277584913f.zip | |
Use Flocq for floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/PrintAsm.ml | 11 | ||||
| -rw-r--r-- | powerpc/PrintOp.ml | 2 |
2 files changed, 7 insertions, 6 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 3492de42..65d6ce0f 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -669,8 +669,8 @@ let print_instruction oc tbl pc = function | Plfi(r1, c) -> let lbl = new_label() in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment c; - float_literals := (lbl, Int64.bits_of_float c) :: !float_literals; + fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment (camlfloat_of_coqfloat c); + float_literals := (lbl, camlint64_of_coqint (Floats.Float.bits_of_double c)) :: !float_literals; | Plfs(r1, c, r2) -> fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 | Plfsx(r1, r2, r3) -> @@ -1070,13 +1070,14 @@ let print_init oc = function | Init_int32 n -> fprintf oc " .long %ld\n" (camlint_of_coqint n) | Init_float32 n -> - fprintf oc " .long %ld %s %.18g\n" (Int32.bits_of_float n) comment n + fprintf oc " .long %ld %s %.18g\n" (camlint_of_coqint (Floats.Float.bits_of_single n)) + comment (camlfloat_of_coqfloat n) | Init_float64 n -> - let b = Int64.bits_of_float n in + let b = camlint64_of_coqint (Floats.Float.bits_of_double n) in fprintf oc " .long %Ld, %Ld %s %.18g\n" (Int64.shift_right_logical b 32) (Int64.logand b 0xFFFFFFFFL) - comment n + comment (camlfloat_of_coqfloat n) | Init_space n -> let n = camlint_of_z n in if n > 0l then fprintf oc " .space %ld\n" n diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 5bc46586..a2f9ff83 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -48,7 +48,7 @@ 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) - | Ofloatconst n, [] -> fprintf pp "%F" n + | Ofloatconst n, [] -> fprintf pp "%F" (camlfloat_of_coqfloat n) | Oaddrsymbol(id, ofs), [] -> fprintf pp "\"%s\" + %ld" (extern_atom id) (camlint_of_coqint ofs) | Oaddrstack ofs, [] -> |