diff options
| author |  varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-03 09:15:24 +0000 |
|---|---|---|
| committer | varobert <varobert@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-07-03 09:15:24 +0000 |
| commit | c677d5021a9a6e057b15cf9df8ca9ce7c0f5ae30 (patch) | |
| tree | 765798824239f826f5cd008eecf1fdb0ea6820f6 /checklink/Asm_printers.ml | |
| parent | 3de3ecc23d8ab5d6d45451075467dd70981f1061 (diff) | |
checklink: adaptation to the new floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'checklink/Asm_printers.ml')
| -rw-r--r-- | checklink/Asm_printers.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml index 9f6a540..094d51d 100644 --- a/checklink/Asm_printers.ml +++ b/checklink/Asm_printers.ml @@ -186,7 +186,7 @@ let string_of_instruction = function | Plhax (i0, i1, i2) -> "Plhax(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Plhz (i0, c1, i2) -> "Plhz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" | Plhzx (i0, i1, i2) -> "Plhzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" -| Plfi (f0, f1) -> "Plfi(" ^ string_of_freg f0 ^ ", " ^ string_of_float f1 ^ ")" +| Plfi (f0, f1) -> "Plfi(" ^ string_of_freg f0 ^ ", " ^ string_of_ffloat f1 ^ ")" | Plwz (i0, c1, i2) -> "Plwz(" ^ string_of_ireg i0 ^ ", " ^ string_of_constant c1 ^ ", " ^ string_of_ireg i2 ^ ")" | Plwzx (i0, i1, i2) -> "Plwzx(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_ireg i2 ^ ")" | Pmfcrbit (i0, c1) -> "Pmfcrbit(" ^ string_of_ireg i0 ^ ", " ^ string_of_crbit c1 ^ ")" @@ -232,8 +232,8 @@ let string_of_init_data = function | Init_int8(i) -> "Init_int8(" ^ string_of_int (z_int_lax i) ^ ")" | Init_int16(i) -> "Init_int16(" ^ string_of_int (z_int_lax i) ^ ")" | Init_int32(i) -> "Init_int32(" ^ string_of_int32i (z_int32 i) ^ ")" -| Init_float32(f) -> "Init_float32(" ^ string_of_float f ^ ")" -| Init_float64(f) -> "Init_float64(" ^ string_of_float f ^ ")" +| Init_float32(f) -> "Init_float32(" ^ string_of_ffloat f ^ ")" +| Init_float64(f) -> "Init_float64(" ^ string_of_ffloat f ^ ")" | Init_space(z) -> "Init_space(" ^ string_of_int (z_int z) ^ ")" | Init_addrof(ident, ofs) -> "Init_addrof(" ^ string_of_pos ident ^ ", " ^ string_of_int32i (z_int32 ofs) ^ ")" |