diff options
| author | Michael Schmidt <github@mschmidt.me> | 2017-12-15 14:06:49 +0100 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2017-12-15 14:06:49 +0100 |
| commit | 57f97c6ba73ce1269d31f563341ec3eefe931d06 (patch) | |
| tree | 0ebcc80a901a41d7672169905a62624beed11631 /arm/TargetPrinter.ml | |
| parent | 9b98d49bbc105d998f9a63868d4b23bfab8d4cf7 (diff) | |
| download | compcert-kvx-57f97c6ba73ce1269d31f563341ec3eefe931d06.tar.gz compcert-kvx-57f97c6ba73ce1269d31f563341ec3eefe931d06.zip | |
Reintroduce informative comments for Pflid_lbl/Pflis_lbl in target printer
Diffstat (limited to 'arm/TargetPrinter.ml')
| -rw-r--r-- | arm/TargetPrinter.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index d402b4a8..56619cdd 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -502,10 +502,13 @@ struct fprintf oc " movt %a, #:upper16:%a\n" ireg r1 symbol_offset (id, ofs) | Pflid_lbl (r1,lbl,f) -> - fprintf oc " vldr %a, %a\n" freg r1 print_label lbl + let f = camlint64_of_coqint(Floats.Float.to_bits f) in + fprintf oc " vldr %a, %a %s %.12g\n" + freg r1 print_label lbl comment (Int64.float_of_bits f) | Pflis_lbl (r1,lbl,f) -> - fprintf oc " vldr %a, %a\n" - freg_single r1 print_label lbl + let f = camlint_of_coqint(Floats.Float32.to_bits f) in + fprintf oc " vldr %a, %a %s %.12g\n" + freg_single r1 print_label lbl comment (Int32.float_of_bits f) | Pflid_imm (r1,f) -> let f = camlint64_of_coqint(Floats.Float.to_bits f) in fprintf oc " vmov.f64 %a, #%.15F\n" |